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