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

[Iavor Diatchki]

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>
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
> .
>
> 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>
> 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> 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> 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>
>>>> 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/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
>>>> 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
>>>>
>>> _______________________________________________
>> 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/b9fd5e11/attachment.html>