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

[Eric Seidel]

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 
> <iavor.diatchki at gmail.com> wrote:
> > Hello,
> > 
> > let's get the discussion going about proposal #155 (https://github.com/goldfirere/ghc-proposals/blob/type-lambda/proposals/0000-type-lambda.rst).
> > 
> > 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 at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>