From: Job Vranish
Sorry for bringing back an ancient thread but I'd still like to understand this
better.
It is still not obvious to me why typechecking infinite types is so hard. Is determining type 'equivalence' the hard part? or is that a separate issue?
Typechecking with regular types isn't hard. The problem is, the type system is almost useless for catching bad programs. Every closed lambda expression is typeable if infinite types are allowed. Usually systems add some sort of ad-hoc restriction on regular types, like requiring that all all cycles pass through a record type.
The algorithm works like this: Given two types a and b: unify a with b, if the resulting type is 'equivalent' to the original a, then b must be (I think) at least as general as a.
To determine equivalence, I start with the head of both types (which are represented as graphs) and check to see if the constructors are the same. If they are then I set those two nodes 'equal' and recurse with the children. It's a 'destructive' algorithm that effectively 'zips' the two graphs together.
It returns false if it encounters two constructors that are different.
I have also found that destructive graph-based unification is the easiest way to work with recursive types. Brandon