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

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

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 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. 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 hash-consing 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		= "290--311",
  year		= 2000,
  month		= nov,
}

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