<div dir="ltr">Well there wasn't really any discussion after my message, to summarize:<div>   * Simon said that he is still on the fence, and would like more input from the rest of the committee,</div><div>   * An you (Joachim) said that you are on the fence, but you think that we should do it because people may use the feature in surprising ways.</div><div><br></div><div>So I am still unconvinced, especially if we don't have a good motivation beyond expecting to be surprised by the users :-)</div><div><br></div><div>As far as I see, the main benefit is the ability to name the type when passing in polymorphic parameters, where the type variable</div><div>does not appear in any of the arguments of to the parameter.</div><div><br></div><div>To me this seems as a rather niche case to warrant a new language construct to make it more convenient.  In addition,</div><div>the notation certainly looks like "big lambda" and I bet there will be some confusion about why it doesn't work as one would expect (yet?).</div><div><br></div><div>So my recommendation would be to shelve this for the moment, and spend some effort to make it behave more like "big lambda",</div><div>which I think would be a potentially useful feature.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Apr 17, 2019 at 12:16 AM Joachim Breitner <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</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">Hi,<br>
<br>
there is lots of fence-sitting here (and I am also on that particular<br>
fence). But to make shake the fence: Let’s do it! I think people will<br>
find good and surprising uses for this feature.<br>
<br>
Iavor, your original message did not carry a concrete recommendation.<br>
Did the discussion help you to form an opinion?<br>
<br>
Cheers,<br>
Joachim<br>
<br>
<br>
Am Donnerstag, den 04.04.2019, 10:10 +0000 schrieb Simon Peyton Jones<br>
via ghc-steering-committee:<br>
> I really am on the fence.   Good things:<br>
>  <br>
> Richard’s first motivating example, where we still need Proxy, is quite convincing.<br>
>  <br>
> It fills out an obvious gap, with the right sort of intro/elim duality with visible type application.<br>
>  <br>
> 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<br>
>  <br>
> f x = Just x<br>
>  <br>
> it is as if you had written<br>
>  <br>
> f :: forall a. a -> Maybe a<br>
> f = \@a \(x::a). Just x<br>
>  <br>
> Less good:<br>
> It’s still incomplete concerning (B) because we can’t talk about dictionary bindings.<br>
> It adds more complexity.<br>
> We are not under real pressure to do this now.<br>
>  <br>
> I’d like to hear from a broader range of opinion.<br>
>  <br>
> Simon<br>
>  <br>
> From: ghc-steering-committee <<a href="mailto:ghc-steering-committee-bounces@haskell.org" target="_blank">ghc-steering-committee-bounces@haskell.org</a>> On Behalf Of Iavor Diatchki<br>
> Sent: 03 April 2019 17:46<br>
> To: Eric Seidel <<a href="mailto:eric@seidel.io" target="_blank">eric@seidel.io</a>><br>
> Cc: ghc-steering-committee <<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a>><br>
> Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas<br>
>  <br>
> Hello,<br>
>  <br>
> 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:<br>
>   1. Eric and Richard seem to be quite keen on the feature<br>
>   2. Simon is on the fence, but likes it because it introduces System F vocabulary to Haskell<br>
>   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.<br>
>  <br>
> Does anyone else have anything else to add?<br>
>  <br>
> -Iavor<br>
>  <br>
>  <br>
>  <br>
> On Tue, Mar 26, 2019 at 6:48 PM Eric Seidel <<a href="mailto:eric@seidel.io" target="_blank">eric@seidel.io</a>> wrote:<br>
> > On Tue, Mar 26, 2019, at 13:17, Iavor Diatchki wrote:<br>
> > > My concern is that the notation certainly suggests that you are binding <br>
> > > types with the @ syntax, but in really it is still the type signature <br>
> > > that guides the binding of the variables and the @ parameters just <br>
> > > duplicate the information from the type signature.<br>
> > <br>
> > 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.<br>
> > <br>
> > 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.<br>
> > <br>
> > Eric<br>
> > _______________________________________________<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>
> <br>
> _______________________________________________<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>
-- <br>
Joachim Breitner<br>
  <a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a><br>
  <a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.de/</a><br>
<br>
_______________________________________________<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>