From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id DAA01271; Thu, 25 Apr 2002 03:11:28 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id DAA01350 for ; Thu, 25 Apr 2002 03:11:26 +0200 (MET DST) Received: from sunny.pacific.net.au (sunny.pacific.net.au [203.25.148.40]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g3P1BO128472 for ; Thu, 25 Apr 2002 03:11:25 +0200 (MET DST) Received: from wisma.pacific.net.au (wisma.pacific.net.au [210.23.129.72]) by sunny.pacific.net.au with ESMTP id g3P1BGXt015664; Thu, 25 Apr 2002 11:11:17 +1000 (EST) Received: from ozemail.com.au (ppp240.dyn18.pacific.net.au [61.8.18.240]) by wisma.pacific.net.au with ESMTP id LAA14830; Thu, 25 Apr 2002 11:11:14 +1000 (EST) Message-ID: <3CC757B2.7030706@ozemail.com.au> Date: Thu, 25 Apr 2002 11:11:14 +1000 From: John Max Skaller User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:0.9.2.1) Gecko/20010901 X-Accept-Language: en-us MIME-Version: 1.0 To: Andreas Rossberg CC: caml-list@inria.fr Subject: Re: [Caml-list] How to compare recursive types? References: <3CBD4523.6080707@ozemail.com.au> <87y9fmr4fo.dlv@wanadoo.fr> <3CC656E1.5020108@ozemail.com.au> <3CC675D7.40ADAD0F@ps.uni-sb.de> <3CC6AF9F.5040801@ozemail.com.au> <3CC6C986.A32F40F7@ps.uni-sb.de> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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