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

Wed Apr 24 11:59:26 UTC 2019

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
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=02%7C01%7Csimonpj%40microsoft.com%7Cb01f469f49274bc3980108d6c80c9851%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636916353760006580&sdata=0bUACqXPM5OmzQnMNq7A%2Bqx7YCd9e1CS44thT%2B44R9g%3D&reserved=0>
> >
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=02%7C01%7Csimonpj%40microsoft.com%7Cb01f469f49274bc3980108d6c80c9851%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636916353760016579&sdata=isitcg1QKSBFqIhhkqazqSujvX4s4lbYC4HiHhQSxdg%3D&reserved=0>
> --
> Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
> <https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Cb01f469f49274bc3980108d6c80c9851%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636916353760016579&sdata=N2iYGZyHh%2BgieMXW7I4D9odfi6HjqazEfWYpN7nK54g%3D&reserved=0>
>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=02%7C01%7Csimonpj%40microsoft.com%7Cb01f469f49274bc3980108d6c80c9851%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636916353760026570&sdata=MP24WmWJS7qksc0%2FQ0PY8WYSBqeMeAogL9b%2BucV%2FBBU%3D&reserved=0>
>
> _______________________________________________
> 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/20190424/6aae949a/attachment-0001.html>