Sean Seefried wrote:
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?
I haven't heard the term "eigen-variable" for this before. It makes
great sense in German, from the little I know, but in english it's
mostly a linear algebra term.
The term I've heard is "skolem constant", which is a freshly invented
thing distinct from everything else. I think it's pretty standard usage.
At the very least, that's what Simon Peyton-Jones' uses in his papers on
typechecking Haskell.
A quick summary of the idea is that to check if a term has a quantified
type like forall a . (a -> a), you can invent a new type constant
distinct from everything else in the system, maybe something printed
like A231, and then typecheck the term as if it had the concrete type
A231 -> A231. If it typechecks like that, then you know the code doesn't
require any assumptions about ustated properties of a or its relation to
other types, so it actually does work as forall a . (a -> a).
If the quantifier has a class constraint on it, I think the skolem
constant gets an imaginary instance, for the purpose of typechecking.
Brandon
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
