<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="">Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here.<div class=""><br class=""></div><div class="">Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.)</div><div class=""><br class=""></div><div class="">Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha).</div><div class=""><br class=""></div><div class="">Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub.</div><div class=""><br class=""></div><div class="">Richard</div><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <<a href="mailto:arnaud.spiwack@tweag.io" class="">arnaud.spiwack@tweag.io</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).</div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" class="">mail@joachim-breitner.de</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">Hi,<br class="">
<br class="">
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:<br class="">
> DataKinds is indeed a "bad" extension because it introduces 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 punned<br class="">
> constructor names.<br class="">
> 2. Merge terms and types, discouraging punned 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 extension moves us<br class="">
> in the direction of option (1), and I imagine the proposed<br class="">
> TypeLevelLiterals would be often used in conjunction with TypeData.<br class="">
> This carves out a limited, conservative language subset for type-<br class="">
> level programming.<br class="">
> * At the same time, #270 "Support pun-free code" moves us in the<br class="">
> direction of option (2), and I expect it to be the better option when<br class="">
> it comes to fully fledged dependently-typed programming envisioned by<br class="">
> #378.<br class="">
> <br class="">
> If I had to choose, I'd go with option (2). I don't see myself using<br class="">
> TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a<br class="">
> thousand flowers bloom" persuasion, hence my 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 approach (2) (which<br class="">
is the general direction outlined by #378), or is yet another take on<br class="">
the issue?<br class="">
If DataKinds was not what we want according to #378, but the fragment<br class="">
carved out by TypeLevelLiterals was, then that would be a strong reason<br class="">
for me to acccept TypeLevelLiterals.<br class="">
But if DataKinds is the goal (or at least “the” goal), then I 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="">
Joachim Breitner<br class="">
<a href="mailto:mail@joachim-breitner.de" target="_blank" class="">mail@joachim-breitner.de</a><br class="">
<a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank" class="">http://www.joachim-breitner.de/</a><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>