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

Hi, I am also part of that minority, but at least until and unless we come to a clear policy that we want to wean off fine-grined language pragmas, I don’t want to block the enthusiasm of those who have stronger opinions in favor of this particular one. As Adam says, we already have very many extensions, so YOLO. Cheers, Joachim Am Montag, dem 08.05.2023 um 11:48 +0000 schrieb Richard Eisenberg:

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 wrote:

I am also in favour for the reasons Adam gives.

Simon

On Mon, 1 May 2023 at 14:17, Adam Gundry 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 mailto:chris@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      mailto:simon.peytonjones@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      mailto:lists@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          mailto:adam@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          mailto:arnaud.spiwack@tweag.io          mailto:arnaud.spiwack@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          mailto:mail@joachim-breitner.de          mailto:mail@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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

---

ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/