In the end, this proposal does not bring in much over ScopedTypeVariables So the gain is relatively small. But the pain is real: more complexity, and that's a long-term cost. Actually the biggest reason I like this proposal is because it takes another step in the direction of directly expressing System F in Haskell. Not so much because I expect to use it a lot but because it gives a vocabulary in which to express what a lot of the implicit elaboration in GHC is doing. I use VTA in this way already. But I'm a bit on the fence overall. With finite effort cycles, we may have more important fish to fry. Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 21 February 2019 18:55 To: Iavor Diatchki Cc: ghc-steering-committee Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas On Feb 19, 2019, at 2:01 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: After a bit more thought, I am not sure what do we get with this notation over ScopedTypeVariables. In particular, here are some things that came up as I was trying to write a couple of examples: 1. The order in which variables are introduced is not clear---presumably it is some sort of left to write ordering based on the type signature. For example: f1 :: (a,b) -> a -- first type param is `a`? f2 :: Ord b => a -> b -> a -- first type param is `b`? type T a b = (b,a) f3 :: T a b -> a -- first type param is? This approach seems quite fragile. This problem first came up (in earnest) in the context of type applications. We now specify the answer in the manual; see the first two bullet-points here: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...https://nam06.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23visible-type-application&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241748539&sdata=YJlqlHlyNlvU7%2FUxxo%2B6E7KhVJik8rGtCGIQGDgj%2FXQ%3D&reserved=0 These points have actually been refined in HEAD. You can view the documentation source here: https://github.com/ghc/ghc/blob/master/docs/users_guide/glasgow_exts.rst#L10...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc%2Fghc%2Fblob%2Fmaster%2Fdocs%2Fusers_guide%2Fglasgow_exts.rst%23L10800&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241748539&sdata=ABm0BqcXoGe5vVfErATx3OehD9LKeojxFM8PxCqOGWI%3D&reserved=0 In answer to your examples: f1: a, b f2: b, a f3: a, b 2. The proposal says that a problem with the `forall` in ScopedTypeVariables is that the signature can be arbitrarily far away from the implementation. I agree that this is a problem, but it seems to remain a problem with this proposal, as you have to look at the signature to see in what order you should write the parameters. Good point. 3. There are some things that you can write with the `forall` notation, that you cannot write using this notation. For example: f3 :: forall a. Bool f3 = null ([] :: [a]) Clearly this example is a bit contrived, but still it illustrates a problem. You can still write `f3 @a = null ([] :: [a])`. As is, I am not sure what we are getting over ScopedTypeVariables. Am I missing something here? While not highlighted in the proposal, the example named `ex` binds a type variable using the new notation that would be very awkward indeed without this extension. Here is the example: higherRank :: (forall a. a -> a -> a) -> ... higherRank = ... ex = higherRank (\ @a x _y -> (x :: a)) The alternative would be to write ex = higherRank ((\ x _y -> (x :: a)) :: forall a. a -> a -> a) just to bring the `a` into scope. In the end, this proposal does not bring in much over ScopedTypeVariables -- it just makes the type-variable scoping mechanism more in line with the term-variable scoping mechanism. There's nothing fundamentally new here: just convenience. You may also want to see https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-4594301...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F155%23issuecomment-459430140&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241758532&sdata=MxZcEwLwkUzM%2B7OgHidINCiC1rNnaYj8nFmnWcpz%2F5E%3D&reserved=0 and https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-4603336...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F155%23issuecomment-460333687&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241758532&sdata=FmRe9%2Ftd7qvXd314pAjNj%2BUX2AVAMvXtP22z57PlxZk%3D&reserved=0 which outline use-cases that would benefit from this new treatment. Thanks, Richard -Iavor On Tue, Feb 19, 2019 at 10:28 AM Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, let's get the discussion going about proposal #155 (https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Ftype-lambda%2Fproposals%2F0000-type-lambda.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C3a5fe98204cf4fe7430d08d6982e2211%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636863721241768529&sdata=azmQaoLX50D7UNWnXdpX4Vu%2Fu7MYwqTXyhu8ikSoP%2B0%3D&reserved=0). Summary: the idea is pretty simple: allow functions to name their type arguments explicitly, so that they can be used in type signatures within the function's definition. The notation for a type argument is `@a`, and such type arguments can be used only when functions have an explicit type signature (technically, when GHC is doing "checking" rather then "inference"). This proposal provides an alternative to "ScopedTypeVariables" to refer to type parameters, which I think is a step in the right direction, as using the `forall` to introduce type variables always felt a bit hacky to me (now, there's a technical argument :) I am a bit concerned with the notation though: in other places where we use `@a`, (e.g., #126 type application in patterns, and TypeApplications) the `a` is a type, while in this use it must be a variable. I wonder if this punning might be confusing. I don't really have an alternative suggestion though. What does everyone else thing? -Iavor _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hello, my concern is mainly with introducing multiple language constructs that do almost the same thing and neither is better than the other as I think this complicates the language unnecessarily. Vladislav, I am not sure of the details of your example, but isn't it the case that you could write it with scoped type variables if you wrote the type down? I agree that this can be a pain, and as far as I see, this is the main use case for this feature---it provides an easier way to call higher-rank functions, when you need to refer to the type parameter in the polymorphic argument. -Iavor On Fri, Feb 22, 2019 at 2:48 AM Vladislav Zavialov wrote:

