<div dir="ltr"><div>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><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">mail@joachim-breitner.de</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">Hi,<br>
<br>
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:<br>
> DataKinds is indeed a "bad" extension because it introduces 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 punned<br>
> constructor names.<br>
> 2. Merge terms and types, discouraging punned constructor names.<br>
> <br>
> Each approach could indeed lead to a "dialect" of sorts.<br>
><br>
> * The (accepted and recently implemented) TypeData extension moves us<br>
> in the direction of option (1), and I imagine the proposed<br>
> TypeLevelLiterals would be often used in conjunction with TypeData.<br>
> This carves out a limited, conservative language subset for type-<br>
> level programming.<br>
> * At the same time, #270 "Support pun-free code" moves us in the<br>
> direction of option (2), and I expect it to be the better option when<br>
> it comes to fully fledged dependently-typed programming envisioned by<br>
> #378.<br>
> <br>
> If I had to choose, I'd go with option (2). I don't see myself using<br>
> TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a<br>
> thousand flowers bloom" persuasion, hence my 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 approach (2) (which<br>
is the general direction outlined by #378), or is yet another take on<br>
the issue?<br>
If DataKinds was not what we want according to #378, but the fragment<br>
carved out by TypeLevelLiterals was, then that would be a strong reason<br>
for me to acccept TypeLevelLiterals.<br>
But if DataKinds is the goal (or at least “the” goal), then I think I’d<br>
like to see stronger arguments for why it should be split.<br>
<br>
<br>
Cheers,<br>
Joachim<br>
<br>
-- <br>
Joachim Breitner<br>
  <a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a><br>
  <a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.de/</a><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>