<div dir="ltr"><div class="gmail_default" style="font-family:tahoma,sans-serif">I am also in favour for the reasons Adam gives.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 1 May 2023 at 14:17, 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">Thanks for your comments Iavor, your input is appreciated.<br>
<br>
The ongoing discussion on language extensions made me think about <br>
proposal #536 again. With due respect to Richard, I still think we <br>
should accept it, for the following reasons:<br>
<br>
* We owe it to proposal authors to make decisions in a reasonably <br>
prompt fashion. The ongoing discussion is unlikely to be resolved <br>
extremely quickly, and the extension split in the proposal accords with <br>
the de facto approach to language extensions as feature flags.<br>
<br>
* Even if we accept the premise that we have too many extensions, <br>
accepting the proposal doesn't really make things worse (if we already <br>
have a hundred extensions too many, what harm one more?).<br>
<br>
* As Iavor says, there is no deep reason for type literals and <br>
DataKinds to be grouped as part of the same feature; it is merely a <br>
historical accident. If we later move to a model where features are <br>
enabled by default and controlled using warnings, it would be equally <br>
reasonable to have separate warnings for type literals and DataKinds.<br>
<br>
* The proposed change is simple, low effort to implement and maintain, <br>
and is clearly desired by some users.<br>
<br>
* The workaround with -Werror=unticked-promoted-constructors doesn't <br>
accurately characterise the language with type literals but not DataKinds.<br>
<br>
Feel free to object, of course. :-)<br>
<br>
Adam<br>
<br>
<br>
<br>
On 20/03/2023 17:59, Iavor Diatchki wrote:<br>
> Hello,<br>
> <br>
> I am not on the committee but as the original author of the type <br>
> literals extensions I thought I'd give my 2c. I am strongly in favor of <br>
> separating type literals from DataKinds, they are not really together <br>
> for any deep reason.<br>
> <br>
> For me the separate extension would be useful because it makes it <br>
> possible to use type literals with the `TypeData` extension, which for <br>
> me, is a much nicer way to work with type level things than `DataKinds`.<br>
> <br>
> -Iavor<br>
> <br>
> <br>
> <br>
> On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <<a href="mailto:chris@chrisdornan.com" target="_blank">chris@chrisdornan.com</a> <br>
> <mailto:<a href="mailto:chris@chrisdornan.com" target="_blank">chris@chrisdornan.com</a>>> wrote:<br>
> <br>
> I am also in favour of extensions that focus on solving a single<br>
> problem well and giving users precise control over what extensions<br>
> they deploy. If we get this right then we should be able discover<br>
> which extensions people want and those that are free of unintended<br>
> consequences, and can put them on track to be included in a GHC and<br>
> then Haskell standard.<br>
> <br>
> This proposal isn't ambitious but it does otherwise appear to<br>
> qualify so I am in favour.<br>
> <br>
> Chris<br>
> <br>
> <br>
> <br>
> <br>
>> On 20 Mar 2023, at 08:43, Simon Peyton Jones<br>
>> <<a href="mailto:simon.peytonjones@gmail.com" target="_blank">simon.peytonjones@gmail.com</a> <mailto:<a href="mailto:simon.peytonjones@gmail.com" target="_blank">simon.peytonjones@gmail.com</a>>><br>
>> wrote:<br>
>><br>
>> Personally I'm happy with having orthogonal extensions that enable<br>
>> just one thing. That allows our users to do what they want,<br>
>> rather than telling them what they want.<br>
>><br>
>> On this particular proposal I don't think it's a big deal either<br>
>> way, but I'd vote in favour. It's not exactly true to say that it<br>
>> duplicates an existing feature. I think Richard's point is that<br>
>> you can get a warning for using an unticked constructor (but<br>
>> nothing for using a ticked one). That's different from getting an<br>
>> error if you use a constructor in a type, ticked or not.<br>
>><br>
>> This particular proposal is easy to describe and easy to<br>
>> implement. But I don't think we should burn a lot of cycles on<br>
>> it... it's a matter of taste, so we could just vote.<br>
>><br>
>> Simon<br>
>><br>
>> On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg<br>
>> <<a href="mailto:lists@richarde.dev" target="_blank">lists@richarde.dev</a> <mailto:<a href="mailto:lists@richarde.dev" target="_blank">lists@richarde.dev</a>>> wrote:<br>
>><br>
>> This argument gave me pause. Thanks, Adam. I think, for me, it<br>
>> comes down to this: what do we think will be more useful to<br>
>> more of our users? A notion of a core language -- perhaps<br>
>> implemented by different compilers -- with extensions? Or a<br>
>> unified language GHC/Haskell which allows subsetting? I tend<br>
>> to think the latter, though I'm not sure.<br>
>><br>
>> Regarding this particular proposal: I remain against the<br>
>> proposal, as it duplicates an existing feature. That's a<br>
>> simple reason to be against a proposal.<br>
>><br>
>> Richard<br>
>><br>
>> > On Mar 10, 2023, at 9:15 AM, Adam Gundry<br>
>> <<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a> <mailto:<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a>>> wrote:<br>
>> ><br>
>> > This proposal is very helpful in exposing some of the<br>
>> divisions about the interpretation of extensions that exist<br>
>> within the committee! "Let a thousand flowers bloom" vs<br>
>> "more-extensions-make-me-wince", if you like.<br>
>> ><br>
>> > For what it's worth I tend to be in the former camp. I think<br>
>> we should strive for orthogonality and avoid bundling together<br>
>> distinct features merely because they have related effects.<br>
>> Instead we should construct our language via composition of<br>
>> simple components. And I think it's reasonable to say that<br>
>> TypeLevelLiterals and (the rest of) DataKinds are clearly<br>
>> distinct and can be understood in isolation.<br>
>> ><br>
>> > If the number of extensions is a problem, that points to the<br>
>> need to better structure our documentation and gather coherent<br>
>> subsets of extensions into manageable pieces (much as GHC2021<br>
>> tries to do). Beyond that I'd like to understand the downsides<br>
>> better (e.g. what costs does it actually impose on HLS to have<br>
>> another extension?).<br>
>> ><br>
>> > A conversation with one of the authors of Helium this week<br>
>> made me think that in the GHC proposals process we have tended<br>
>> to neglect the possible presence of other Haskell<br>
>> implementations. It's not realistic to expect that anyone will<br>
>> reimplement the whole of GHC Haskell, but perhaps there is a<br>
>> fragment large enough to be useful for a fair number of<br>
>> Haskell programs but also small enough to be independently<br>
>> implemented (e.g. by Helium). It would strike me as plausible<br>
>> that such an implementation might want to support<br>
>> TypeData+TypeLevelLiterals but not DataKinds.<br>
>> ><br>
>> > Adam<br>
>> ><br>
>> ><br>
>> > On 09/03/2023 16:21, Richard Eisenberg wrote:<br>
>> >> Though I see the arguments in the other direction, I vote<br>
>> against this proposal. As Joachim argues, adding an extension<br>
>> puts a tax on the entire ecosystem by adding one more bit of<br>
>> context a reader has to have to understand code. In addition,<br>
>> HLS will have to be aware of this extension. And the benefits<br>
>> seem pretty marginal here.<br>
>> >> Can we instead simply provide a warning? The warning here<br>
>> would be something like the -Wpuns idea, in that it helps the<br>
>> author keep to a particular subset of the language. (We might<br>
>> want to collect such warnings somehow in our documentation.)<br>
>> >> Actually, it occurs to me we already have the warning:<br>
>> -Wunticked-promoted-constructors. We've put that warning in<br>
>> the -Weverything bin (not even -Wall) because in the past<br>
>> we've decided that we shouldn't recommend/require the ' when<br>
>> using a constructor in a type. But actually, setting<br>
>> -Werror=unticked-promoted-constructors would seem to be a<br>
>> perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK,<br>
>> not perfect: you could still use a constructor in a type with<br>
>> a ' mark. But I think that's great, actually, because perhaps<br>
>> an author wary of constructors in types still might need to<br>
>> use one, in one place, in a 2,000-line file. This ticks all<br>
>> the boxes (ha ha).<br>
>> >> Having discovered this replacement, I'm now pretty strongly<br>
>> against this proposal. I'll also post on GitHub.<br>
>> >> Richard<br>
>> >>> On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack<br>
>> <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a> <mailto:<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>><br>
>> <mailto:<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a><br>
>> <mailto:<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>>>> wrote:<br>
>> >>><br>
>> >>> I can see where the author is coming from. But as Joachim,<br>
>> I find myself unconvinced that it is worth yet one extra<br>
>> extension (but then again, I'm the<br>
>> more-extensions-make-me-wince member of this committee).<br>
>> >>><br>
>> >>> On Wed, 8 Mar 2023 at 13:56, Joachim Breitner<br>
>> <<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a> <mailto:<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>><br>
>> <mailto:<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a><br>
>> <mailto:<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>>>> wrote:<br>
>> >>><br>
>> >>> Hi,<br>
>> >>><br>
>> >>> Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb<br>
>> Vladislav Zavialov:<br>
>> >>> > DataKinds is indeed a "bad" extension because it<br>
>> introduces<br>
>> >>> ambiguity<br>
>> >>> > to name resolution.<br>
>> >>> ><br>
>> >>> > There are two ways to avoid this issue:<br>
>> >>> > 1. Keep namespaces separate and double down on using<br>
>> punned<br>
>> >>> > constructor names.<br>
>> >>> > 2. Merge terms and types, discouraging punned<br>
>> constructor names.<br>
>> >>> ><br>
>> >>> > Each approach could indeed lead to a "dialect" of sorts.<br>
>> >>> ><br>
>> >>> > * The (accepted and recently implemented) TypeData<br>
>> extension<br>
>> >>> moves us<br>
>> >>> > in the direction of option (1), and I imagine the<br>
>> proposed<br>
>> >>> > TypeLevelLiterals would be often used in conjunction<br>
>> with TypeData.<br>
>> >>> > This carves out a limited, conservative language<br>
>> subset for type-<br>
>> >>> > level programming.<br>
>> >>> > * At the same time, #270 "Support pun-free code"<br>
>> moves us in the<br>
>> >>> > direction of option (2), and I expect it to be the<br>
>> better option<br>
>> >>> when<br>
>> >>> > it comes to fully fledged dependently-typed programming<br>
>> >>> envisioned by<br>
>> >>> > #378.<br>
>> >>> ><br>
>> >>> > If I had to choose, I'd go with option (2). I don't<br>
>> see myself using<br>
>> >>> > TypeData, nor TypeLevelLiterals for that matter. But<br>
>> I am of a<br>
>> >>> "let a<br>
>> >>> > thousand flowers bloom" persuasion, hence my<br>
>> recommendation to<br>
>> >>> > accept.<br>
>> >>><br>
>> >>><br>
>> >>> Thanks for putting this into a clearer context.<br>
>> >>><br>
>> >>> Where does DataKind fit in? Is it a natural part of<br>
>> approach (2)<br>
>> >>> (which<br>
>> >>> is the general direction outlined by #378), or is yet<br>
>> another take on<br>
>> >>> the issue?<br>
>> >>> If DataKinds was not what we want according to #378,<br>
>> but the fragment<br>
>> >>> carved out by TypeLevelLiterals was, then that would be<br>
>> a strong<br>
>> >>> reason<br>
>> >>> for me to acccept TypeLevelLiterals.<br>
>> >>> But if DataKinds is the goal (or at least “the” goal),<br>
>> then I<br>
>> >>> think I’d<br>
>> >>> like to see stronger arguments for why it should be split.<br>
>> >>><br>
>> >>><br>
>> >>> Cheers,<br>
>> >>> Joachim<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>