[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

Thu May 9 18:26:02 UTC 2019

Hello,

we've been contemplating this for a while and the discussion does not
seem to be making significant progress, so I thinking we are probably
ready to make a decision.

It seems that at least a few people on the committee find this feature
useful, and nobody is strongly against, so I'll mark this one as
ACCEPT.

-Iavor

On Wed, Apr 24, 2019 at 4:59 AM Vitaly Bragilevsky <bravit111 at gmail.com> wrote:
>
> Hello,
>
> I actually like this proposal. I see it as a relatively simple (limited, but that's ok) way to express some of System F features in Haskell. By the way, it makes it easier to teach about Haskell to Core translation (I did that several times): we could present it step by step without leaving Haskell while being able to use GHC for checking code. Getting rid of Proxy and providing an alternative to the less-intuitive ScopedTypeVariables extension is a big plus either.
>
> Regards,
> Vitaly
>
> ср, 24 апр. 2019 г. в 01:46, Simon Peyton Jones via ghc-steering-committee <ghc-steering-committee at haskell.org>:
>>
>> I’m puzzled why other members of the committee have not expressed a view.  Would you consider doing so?
>>
>>
>> Simon
>>
>>
>>
>> From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Iavor Diatchki
>> Sent: 23 April 2019 17:56
>> To: Joachim Breitner <mail at joachim-breitner.de>
>> Cc: ghc-steering-committee <ghc-steering-committee at haskell.org>
>> Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas
>>
>>
>>
>> Well there wasn't really any discussion after my message, to summarize:
>>
>>    * Simon said that he is still on the fence, and would like more input from the rest of the committee,
>>
>>    * 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.
>>
>>
>>
>> So I am still unconvinced, especially if we don't have a good motivation beyond expecting to be surprised by the users :-)
>>
>>
>>
>> As far as I see, the main benefit is the ability to name the type when passing in polymorphic parameters, where the type variable
>>
>> does not appear in any of the arguments of to the parameter.
>>
>>
>>
>> To me this seems as a rather niche case to warrant a new language construct to make it more convenient.  In addition,
>>
>> 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?).
>>
>>
>>
>> So my recommendation would be to shelve this for the moment, and spend some effort to make it behave more like "big lambda",
>>
>> which I think would be a potentially useful feature.
>>
>>
>>
>> -Iavor
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> On Wed, Apr 17, 2019 at 12:16 AM Joachim Breitner <mail at joachim-breitner.de> wrote:
>>
>> Hi,
>>
>> there is lots of fence-sitting here (and I am also on that particular
>> fence). But to make shake the fence: Let’s do it! I think people will
>> find good and surprising uses for this feature.
>>
>> Iavor, your original message did not carry a concrete recommendation.
>> Did the discussion help you to form an opinion?
>>
>> Cheers,
>> Joachim
>>
>>
>> Am Donnerstag, den 04.04.2019, 10:10 +0000 schrieb Simon Peyton Jones
>> via ghc-steering-committee:
>> > 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 at haskell.org> On Behalf Of Iavor Diatchki
>> > Sent: 03 April 2019 17:46
>> > To: Eric Seidel <eric at seidel.io>
>> > Cc: ghc-steering-committee <ghc-steering-committee at 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 at 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 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
>> --
>> Joachim Breitner
>>   mail at joachim-breitner.de
>>   http://www.joachim-breitner.de/
>>
>> _______________________________________________
>> 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