I really am on the fence.   Good things:

• Richard’s first motivating example, where we still need Proxy, is quite convincing.

• It fills out an obvious gap, with the right sort of intro/elim duality with visible type application.

• And I like that it gives us a language in which to talk about System F elaboration of the program, if and when we want to.  E.g. we can say: if you write

f x = Just x

it is as if you had written

f :: forall a. a -> Maybe a

f = \@a \(x::a). Just x

Less good:

• It’s still incomplete concerning (B) because we can’t talk about dictionary bindings.
• It adds more complexity.
• We are not under real pressure to do this now.

I’d like to hear from a broader range of opinion.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces@haskell.org> On Behalf Of Iavor Diatchki
Sent: 03 April 2019 17:46
To: Eric Seidel <eric@seidel.io>
Cc: ghc-steering-committee <ghc-steering-committee@haskell.org>
Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

Hello,

perhaps it is time to come up with some sort of decision here.  Based on the replies to this thread we seem to have the following opinions:

  1. Eric and Richard seem to be quite keen on the feature

  2. Simon is on the fence, but likes it because it introduces System F vocabulary to Haskell

  3. I am skeptical of the proposal as is, as I think it adds additional complexity to the language (more non-orthogonal features) without significant payoff.

Does anyone else have anything else to add?

-Iavor

On Tue, Mar 26, 2019 at 6:48 PM Eric Seidel <eric@seidel.io> wrote:

On Tue, Mar 26, 2019, at 13:17, Iavor Diatchki wrote:
> My concern is that the notation certainly suggests that you are binding
> types with the @ syntax, but in really it is still the type signature
> that guides the binding of the variables and the @ parameters just
> duplicate the information from the type signature.

But you are binding types with the @ syntax. The proposal gives a number of examples where the @-bound type variable is bound by a different name (or not at all) in the type signature. Many are contrived, to demonstrate where the binders are allowed, but the higher-rank and proxy-eliding examples look compelling to me.

We also already allow repeated value binders in Haskell. When I write a function in equational style, I have to rebind each argument in each alternate equation. Sometimes this is noisy and I'll prefer a single equation with an explicit `case`. But for functions where the body is sizable, I find the repeated binders to be quite helpful because the scopes are smaller. I can easily see the same benefit applying to type binders. Ultimately, I think this comes down to a matter of style, and I favor letting Haskell programmers pick the style that works best for them.

Eric
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee