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

Thu May 9 21:44:14 UTC 2019

This proposal is more than a simple syntactic tweak like extra-commas or where to place 'qualified'.  For those things both costs and benefits are small; there are judgements of taste but I can live with any outcome.

Far at the other end of the spectrum is something like linear types: a big, expensive, pervasive change -- but one that is part of Haskell's goal of being a laboratory for growing cool ideas, and one from which we will, I hope, learn a lot.

This proposal is in the middle.  It's "filling out the envelope" of the system we now have, as are many other proposals on table at the moment, trying to make the language we have as consistent, predictable and coherent as possible.

So I like the fact that this proposal lets us write the System F terms that Haskell elaborates too.  It gives us a language in which to explain to our users a model of what is "really happening", and what the type inference system fills in.  I like that it gives the lambda part of visible type application (we should call it "visible type abstraction" perhaps!).

But it does add yet another piece to our language; and it's a piece that few people really need.  While there is no substantial opposition, support is pretty muted.  I'd really be more comfortable if there were lots of people saying "yes we really want this". 

On balance I'm happy to support Iavor's "accept" proposal.  But only just!

Simon

| -----Original Message-----
| From: Iavor Diatchki <iavor.diatchki at gmail.com>
| Sent: 09 May 2019 19:26
| To: Vitaly Bragilevsky <bravit111 at gmail.com>
| Cc: Simon Peyton Jones <simonpj at microsoft.com>; Joachim Breitner
| <mail at joachim-breitner.de>; ghc-steering-committee <ghc-steering-
| committee at haskell.org>
| Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in
| Labmdas
| 
| 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2
| >> > > Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-c
| >> > > ommittee&data=01%7C01%7Csimonpj%40microsoft.com%7Cf6979d8c314
| >> > > b47c1133c08d6d4abd337%7C72f988bf86f141af91ab2d7cd011db47%7C1&
| >> > > sdata=UFzBeDE2vfeqnbJYpXHG%2FbnM2PJsYOLiqFlVuSYELcg%3D&reserv
| >> > > ed=0
| >> >
| >> > _______________________________________________
| >> > ghc-steering-committee mailing list
| >> > ghc-steering-committee at haskell.org
| >> > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fm
| >> > ail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-commi
| >> > ttee&data=01%7C01%7Csimonpj%40microsoft.com%7Cf6979d8c314b47c11
| >> > 33c08d6d4abd337%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=UF
| >> > zBeDE2vfeqnbJYpXHG%2FbnM2PJsYOLiqFlVuSYELcg%3D&reserved=0
| >> --
| >> Joachim Breitner
| >>   mail at joachim-breitner.de
| >>
| >> https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.
| >> joachim-breitner.de%2F&data=01%7C01%7Csimonpj%40microsoft.com%7Cf
| >> 6979d8c314b47c1133c08d6d4abd337%7C72f988bf86f141af91ab2d7cd011db47%7C
| >> 1&sdata=Spw%2F2dNnY8edtps1c3uBA4fTRybn0dCtvqQkoKiX8eQ%3D&rese
| >> rved=0
| >>
| >> _______________________________________________
| >> ghc-steering-committee mailing list
| >> ghc-steering-committee at haskell.org
| >> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmai
| >> l.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee
| >> &data=01%7C01%7Csimonpj%40microsoft.com%7Cf6979d8c314b47c1133c08d
| >> 6d4abd337%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=UFzBeDE2vf
| >> eqnbJYpXHG%2FbnM2PJsYOLiqFlVuSYELcg%3D&reserved=0
| >>
| >> _______________________________________________
| >> ghc-steering-committee mailing list
| >> ghc-steering-committee at haskell.org
| >> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmai
| >> l.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee
| >> &data=01%7C01%7Csimonpj%40microsoft.com%7Cf6979d8c314b47c1133c08d
| >> 6d4abd337%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=UFzBeDE2vf
| >> eqnbJYpXHG%2FbnM2PJsYOLiqFlVuSYELcg%3D&reserved=0