Scoped type variables
Olaf Chitil
O.Chitil at kent.ac.uk
Wed Feb 8 16:51:37 EST 2006
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
More information about the Haskell-prime
mailing list