Scoped type variables

[Olaf Chitil]

Sorry, but I cannot resist to mention an alternative language construct 
to scoped type variables which gives you the same power of annotating 
any subexpression with type information. I did mention it in my ICFP 
2001 paper on Compositional Explanations of Types as a side note.

The nice property of this language construct is that all type variables 
scope only over a single type; you never have to look if the same type 
variable appears somewhere else far away in your program.

The idea is that a type may contain part of a type environment (so 
actually it is no longer a type but a typing). This typ environment 
constructs the relation to other types.

Instead of

f :: forall a. [a] -> ...
f xs = ...
  where
  g :: a -> [a]
  g x = x:xs

you write

f :: [a] -> ...
f xs = ...
  where
  g :: (xs::[b]) => b -> [b]
  g x = x:xs

So (xs::[b]) is this new type environment that is part of the type of g. 
Whether you want to write it similar to a class context, is a matter of 
taste.

This extended type (typing) is the principal monomorphic typing for the 
function g. Every subexpression has a principal monomorphic typing and 
hence you can annotate any expression with a typing. Type variables 
always scope only over a typing.

This system of typings works fine for the Hindley-Milner system and also 
for Haskell 98 classes. I have to admit that I never looked beyond; so I 
don't know which problems may crop up for rank-n, existentials etc.

Ciao,
Olaf