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

[Spiwack, Arnaud]

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/20201013/b437be3f/attachment.html>