[ghc-steering-committee] #536: Type-level literals as a separate language extension, rec: accept

Richard Eisenberg lists at richarde.dev
Mon May 8 11:48:08 UTC 2023


I remain opposed, but I understand that I'm in the minority here.

Richard

> On May 1, 2023, at 2:19 PM, Simon Peyton Jones <simon.peytonjones at gmail.com> wrote:
> 
> 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 <mailto: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> 
> > <mailto: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> <mailto: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> <mailto: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> <mailto: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>>
> >>         <mailto: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>>
> >>         <mailto: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/ <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 <mailto:ghc-steering-committee at haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <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/20230508/ac10065a/attachment-0001.html>


More information about the ghc-steering-committee mailing list