[Camllist] equirecursive Fold isomorphism
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20020728 (20:15) 
From:  Alain Frisch <frisch@c...> 
Subject:  Re: [Camllist] equirecursive Fold isomorphism 
On Sun, 28 Jul 2002, John Max Skaller wrote: > Hmmm: Ocaml 3.04+15 with rectypes > > > # let rec x = (1,(1,(1,x)));; > val x : int * (int * (int * 'a)) as 'a = > .... > > Seem like Ocaml doesn't minimise the type, but: > > > let rec y = (1,y);; > > x = y;; > > Works correctly (so it knows the two types are comparable). > Interestingly, the answer is false Are you sure ? It seems that the comparison doesn't terminate, as expected (as it does not consume memory). The manual says: << Equality between cyclic data structures may not terminate. >> : both data structures > consist of an infinite stream of 1's, represented by > cycles of distinct lengths. No item by item comparison > could reveal any distinction: the infinite tree expansions > of the data structures are the same. Is Ocaml's answer correct? As you know, to implement the comparison between cyclic values with the expected behaviour, one has to use a coinductive algorithm with some kind of memoization. This would be much slower for the noncyclic case, and many people expect a fast generic compare function. I would like to say that you can always take the code in byterun/compare.c and implement your own equirecursive generic comparison in C, but this is actually not possible (you need the Is_young and Is_in_heap macros that are not available). Using the mentioned Recurse module, you could do: module I = struct type 'a t = Int of int  Pair of 'a * 'a let map f = function  Int i > Int i  Pair (a,b) > Pair (f a, f b) let equal f x y = match (x,y) with  (Int i, Int j) when i = j > ()  (Pair (a1,b1), Pair (a2,b2)) > f a1 a2; f b1 b2  _ > raise Recursive.NotEqual let iter f x = ignore (map f x) let hash f x = Hashtbl.hash (map f x) let deep = 4 end module X = Recursive.Make(I) let cons x = let n = X.make () in X.define n x; n let recurs f = let n = X.make () in X.define n (f n); n let int' i = I.Int i let int i = cons (int' i) let pair' a b = I.Pair (a,b) let pair a b = cons (pair' a b) let x = recurs (fun x > pair' (int 1) (pair (int 1) (pair (int 1) x))) let y = recurs (fun y > pair' (int 1) y) let x = X.internalize x and y = X.internalize y let () = Printf.printf "%i;%i;%b\n" (X.id x) (X.id y) (x = y) (the equility test is specified by Recurse to run in constant time) Sidenote: be careful if you implement a language with subtyping and both recursive types and recursive (cyclic) values. Indeed, the usual equirecursive definition of subtyping is not sound if you allow cyclic values. For instance, the algorithm would say that the type ('a * 'a) as 'a is empty, even though it is inhabited by values.  Alain  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners