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

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