<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail_default" style="font-family:tahoma,sans-serif">
It seems to me that this proposal makes DataKinds less complex, by <br>
decomposing it into simpler independent pieces. Indeed, as Simon <br>
mentions on the PR thread, we could reasonably give names to both these <br>
pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion

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