Dear GHC steering committee,

...

In the end, this proposal does not bring in much over ScopedTypeVariables

Please note that comparing this feature to ScopedTypeVariables does not capture the full picture. There are two examples of code in the proposal, which I provided, that cannot be expressed using ScopedTypeVariables without a dummy Proxy argument.

...

With finite effort cycles, we may have more important fish to fry.

I was planning to implement this proposal if it would be accepted.

All the best, - Vladislav

Hello, I assume the arguments to `reify` are meant to be the other way around? Here is the ScopedTypeVariables version I thought should work but indeed it doesn't, although I don't fully understand why. Is it because GHC instantiates `val` and then tries to generalize again, but fails since the polymorphic argument to `reify` is very ambiguous? And is this the intended behavior? {-# Language ScopedTypeVariables #-} {-# Language RankNTypes #-} {-# Language TypeApplications #-} {-# Language MultiParamTypeClasses #-} {-# Language FlexibleContexts #-} {-# Language AllowAmbiguousTypes #-} class Reifies s a reify :: forall a r. a -> (forall s. Reifies s a => r) -> r reify _ _ = undefined reflect :: forall s a. Reifies s a => a reflect = undefined example = reify 5 val where val :: forall s. Reifies s Integer => Integer val = reflect @s + reflect @s On Fri, Feb 22, 2019 at 9:55 AM Vladislav Zavialov wrote:

...

isn't it the case that you could write it with scoped type variables if you wrote the type down?

I don't think so, the type does not necessarily mention the type variables. For example, imagine we removed Proxy from reflection:

reify :: forall a r. a -> (forall s. Reifies s a => r) -> r reflect :: forall s a. Reifies s a => a

Under this proposal, I would be able to write

x = reify (\ @s -> reflect @s + reflect @s) (5 :: Integer)

Here, x = 10 :: Integer.

ScopedTypeVariables require extra Proxy arguments to express this, which are not only an inconvenience, but also extra data passed at runtime. Same reasoning applies to other higher-rank situations, including my other example with CPS-d proofs.

All the best, - Vladislav

1. Should we allow binding type variables that are not explicitly quantified with a forall? I'm concerned about the potential for breaking code should GHC's rules for ordering quantifiers change. Does GHC already guarantee a particular ordering? See my commentshttps://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-4692418... on GitHub. 2. I wonder if supporting type binders in inference mode is as hard as the proposal fears. I think it’s hard. f @a x = x we could infer any of. f :: forall a b. b -> b f :: forall a. a -> a f :: forall b a. b -> b Roughly, it’s as hard as figuring out impredicative polymorphism I think. Let’s not go there 😊. Simon -----Original Message----- From: ghc-steering-committee On Behalf Of Eric Seidel Sent: 04 March 2019 01:44 To: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas One argument in favor of the proposal that I don't believe I've seen mentioned is that, now that we can explicitly apply types with the @ syntax, it feels very intuitive to also bind them with the same syntax. So even if this proposal does not add much technically over ScopedTypeVariables, I think it's still a good idea. I do have a couple of questions/comments though: 1. Should we allow binding type variables that are not explicitly quantified with a forall? I'm concerned about the potential for breaking code should GHC's rules for ordering quantifiers change. Does GHC already guarantee a particular ordering? Would we want to? 2. I wonder if supporting type binders in inference mode is as hard as the proposal fears. The alternatives section mentions the possibility of extracting a partial type signature from the LHS, but I had a simpler thought. Why not say that `\ @a -> body` infers the type `forall a. ty` where `body :: ty`, and let unification handle the rest? It seems like that would handle all of the variants of `null` in section 7, though not the example in section 3 with the equality constraint. But to be honest, I'd be ok with rejecting that program. It would be much clearer with a single type binder. I don't think the lack of a solution for type binders in inference mode should block this proposal, but it would be much nicer if we had one! I don't want Haskell programmers to have to learn the intricacies of bidirectional type checking to use what is otherwise a very intuitive feature. Eric On Tue, Feb 19, 2019, at 14:01, Iavor Diatchki wrote:

After a bit more thought, I am not sure what do we get with this

notation over ScopedTypeVariables. In particular, here are some things

that came up as I was trying to write a couple of examples:

1. The order in which variables are introduced is not

clear---presumably it is some sort of left to write ordering based on

the type signature. For example:

f1 :: (a,b) -> a -- first type param is `a`?

f2 :: Ord b => a -> b -> a -- first type param is `b`?

type T a b = (b,a)

f3 :: T a b -> a -- first type param is?

This approach seems quite fragile.

2. The proposal says that a problem with the `forall` in

ScopedTypeVariables is that the signature can be arbitrarily far away

from the implementation. I agree that this is a problem, but it seems

to remain a problem with this proposal, as you have to look at the

signature to see in what order you should write the parameters.

3. There are some things that you can write with the `forall`

notation, that you cannot write using this notation. For example:

f3 :: forall a. Bool

f3 = null ([] :: [a])

Clearly this example is a bit contrived, but still it illustrates a problem.

As is, I am not sure what we are getting over ScopedTypeVariables. Am

I missing something here?

-Iavor

On Tue, Feb 19, 2019 at 10:28 AM Iavor Diatchki

mailto:iavor.diatchki@gmail.com> wrote:

...

Hello,

...

...

let's get the discussion going about proposal #155 (https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-...).

...

...

Summary:

...

the idea is pretty simple: allow functions to name their type arguments explicitly, so that they can be used in type signatures within the function's definition. The notation for a type argument is `@a`, and such type arguments can be used only when functions have an explicit type signature (technically, when GHC is doing "checking" rather then "inference").

...

...

This proposal provides an alternative to "ScopedTypeVariables" to

...

refer to type parameters, which I think is a step in the right

...

direction, as using the `forall` to introduce type variables always

...

felt a bit hacky to me (now, there's a technical argument :)

...

...

I am a bit concerned with the notation though: in other places where we use `@a`, (e.g., #126 type application in patterns, and TypeApplications) the `a` is a type, while in this use it must be a variable. I wonder if this punning might be confusing. I don't really have an alternative suggestion though.

...

...

What does everyone else thing?

...

...

-Iavor

_______________________________________________

ghc-steering-committee mailing list

ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ

ee

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

Hello,

2. I wonder if supporting type binders in inference mode is as hard as

...

the proposal fears.

I think it’s hard.

f @a x = x

we could infer any of.

f :: forall a b. b -> b

f :: forall a. a -> a

f :: forall b a. b -> b

I don't know how we'd infer the 2nd option, even though that's surely what was intended. There's simply no link between the `a` and `x` in the code. So I'd expect GHC to infer either the 1st or 3rd type, and emit a warning about the unused type abstraction similar to the existing warnings about unused variables or unused foralls. Does the order of tyvars matter here? Doesn't seem so, as `b` should be marked inferred, and thus ineligible for VTA.

Like Eric, I would expect that the type of `f` should be something like (1) or (3), except that the inferred polymorphic variables should not be visible (i.e., you shouldn't be able to explicitly apply them), in which case (1) and (3) are essentially the same: f :: forall a {b}. b -> b -Iavor

I haven't thought through the consequences of this fully, but it does seem plausible. It says we must generalise over some ‘a’, but which ‘a’? What type does (\@a (\x. x)) have? I suppose you could say (forall b. (forall a. b -> b)), but presumably it could equally well have the type (forall a. a->a). I think I can see an algorithm. But someone would need to write down a type system. (I think I was probably was wrong to mutter about impredicativity.) Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 05 March 2019 03:06 To: Eric Seidel Cc: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas On Mar 3, 2019, at 8:44 PM, Eric Seidel mailto:eric@seidel.io> wrote: Why not say that `\ @a -> body` infers the type `forall a. ty` where `body :: ty`, and let unification handle the rest? That's intriguingly simple. I haven't thought through the consequences of this fully, but it does seem plausible. I'm not ready to commit to that, but after a few minutes' focused thought, I can't see any problems with it. In any case, the proposal as written is forward-compatible with such a change, as doing what you say will allow only more programs: ones accepted by the proposal will remain accepted and with the same meanings. Richard

On Tue, Mar 5, 2019, at 16:19, Richard Eisenberg wrote:

...

On Mar 5, 2019, at 11:34 AM, Simon Peyton Jones wrote:

I haven't thought through the consequences of this fully, but it does seem plausible. It says we must generalise over some ‘a’, but *which* ‘a’? What type does (\@a (\x. x)) have?

My understanding of Eric's idea is that GHC would give (\x.x) the type (alpha -> alpha), as usual. Then (\ @a (\x.x)) gets the type forall a. alpha -> alpha. Later, we might solve for alpha or generalize over it, perhaps leading a type like forall b a. b -> b.

Yep, that's precisely what I would expect. It doesn't need to happen for this proposal, but it would make a very nice addition assuming the theory works out.

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

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 On Behalf Of Iavor Diatchki Sent: 03 April 2019 17:46 To: Eric Seidel Cc: ghc-steering-committee 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 mailto: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.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committeehttps://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%7C8371ed497872442e7ba708d6b853dea8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636899067690452644&sdata=uPf6eWyl9bxDxwsVqC%2FxB%2FqtVXwCEz2WP5LAHsURB3I%3D&reserved=0

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 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

...

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 On Behalf Of Iavor Diatchki Sent: 03 April 2019 17:46 To: Eric Seidel Cc: ghc-steering-committee 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

...

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 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

Am Donnerstag, den 04.04.2019, 10:10 +0000 schrieb Simon Peyton Jones via ghc-steering-committee: the replies to this thread we seem to have the following opinions: 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

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

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

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@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 *On Behalf Of *Iavor Diatchki *Sent:* 23 April 2019 17:56 *To:* Joachim Breitner *Cc:* ghc-steering-committee *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@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

...

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 On Behalf Of Iavor Diatchki Sent: 03 April 2019 17:46 To: Eric Seidel Cc: ghc-steering-committee 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

...

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 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

Am Donnerstag, den 04.04.2019, 10:10 +0000 schrieb Simon Peyton Jones via ghc-steering-committee: the replies to this thread we seem to have the following opinions: 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 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@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@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@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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

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 | Sent: 09 May 2019 19:26 | To: Vitaly Bragilevsky | Cc: Simon Peyton Jones ; Joachim Breitner | ; ghc-steering-committee | 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 | 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 : | >> | >> I’m puzzled why other members of the committee have not expressed a | view. Would you consider doing so? | >> | >> | >> Simon | >> | >> | >> | >> From: ghc-steering-committee | >> On Behalf Of Iavor | >> Diatchki | >> Sent: 23 April 2019 17:56 | >> To: Joachim Breitner | >> Cc: ghc-steering-committee | >> 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 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 | >> > On Behalf Of Iavor | >> > Diatchki | >> > Sent: 03 April 2019 17:46 | >> > To: Eric Seidel | >> > Cc: ghc-steering-committee | >> > 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 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://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@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@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@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@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