> Thx. I'm using the Robinson algorithm at present: simple, but not efficient.
> [And it doesn't match equi-recursive terms correctly .. I can't figure out
> a fast way to minimise such a term .. hmmm.. linearise and use a
> string matching algorithm ..?]

I don't know Robinson's algorithm, but the usual way to perform unification
in the presence of cyclic (equi-recursive) terms is to physically unify two
nodes *before* looking at their sub-terms (instead of *after*, or not at all,
in the non-cyclic case). This way, if you run into a cycle and you end up
attempting to unify the same two nodes, you will succeed immediately, provided
your first step is to check for physical equality. I can provide some sample
code if that helps.

That said, type inference in the presence of equi-recursive types is considered
difficult for the user to figure out... many intuitively `meaningless' programs
admit (weird) recursive types.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners