[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:  20020424 (15:03) 
From:  Andreas Rossberg <rossberg@p...> 
Subject:  Re: [Camllist] How to compare recursive types? 
John Max Skaller wrote: > > > In that case > >any type term can be interpreted as a rational tree. > > > .. what's that? An infinite tree that has only a finite number of different subtrees. Such trees can naturally be represented as cyclic graphs. > >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. If you have type functions you have type lambdas, even if they are implicit in the source syntax. And decidability of structural recursion between type functions is an open problem, at least for arbitrary functions, so be careful. (Thanks to Haruo for reminding me of Salomon's paper, I already forgot about that.) OCaml avoids the problem by requiring uniform recursion for structural types, so that all lambdas can be lifted out of the recursion. > >[...] > > I don't understand: probably because my description of the algorithm > was incomplete, you didn't follow my intent. Real code below. OK, now it is getting clearer. Your idea is to unroll the types k times for some k. Of course, this is trivially correct for infinite k. The correctness of your algorithm depends on the existence of a finite k. > I guess that, for example, 2(n +1) is enough for the counter, > where n is the number of typedefs in the environment. I don't think so. Consider: t1 = a*(a*(a*(a*(a*(a*(a*(a*b))))))) t2 = a*t2 This suggests that k must be at least 2m(n+1), where m is the size of the largest type in the environment. Modulo this correction, you might be correct. Still, ordinary graph traversal seems the more appropriate approach to me: represent types as cyclic graphs and check whether the reachable subgraphs are equivalent. There is also a recent paper about how to apply hashconsing techniques to cyclic structures: @article{Mauborgne:IncrementalUniqueRepresentation, author = "Laurent Mauborgne", title = "An Incremental Unique Representation for Regular Trees", editor = "Gert Smolka", journal = "Nordic Journal of Computing", volume = 7, pages = "290311", year = 2000, month = nov, }  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