<div dir="ltr"><div>I agree with Arnaud's observations.</div><div><br></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>Thoughts?<br><div><div><br><div>-Iavor</div></div></div></div></div><br><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">arnaud.spiwack@tweag.io</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"><div dir="ltr"><div>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">https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-707033510</a> .</div><div><br></div><div>But I wanted to point out that there are really two, interlocked, yet distinct, parts in this proposal.</div><div>1. Having a `forall a ->` construct for types of terms</div><div>2. How is `f blah` parsed if `f` has type `forall a -> …`?</div><div><br></div><div>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></div><div><br></div><div>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><br></div><div>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><br></div><div>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><br></div><div>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><br></div><div>/Arnaud<br></div></div><br><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">iavor.diatchki@gmail.com</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"><div dir="ltr">I've been following the discussion and I think we should keep it in the "committee review" phase because<div> 1. The discussion is due to questions from the committee members, and </div><div> 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><br></div><div>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><br></div><div>Let me know,</div><div>-Iavor</div><div><br></div></div><br><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">marlowsd@gmail.com</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"><div dir="ltr">There seems to have been a lot of ensuing discussion on this one, should it go back into the discussion phase?<br></div><br><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">rae@richarde.dev</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"><div>I'm in support of this proposal, but I've pushed back on a few softer points. I've commented on GitHub.<div><br></div><div>Richard<br><div><br><blockquote type="cite"><div>On Oct 1, 2020, at 1:07 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>> wrote:</div><br><div><div dir="ltr"><div>Hello,</div><div><br></div><div>Proposal #281 is ready for review by the committee. My recommendation is to accept it, I've</div><div>written a summary of my understanding to the proposal and my recommendation on the GitHub</div><div>thread, accessible through these links:</div><div><br></div><a href="https://github.com/ghc-proposals/ghc-proposals/pull/281" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281</a><br><div><a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst" target="_blank">https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst</a><br></div><div><br></div><div>Let the discussion begin!</div><div><br></div><div>-Iavor</div></div>
_______________________________________________<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" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br></div></blockquote></div><br></div></div>_______________________________________________<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>
</blockquote></div>
_______________________________________________<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>
</blockquote></div>