Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] equi-recursive Fold isomorphism
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: John Max Skaller <skaller@o...>
Subject: [Caml-list] equi-recursive Fold isomorphism
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 
[I don't know how to do this 'replacement' efficiently though]

John Max Skaller,
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: