Re: [Caml-list] How to compare recursive types?

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

Argg.. my algorithm is wrong. Here is a counterexample:

typedef x = x * int;
typedef y = (y * int) * int;

If you just unroll these types for a while, they look equal,
but they aren't: in fact y might be considered a subtype of x.
Type x is any cyclic list of n>0 ints.
Type y is any non-empty cyclic list of an *even* number of ints.
Y might be represented in C using

struct y {
  y *next;
  int first;
  int second;
};

Now I *really* need a proper algorithm ..

Felix is extensional: in a product, we normally expand
types, but we can't do that if the type is recursive.

A pointer must be used not only at the fix point,
but at any possible fixpoint of an equivalent
definition...so any strongly connected components
have to be refered to by a pointer I think .. this
would solve the representation problem above
(at least in this case) but the fact remains
that the types above are not equal.

A similar example:

x2 = x * int;
x3 = x2 * int;
...

shows how to construct a type holding 'at least'
a certain number of ints... and my algorithm
also fails to distinguish these types.
Here., the representations would be different ..
there is no recursion in the 'top' part of the type,
so an expanded struct would be used ..

Hmmm.. does it show one type is a subtype
of the other .. hmmm .. perhaps it shows that
there exists a type  which both types are
subtypes of .. that sounds right ..


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