[Caml-list] equi-recursive Fold isomorphism

[John Max Skaller <skaller@ozemail.com.au>]

Given a recursive type

    Fix 'a .  T  (where 'a occurs in T)

we can unfold the type to T' = T['a -> Fix 'a.T],
we define unfold t = t, if t doesn't start with a fixpoint operator.

Any ideas how to best implement fold, the inverse isomorphism?

Brute force method: examine every subterm, and compare with
the main term using equi-recusive comparison .. this seems quadratic
in the number of nodes .. smarter method: only compare arguments
of fixpoint binders .. can we do any better? For example,
replace the subterm in the main term with a fixpoint variable, and compare
the subterm with the modified main term (directly, ie. using ocaml 
'compare')
[I don't know how to do this 'replacement' efficiently though]

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850



-------------------
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