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

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

Andreas Rossberg wrote:

>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.
>
Ah, thanks.

>>>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;
    all (x:type) fun rev(a:list x): list x = { .. code to reverse a list }

but the only way to use it will be to instantiate it manually to create
an actual type:

  val x:list int = ....
  val y:list int = rev[int] x;

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

>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.
>
Ah. I see... you don't happen to have any references to online
material explaining that? .. let me guess, the fixpoints aren't allowed
inside the lambdas .. ok .. I have a picture of it in my head ..

>>>[...]
>>>
>>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.
>
Yes. And I contend it must exist, for a rational tree: the problem is
calculating it... or finding a better algorithm.

>>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
>
You are right, I thought of this example myself.

>
>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.
>
Yes, that seems like a good starting point.. though that number is
VERY large .. the 'unrolling' is exponential .. so my algorithm
is not very good: k is global .. so many unrollings are too long ..

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

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