Dominic Steinitz wrote:
Can someone give an explanation of how the marks get built up?
Suppose we have a class TypeEq a b so that the constraint TypeEq holds
whenever a and b are the same. Then the type Int and the type
TypeEq a Int => a
are kind of equivalent, right? The HList library plays many tricks
like that. The idea is that we can replace a definite type with a type
variable subject to some constraint (which we can fix later on).
In some respects, constraints are more convenient: they float, their
order does not matter, their duplicates are automatically
eliminated. Just what we need to build a set...
It ``follows'' then that instead of building the union of types, we
can build the union of constraints. The latter operation is trivial:
the typechecker does that all the time. If we restrict the scope of
the type variable by quantification, the scope of the corresponding
constraint is likewise restricted. The quantification also builds
eigen-variables (which are distinct from anything else) -- so we get
'gensym' on the type level for free. That is all there is to it...
Olge, I found this explanation really useful. I was wondering if you
could explain to me what you mean by eigen-variable though?
Sean
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
