[ghc-steering-committee] #536: Type-level literals as a separate language extension, rec: accept
Simon Peyton Jones
simon.peytonjones at gmail.com
Mon May 1 18:19:27 UTC 2023
I am also in favour for the reasons Adam gives.
Simon
On Mon, 1 May 2023 at 14:17, Adam Gundry <adam at well-typed.com> wrote:
> Thanks for your comments Iavor, your input is appreciated.
>
> The ongoing discussion on language extensions made me think about
> proposal #536 again. With due respect to Richard, I still think we
> should accept it, for the following reasons:
>
> * We owe it to proposal authors to make decisions in a reasonably
> prompt fashion. The ongoing discussion is unlikely to be resolved
> extremely quickly, and the extension split in the proposal accords with
> the de facto approach to language extensions as feature flags.
>
> * Even if we accept the premise that we have too many extensions,
> accepting the proposal doesn't really make things worse (if we already
> have a hundred extensions too many, what harm one more?).
>
> * As Iavor says, there is no deep reason for type literals and
> DataKinds to be grouped as part of the same feature; it is merely a
> historical accident. If we later move to a model where features are
> enabled by default and controlled using warnings, it would be equally
> reasonable to have separate warnings for type literals and DataKinds.
>
> * The proposed change is simple, low effort to implement and maintain,
> and is clearly desired by some users.
>
> * The workaround with -Werror=unticked-promoted-constructors doesn't
> accurately characterise the language with type literals but not DataKinds.
>
> Feel free to object, of course. :-)
>
> Adam
>
>
>
> On 20/03/2023 17:59, Iavor Diatchki wrote:
> > Hello,
> >
> > I am not on the committee but as the original author of the type
> > literals extensions I thought I'd give my 2c. I am strongly in favor of
> > separating type literals from DataKinds, they are not really together
> > for any deep reason.
> >
> > For me the separate extension would be useful because it makes it
> > possible to use type literals with the `TypeData` extension, which for
> > me, is a much nicer way to work with type level things than `DataKinds`.
> >
> > -Iavor
> >
> >
> >
> > On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <chris at chrisdornan.com
> > <mailto:chris at chrisdornan.com>> wrote:
> >
> > I am also in favour of extensions that focus on solving a single
> > problem well and giving users precise control over what extensions
> > they deploy. If we get this right then we should be able discover
> > which extensions people want and those that are free of unintended
> > consequences, and can put them on track to be included in a GHC and
> > then Haskell standard.
> >
> > This proposal isn't ambitious but it does otherwise appear to
> > qualify so I am in favour.
> >
> > Chris
> >
> >
> >
> >
> >> On 20 Mar 2023, at 08:43, Simon Peyton Jones
> >> <simon.peytonjones at gmail.com <mailto:simon.peytonjones at gmail.com>>
> >> wrote:
> >>
> >> 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 <mailto: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 <mailto: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>
> >> <mailto: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>
> >> <mailto: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
>
> --
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230501/1b91d92a/attachment-0001.html>
More information about the ghc-steering-committee
mailing list