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

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

John Max Skaller wrote:
> 
> >>>If you add lambdas (under recursion) things get MUCH harder. Last time I
> >>>looked the problem of equivalence of such types under the equi-recursive
> >>>interpretation you seem to imply (i.e. recursion is `transparent') was
> >>>believed to be undecidable.
> >>>
> >>In the first instance, the client will have to apply type functions
> >>to create types ..
> >
> >I don't understand what you mean.
> 
> Like C++ tempates.
> 
>     all (x:type) type list = Empty | x * list x;

But that's not the point. You do the same in ML. Still, if you allow
arbitrary (probably higher-order) type declarations of the above form to
be mutually recursive, it is unknown whether you can still decide type
equivalence.

> so the compiler doesn't have to deal directly with the type functions,
> other than to apply them to create instance types.

It has, because reduction of an application of a recursive type function
may yield new redexes. In general, this procedure does not terminate.
Using non-uniform recursion you can create type terms that correspond to
irrational trees.

> >OCaml avoids the problem by requiring uniform recursion for structural
> >types, so that all lambdas can be lifted out of the recursion.
>
> Ah. I see... you don't happen to have any references to online
> material explaining that?

Not really, but the OCaml sources are relatively readable :-)

> .. let me guess, the fixpoints aren't allowed
> inside the lambdas .. ok .. I have a picture of it in my head ..

Not sure what you call "the fixpoints" (in your sources you called the
actual fixpoint construct "Bind" and used "Fix" for recursive refs).

Using the correct terminology the restriction is that lambdas are not
allowed under fixpoints.

> >Still, ordinary graph traversal seems the more appropriate approach to
> >me: represent types as cyclic graphs and check whether the reachable
> >subgraphs are equivalent.
> >
> Yeah .. well .. that's what my algorithm is doing ..
> I just need a better algorithm  :-)

Why not use standard graph algorithms then?

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

Huh? These types ARE equal: they both have the same infinite unrolling.
The rational trees representing them are equal in the theories I know of
- speaking of even or odd does not make any sense for infinite counts.

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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