<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="">Yes, I think this proposal meets the criteria of "needs revision" -- if at least to clarify all the points that have been raised.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 15, 2020, at 11:41 AM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">I agree with Arnaud's observations.</div><div class=""><br class=""></div>It seems that the discussion on this proposal is not converging toward a solution, and now more folks from the community have jumped in, so my inclination would be to move this proposal back to the "needs revision" phase as Simon M suggested earlier.<div class="">Thoughts?<br class=""><div class=""><div class=""><br class=""><div class="">-Iavor</div></div></div></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Oct 13, 2020 at 12:37 AM Spiwack, Arnaud <<a href="mailto:arnaud.spiwack@tweag.io" class="">arnaud.spiwack@tweag.io</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"><div dir="ltr" class=""><div class="">There has been conversation to this effect on the Github PR, for a day or so, starting at <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-707033510" target="_blank" class="">https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-707033510</a> .</div><div class=""><br class=""></div><div class="">But I wanted to point out that there are really two, interlocked, yet distinct, parts in this proposal.</div><div class="">1. Having a `forall a ->` construct for types of terms</div><div class="">2. How is `f blah` parsed if `f` has type `forall a -> …`?</div><div class=""><br class=""></div><div class="">I am definitely sympathetic to (1). As much as I like my `f @…`s I am bound to admit that it produces error messages from the 7th Circle of Hell. And, since it's a very useful pattern, making it "official" is rather neat a plan on paper.<br class=""></div><div class=""><br class=""></div><div class="">But (2) is very very difficult, because we have really two grammars at play here: the grammar for term, and the grammar for types (I'll conflate grammar and name resolution in the following). In the `f @…` style, we switch to the type grammar to parse whatever's in the `@`. But if we want to to write type applications in the `forall a->` case as `f a`, then we sort of have to parse `a` as a term (though there is some leeway in name resolution). And that introduces all sorts of potentially weird behaviour (see the link above for a good documentation of what). Part of the difficulty, I should stress, is that, in types the apostrophe `'` means: I'm speaking of a data constructor, not a type constructor. Whereas in terms, it means: I'm opening a Template Haskell slice.</div><div class=""><br class=""></div><div class="">Part of the impetus for the proposal actually going in the direction of parsing the type argument as a term, is the desire to eventually merge the terms and types grammars. I don't know how widespread this desire actually is (maybe this is something we should speak about). In my personal opinion, it's not a very plausibly achievable goal, nor is it particularly necessary for dependent types. (It does, of course, have a number of advantages, which is why Coq, Agda, and Idris do have a single grammar indeed).</div><div class=""><br class=""></div><div class="">I think that I'd be happier if we had a sigil to switch between the type grammar and the term grammar. But, here, the issue is that nice sigils are harder and harder to come by.</div><div class=""><br class=""></div><div class="">My point, though, is that while this proposal may look like it has a small scope, it actually is a fairly large and intricate proposal, and requires quite a bit of attention.</div><div class=""><br class=""></div><div class="">/Arnaud<br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Oct 5, 2020 at 7:25 PM Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank" class="">iavor.diatchki@gmail.com</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"><div dir="ltr" class="">I've been following the discussion and I think we should keep it in the "committee review" phase because<div class=""> 1. The discussion is due to questions from the committee members, and </div><div class=""> 2. Even though it seems like a lot, mostly it's been along the lines of clarification and better phrasing of things, rather than big changes to the proposal</div><div class=""><br class=""></div><div class="">I don't feel strongly about it, so if others also think we should move it to the discussion phase, I'd be happy to do so, I just don't want to loose the steam we seem to have gathered :)</div><div class=""><br class=""></div><div class="">Let me know,</div><div class="">-Iavor</div><div class=""><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Oct 5, 2020 at 2:38 AM Simon Marlow <<a href="mailto:marlowsd@gmail.com" target="_blank" class="">marlowsd@gmail.com</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"><div dir="ltr" class="">There seems to have been a lot of ensuing discussion on this one, should it go back into the discussion phase?<br class=""></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 2 Oct 2020 at 20:06, Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank" class="">rae@richarde.dev</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"><div class="">I'm in support of this proposal, but I've pushed back on a few softer points. I've commented on GitHub.<div class=""><br class=""></div><div class="">Richard<br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Oct 1, 2020, at 1:07 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class=""><div class=""><div dir="ltr" class=""><div class="">Hello,</div><div class=""><br class=""></div><div class="">Proposal #281 is ready for review by the committee. My recommendation is to accept it, I've</div><div class="">written a summary of my understanding to the proposal and my recommendation on the GitHub</div><div class="">thread, accessible through these links:</div><div class=""><br class=""></div><a href="https://github.com/ghc-proposals/ghc-proposals/pull/281" target="_blank" class="">https://github.com/ghc-proposals/ghc-proposals/pull/281</a><br class=""><div class=""><a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst" target="_blank" class="">https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst</a><br class=""></div><div class=""><br class=""></div><div class="">Let the discussion begin!</div><div class=""><br class=""></div><div class="">-Iavor</div></div>
_______________________________________________<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" target="_blank" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br class=""></div></blockquote></div><br class=""></div></div>_______________________________________________<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>
</blockquote></div>
_______________________________________________<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>
</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=""></body></html>