<div dir="ltr"><div dir="ltr">On Wed, Mar 8, 2023 at 2:19 PM Joachim Breitner <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
It seems that one motivation is that DataKinds is “bad” in some way,<br>
namely in that term constructors are available in types. So if we<br>
accept this proposal, does that mean we agree with that assessment,<br>
what are we going to do about it? Is there a better way of referring to<br>
term constructors that we could work to wards to that works for<br>
everyone? Or are we going to have multiple future Haskell dialects, one<br>
with strict separation between terms and types, one with some things<br>
also on the type level (basic literals, but no tuples or user-defined<br>
constructors), and a third one that’s the full story?<br></blockquote><div><br></div><div>DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.</div><div><br></div><div>There are two ways to avoid this issue:</div><div>1. Keep namespaces separate and double down on using punned constructor names.</div><div>2. Merge terms and types, discouraging punned constructor names.</div><div><br></div><div>Each approach could indeed lead to a "dialect" of sorts.</div><div>* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type-level programming.</div><div>* At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.</div><div><br></div><div>If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.</div><div><br></div><div>- Vlad</div><div><br></div></div></div>