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