<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">This thread has trailed off, having escaped the pen while the shepherd (me) was distracted (first by travel, then by POPL). I'd like to resume it.<div class=""><br class=""></div><div class="">You may wish to refresh yourself on the content of the proposal, which I summarize in <a href="https://mail.haskell.org/pipermail/ghc-steering-committee/2021-May/002454.html" class="">https://mail.haskell.org/pipermail/ghc-steering-committee/2021-May/002454.html</a></div><div class=""><br class=""></div><div class="">My recommendation remains to accept, for the same reasons it was originally.</div><div class=""><br class=""></div><div class="">This proposal is somewhat controversial (it has garnered 278 comments!), and so it would be ideal to hear opinions from as many of you as possible, even if the opinion is just to accept the recommendation.</div><div class=""><br class=""></div><div class="">Simon M wrote the last email in the thread before the hiatus, with a few questions. I'll attempt these now:</div><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jun 7, 2021, at 4:19 AM, Simon Marlow <<a href="mailto:marlowsd@gmail.com" class="">marlowsd@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">As a user I usually need to know whether I'm looking at a type or a term in the code. For doing renaming in your head, it makes a difference whether you're looking at a type or a term: the namespaces are different.</div><div class=""><br class=""></div><div class="">Is it reasonable for that to apply to visible type application too? That is, are we assuming that the user knows they're looking at a type, or are we assuming that the user "shouldn't need to care", or something else?</div></div></div></blockquote><div><br class=""></div><div>My answer: "shouldn't need to care". This is enshrined in the Syntactic Unification Principle (SUP) in <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst:" class="">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst:</a></div><div><br class=""></div><div>> <strong class="">Syntactic Unification Principle (SUP).</strong> In the absence of punning, there is
no difference between type-syntax and term-syntax.</div><div class=""><br class="webkit-block-placeholder"></div><div class="">Here, "punning" means having the same identifier in scope in both terms and types. Forgetting about the possibility of punning, users shouldn't care about whether they're writing a term or a type. All syntax will have equivalent meanings in the two environments. The *only* challenge is around namespacing -- and the LSP says that, in a term, names should correspond to term-level entities.</div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">What could we do if we were allowed to treat types differently? Well, we already do various bits of magic in T2T. But we could also use different name resolution rules. That doesn't necessarily mean we have to defer renaming until during type checking: we could resolve each name twice, once for the term context and once for the type context, and then pick one of these later when we apply the T2T mapping. (earlier Vlad objected to this idea on the grounds that it might introduce spurious recursive dependencies, though).</div></div></div></blockquote><div><br class=""></div><div>We *could* do this, yes, but it's in violation of the LSP (and, perhaps, the SUP). Of course, we wrote the LSP and can choose to break it, but, like Simon PJ, I think the ability to resolve names in the absence of type-checking is very valuable to readers of code.</div><div><br class=""></div><div>--------------</div><div><br class=""></div><div>One development on the GitHub tracker that may be of interest:</div><div><br class=""></div><div>@AntC2 proposes a migration trick to allow functions to migrate from today's world to a world with this new feature. The key example is sizeOf. Today, we have</div><div><br class=""></div><div>> sizeOf :: Storable a => a -> Int</div><div><br class=""></div><div>where the argument to sizeOf is always unevaluated and ignored. The proposal under consideration would allow this to change to</div><div><br class=""></div><div>> sizeOf' :: forall a -> Storable a => Int</div><div><br class=""></div><div>(NB: do not get distracted by the movement of the constraint, which will be invisible at usage sites) The problem is that we would have to make sizeOf' a new function, likely exported from a new library, in order not to clash. This is annoying. So @AntC2 proposes (in my paraphrasing, which @AntC2 has agreed with):</div><div><br class=""></div><div>* With <code class="">-XNoRequiredTypeArguments</code>, if a function <code class="">f</code> takes a required type argument of kind <code class="">Type</code>, then instead you can pass an arbitrary expression. <code class="">f</code> is called with the type of that expression; the expression is never evaluated.</div></div><br class=""></div><div class="">This would allow, e.g. sizeOf True to work with both the old and the new types.</div><div class=""><br class=""></div><div class="">I am against this little addition, because it's narrowly applicable and has negative educational consequences (that is, someone encountering the type written for sizeOf' but then seeing sizeOf' True work correctly will be quite befuddled and likely form a misunderstanding of how forall -> works). Yet I can see this idea's appeal, thus my mentioning it here.</div><div class=""><br class=""></div><div class="">------------------</div><div class=""><br class=""></div><div class="">It would be great if I could hear from everyone on the committee in the next two weeks with their opinion about accepting this proposal.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Richard</div></body></html>