[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:  20020425 (01:11) 
From:  John Max Skaller <skaller@o...> 
Subject:  Re: [Camllist] How to compare recursive types? 
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 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; 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:61296600850 > >  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