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

[Simon Peyton Jones]

>
> It seems to me that this proposal makes DataKinds less complex, by
> decomposing it into simpler independent pieces. Indeed, as Simon
> mentions on the PR thread, we could reasonably give names to both these
> pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion
>

If we accept at all, I would strongly like to accept in this form.

Simon

On Fri, 20 Oct 2023 at 12:16, Adam Gundry <adam at well-typed.com> wrote:

> I remain in favour of this proposal. I think minimizing the *number* of
> extensions is fundamentally the wrong approach; instead we should aim to
> minimize *complexity*, both of individual extensions and of the system
> as a whole.
>
> It seems to me that this proposal makes DataKinds less complex, by
> decomposing it into simpler independent pieces. Indeed, as Simon
> mentions on the PR thread, we could reasonably give names to both these
> pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion.
>
> Cheers,
>
> Adam
>
>
> On 18/10/2023 17:30, Vladislav Zavialov wrote:
> > Dear Committee,
> >
> > Back in March I initiated a discussion of #536 "Type-level literals as a
> > separate language extension" by Ross Paterson. Quick recap: currently
> > DataKinds controls promotion of ADTs and Symbol/Natural/Char literals.
> > The proposal is to factor out promotion of literals into their own
> > extension, TypeLevelLiterals.
> >
> > I recommended acceptance but received mixed feedback. Summary of
> opinions:
> > Vlad: "rec: accept"
> > SPJ: "content to accept"
> > Joachim: "unsure how that fits with the overall direction we have for
> > namespaces"
> > Arnaud: "unconvinced that it is worth yet one extra extension"
> > Richard: "pretty strongly against"
> > Adam: "avoid bundling together distinct features" (i.e. accept)
> > Chris: "in favour"
> > Iavor (as ex-member): "strongly in favor"
> >
> > Haven't yet expressed their opinion: Simon M. and Moritz.
> >
> > So we have roughly 5 votes in-favor-or-don't-mind and 3 votes
> > against-or-unconvinced. SPJ suggested that we simply count the votes,
> > but after reading the discussion, I find that there's a deeper reason
> > for disagreement. Essentially, we have two camps:
> >
> > 1. "Let a thousand flowers bloom": Haskell should be customizable, built
> > out of small extensions à la carte. (A necessary implication here is
> > that this gives rise to dialects of Haskell that depend on the set of
> > enabled extensions)
> > 2. "More extensions make me wince": Extensions are a necessary evil
> > while we explore the language design space, and we shouldn't create them
> > unnecessarily. (Language editions like GHC2021 help with that, allowing
> > the users to forget about individual extensions and simply use a
> > better/newer Haskell)
> >
> > The 1st paradigm suggests that TypeLevelLiterals should be factored out.
> > TypeLevelLiterals+TypeData form a dialect different from DataKinds with
> > regards to name resolution, which some users might prefer. Let them have
> > it, why not?
> >
> > The 2nd paradigm suggests that breaking DataKinds into smaller
> > extensions is counterproductive. Do we want fewer extensions or more
> > extensions, after all? And as a steering committee, don't we have a
> > clear direction in which we steer?
> >
> > Unfortunately, we don't have a general policy that would clearly tell us
> > which camp/paradigm is right. And it's about time that we make a
> > decision regarding #536, even if we don't have a policy to guide us.
> >
> > Because of that, my new plan is to reject the proposal out of caution.
> > We have at least one "strongly against", and it's enough to give me
> > pause. It's probably better to stick to the status quo, at least until
> > we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a
> > digression, but this also calls into question whether 448 is justified
> > in splitting ScopedTypeVariables
> > into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe
> > we don't want fine-grained extensions after all)
> >
> > The new recommendation is to reject the proposal, but I still can't make
> > this decision single-handedly. So let's do another round of discussion,
> > only this time let's stick to practicalities, not general
> > considerations. Is there anyone on the committee (or do we know someone)
> > who needs TypeLevelLiterals for practical reasons, not just as a matter
> > of taste? For example,
> > 1. You are writing a book and you want to introduce TypeLevelLiterals
> > before DataKinds
> > 2. You are developing or maintaining a library or application that needs
> > TypeLevelLiterals but cannot use DataKinds
> > 3. You are working on an alternative Haskell implementation and intend
> > to support TypeLevelLiterals but not DataKinds
> >
> > If any of the above (or similar) applies, speak up.
> >
> > Vlad
> >
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
> --
> 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/20231020/646e70e4/attachment-0001.html>