[ghc-steering-committee] #536: Type-level literals as a separate language extension, rec: accept
Simon Peyton Jones
simon.peytonjones at gmail.com
Mon Mar 20 08:43:55 UTC 2023
Personally I'm happy with having orthogonal extensions that enable just one
thing. That allows our users to do what they want, rather than telling
them what they want.
On this particular proposal I don't think it's a big deal either way, but
I'd vote in favour. It's not exactly true to say that it duplicates an
existing feature. I think Richard's point is that you can get a warning
for using an unticked constructor (but nothing for using a ticked one).
That's different from getting an error if you use a constructor in a type,
ticked or not.
This particular proposal is easy to describe and easy to implement. But I
don't think we should burn a lot of cycles on it... it's a matter of taste,
so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists at richarde.dev> wrote:
> This argument gave me pause. Thanks, Adam. I think, for me, it comes down
> to this: what do we think will be more useful to more of our users? A
> notion of a core language -- perhaps implemented by different compilers --
> with extensions? Or a unified language GHC/Haskell which allows subsetting?
> I tend to think the latter, though I'm not sure.
>
> Regarding this particular proposal: I remain against the proposal, as it
> duplicates an existing feature. That's a simple reason to be against a
> proposal.
>
> Richard
>
> > On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam at well-typed.com> wrote:
> >
> > This proposal is very helpful in exposing some of the divisions about
> the interpretation of extensions that exist within the committee! "Let a
> thousand flowers bloom" vs "more-extensions-make-me-wince", if you like.
> >
> > For what it's worth I tend to be in the former camp. I think we should
> strive for orthogonality and avoid bundling together distinct features
> merely because they have related effects. Instead we should construct our
> language via composition of simple components. And I think it's reasonable
> to say that TypeLevelLiterals and (the rest of) DataKinds are clearly
> distinct and can be understood in isolation.
> >
> > If the number of extensions is a problem, that points to the need to
> better structure our documentation and gather coherent subsets of
> extensions into manageable pieces (much as GHC2021 tries to do). Beyond
> that I'd like to understand the downsides better (e.g. what costs does it
> actually impose on HLS to have another extension?).
> >
> > A conversation with one of the authors of Helium this week made me think
> that in the GHC proposals process we have tended to neglect the possible
> presence of other Haskell implementations. It's not realistic to expect
> that anyone will reimplement the whole of GHC Haskell, but perhaps there is
> a fragment large enough to be useful for a fair number of Haskell programs
> but also small enough to be independently implemented (e.g. by Helium). It
> would strike me as plausible that such an implementation might want to
> support TypeData+TypeLevelLiterals but not DataKinds.
> >
> > Adam
> >
> >
> > On 09/03/2023 16:21, Richard Eisenberg wrote:
> >> Though I see the arguments in the other direction, I vote against this
> proposal. As Joachim argues, adding an extension puts a tax on the entire
> ecosystem by adding one more bit of context a reader has to have to
> understand code. In addition, HLS will have to be aware of this extension.
> And the benefits seem pretty marginal here.
> >> Can we instead simply provide a warning? The warning here would be
> something like the -Wpuns idea, in that it helps the author keep to a
> particular subset of the language. (We might want to collect such warnings
> somehow in our documentation.)
> >> Actually, it occurs to me we already have the warning:
> -Wunticked-promoted-constructors. We've put that warning in the
> -Weverything bin (not even -Wall) because in the past we've decided that we
> shouldn't recommend/require the ' when using a constructor in a type. But
> actually, setting -Werror=unticked-promoted-constructors would seem to be a
> perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect:
> you could still use a constructor in a type with a ' mark. But I think
> that's great, actually, because perhaps an author wary of constructors in
> types still might need to use one, in one place, in a 2,000-line file. This
> ticks all the boxes (ha ha).
> >> Having discovered this replacement, I'm now pretty strongly against
> this proposal. I'll also post on GitHub.
> >> Richard
> >>> On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack at tweag.io
> <mailto:arnaud.spiwack at tweag.io>> wrote:
> >>>
> >>> I can see where the author is coming from. But as Joachim, I find
> myself unconvinced that it is worth yet one extra extension (but then
> again, I'm the more-extensions-make-me-wince member of this committee).
> >>>
> >>> On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <
> mail at joachim-breitner.de <mailto:mail at joachim-breitner.de>> wrote:
> >>>
> >>> Hi,
> >>>
> >>> Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav
> Zavialov:
> >>> > DataKinds is indeed a "bad" extension because it introduces
> >>> ambiguity
> >>> > to name resolution.
> >>> >
> >>> > There are two ways to avoid this issue:
> >>> > 1. Keep namespaces separate and double down on using punned
> >>> > constructor names.
> >>> > 2. Merge terms and types, discouraging punned constructor names.
> >>> >
> >>> > Each approach could indeed lead to a "dialect" of sorts.
> >>> >
> >>> > * The (accepted and recently implemented) TypeData extension
> >>> moves us
> >>> > in the direction of option (1), and I imagine the proposed
> >>> > TypeLevelLiterals would be often used in conjunction with
> TypeData.
> >>> > This carves out a limited, conservative language subset for type-
> >>> > level programming.
> >>> > * At the same time, #270 "Support pun-free code" moves us in the
> >>> > direction of option (2), and I expect it to be the better option
> >>> when
> >>> > it comes to fully fledged dependently-typed programming
> >>> envisioned by
> >>> > #378.
> >>> >
> >>> > If I had to choose, I'd go with option (2). I don't see myself
> using
> >>> > TypeData, nor TypeLevelLiterals for that matter. But I am of a
> >>> "let a
> >>> > thousand flowers bloom" persuasion, hence my recommendation to
> >>> > accept.
> >>>
> >>>
> >>> Thanks for putting this into a clearer context.
> >>>
> >>> Where does DataKind fit in? Is it a natural part of approach (2)
> >>> (which
> >>> is the general direction outlined by #378), or is yet another take
> on
> >>> the issue?
> >>> If DataKinds was not what we want according to #378, but the
> fragment
> >>> carved out by TypeLevelLiterals was, then that would be a strong
> >>> reason
> >>> for me to acccept TypeLevelLiterals.
> >>> But if DataKinds is the goal (or at least “the” goal), then I
> >>> think I’d
> >>> like to see stronger arguments for why it should be split.
> >>>
> >>>
> >>> Cheers,
> >>> Joachim
> >>>
> >>> -- Joachim Breitner
> >>> mail at joachim-breitner.de <mailto:mail at joachim-breitner.de>
> >>> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
> >
> > --
> > Adam Gundry, Haskell Consultant
> > Well-Typed LLP, https://www.well-typed.com/
> >
> > Registered in England & Wales, OC335890
> > 27 Old Gloucester Street, London WC1N 3AX, England
> >
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230320/7058763d/attachment-0001.html>
More information about the ghc-steering-committee
mailing list