[Haskell-cafe] Re: Lexically scoped type variables

[apfelmus at quantentunnel.de]

I think the problem comes from the fact that

    let (x :: a) = rhs in expr

has two interpretations: either the programmer mainly specifies a
judgment (\Gamma |- rhs :: a) (f.i. as a guide for type inference) or he
just introduces a new variable and sees let as a sugar for

    (\(x :: a) -> expr) rhs

with the viewpoint that the program is a huge expression and all
top-level declarations are just (somewhat superflous) lambdas which lead
to a final goal.


In both cases, one would assume that the main variable binder is our
good old lambda. Thus, the (::) in (\(x::a) -> ..) behaves like a
constructor and the type variable on the right hand side is just a pattern:
    f (x :: [a]) = ...
is not any different from
    f (Cons x [a]) = ...
When f is applied to an argument, it's the type checker that performs
"pattern matching". Of course, one needs nonlinear "type patterns":
    (f :: a -> b) $ (x :: a) = f x
So the type variables in lambdas behaves like normal variables and
things like
    g :: Int -> Int
    g (x :: a) = x + 1 :: a
are entirely fine. All in all, type variables in lambdas are real variables.


The first interpretation of let amounts to the Haskell98 intuition: the code

    x :: a -> a
    x = rhs

means a judgment that x has type (forall . a -> a). This also means that
this does not bring any new type variables in scope, only lambdas are
capable of introducing new variables. GHC 6.6 rules are not compatible
with that. They somehow admit variable bindings by judgments only to
discover that this doesn't work for existential types.

But note that we have (x :: ...) and (x=...) as separate statements, and
we may well keep the second interpretation:

   f :: Int -> Int
   (f :: a -> a) =
       \x -> (x+1 :: a)

The intuition is that stand-alone statements (x :: ...) are exactly what
they look like: judgments for the type system. The only odd thing about
them is that they are stand-alone and do not add to the "main program
expression".

IMHO, the most natural thing would be that type judgments appear on the
rhs of a let or a lambda and that type variable bindings appear on the
lhs of a let or a lambda. In the definition of f above, (f :: Int ->
Int) and (x+1 :: a) are judgments and (f :: a -> a) is a variable
binding. Any confusion between judgment and binding is just like a
confusion between constructor application and pattern.

Regards,
apfelmus