[Camllist] Polymorphic variants
[
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:   (:) 
From:  Andreas Rossberg <rossberg@p...> 
Subject:  Re: [Camllist] How to compare recursive types? 
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 equirecursive > >>>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 higherorder) 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 nonuniform 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 nonempty 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.unisb.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 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