[ghc-steering-committee] Please review #281: Visible 'forall' in types of terms

Thu Oct 15 15:54:52 UTC 2020

Yes, I think this proposal meets the criteria of "needs revision" -- if at least to clarify all the points that have been raised.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20201015/3999ca95/attachment-0001.html>