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

[Vladislav Zavialov]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20231018/6631271a/attachment.html>