<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 proposal has been revised for clarity, yet much of the payload is the same. I've just made a few small suggestions, but I believe we can deliberate here in parallel.<div class=""><br class=""></div><div class="">To recap:</div><div class=""><span id="x-apple-selection:end"></span><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Proposal PR: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281" class="">https://github.com/ghc-proposals/ghc-proposals/pull/281</a></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Proposal text: <a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst" class="">https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst</a></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">The text of the proposal is long and detailed, but do not be daunted: it is simpler in practice than it appears.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">The main payload of the proposal is: Introduce a new extension -XRequiredTypeArguments. With this extension enabled, the `forall ... ->` syntax, currently in existence in kinds, is now available in types (of ordinary functions). This means that function definitions and call sites are sometimes required to write a type argument. The type argument is *not* preceded by @ or any other syntactic marker.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">This is useful for defining what would otherwise be ambiguous types. Example:</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"></div><blockquote type="cite" class=""><div class="">sizeof :: forall a -> Sizeable a => Int</div><div class="">sizeof = ...</div><div class=""><br class=""></div><div class="">intWidth = sizeof Int</div></blockquote><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">There are further examples and motivation in the proposal.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">The rest of the proposal is simply about dealing with odd corner cases that come up with the main payload. In particular, mixing types in with terms with no syntactic signifier means that we must be careful about parsing and namespaces. If a type argument is written in the syntax that is shared between types and terms (including function application!) and uses identifiers in scope in only one of the two namespaces, nothing unusual can be observed. But, of course, there are corner cases. Here are some of the salient details:</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">- Define type-syntax and term-syntax, where the choice of syntax is always driven by syntactic markers, such as :: or @. See the <a href="https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#lexical-scoping-term-syntax-and-type-syntax-and-renaming" class="">dependent types proposal</a> for more details. Parsing and name-resolution are controlled by whether a phrase is in type-syntax or term-syntax. For name resolution, if a lookup fails in the first namespace (the term-level namespace in term-syntax or the type-level namespace in type-syntax), we try the other namespace before failing.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">- One unfortunate consequence of this extra namespace looking is around implicit quantification. If we have `a = 42` in scope and write `f :: a -> a`, that `a` will <i class="">not</i><span style="font-style: normal;" class=""> be implicitly quantified. Instead, the user will get an error about the appearance of a term in a type -- but only if -XRequiredTypeArguments is on. This change affects no current code, but it does make the extension fork-like, in that enabling the new extension is not conservative.</span></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">- Because term- vs type-syntax is controlled by syntax, a required type argument is in *term*-syntax and gets name-resolved *as a term*. In the absence of punning, this works out fine, but it is possible that a punned identifier will cause confusion. The proposal allows users to write `type` to signify a switch to type-syntax.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">- The proposal also includes a way to avoid punning for the built-in types with privileged syntax: lists and tuples. This method allows users to specify -XNoListTupleTypeSyntax to disable the list and tuple syntax in types (but still allows it for terms). The proposal also suggests exporting type List = [] from Data.List and other synonyms for tuples from Data.Tuple.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">---------------</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">I recommend acceptance. When doing type-level programming, the lack of this feature is strange, leading to ambiguous types and easy-to-forget arguments and easy-to-make type errors. The design space here is difficult, but this proposal is very much in keeping with the design sketch of our recently-accepted #378, in particular <a href="https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#dependent-application-and-the-static-subset" class="">its section on this point</a>. I believe the design described here is both backward compatible with what we have today (users who do not use this feature will not notice a difference) and forward compatible with a cohesive design for dependent types.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">The "unfortunate consequence" above is, well, unfortunate, but I think it is unavoidable in the context of #378 -- and it will not bite if the user avoids puns.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">It would be great to bring this long-running proposal to a conclusion, so I'd love to hear your opinions in the next two weeks.</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Thanks!</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Richard</div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div><blockquote type="cite" class=""><div class="">On Jul 19, 2021, at 3:22 PM, Richard Eisenberg <<a href="mailto:rae@richarde.dev" class="">rae@richarde.dev</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=us-ascii" class=""><div 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 class=""><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 class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">> <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 class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">--------------</div><div class=""><br class=""></div><div class="">One development on the GitHub tracker that may be of interest:</div><div class=""><br class=""></div><div class="">@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 class=""><br class=""></div><div class="">> sizeOf :: Storable a => a -> Int</div><div class=""><br class=""></div><div class="">where the argument to sizeOf is always unevaluated and ignored. The proposal under consideration would allow this to change to</div><div class=""><br class=""></div><div class="">> sizeOf' :: forall a -> Storable a => Int</div><div class=""><br class=""></div><div class="">(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 class=""><br class=""></div><div class="">* 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></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>