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

[Adam Gundry]

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