>From: Job Vranish <[email protected]>
>
>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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
