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 GAA03574; Thu, 25 Apr 2002 06:41:53 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id GAA03625 for ; Thu, 25 Apr 2002 06:41:52 +0200 (MET DST) Received: from sunny.pacific.net.au (sunny.pacific.net.au [203.25.148.40]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g3P4foT13594 for ; Thu, 25 Apr 2002 06:41:50 +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 g3P4flXt002844; Thu, 25 Apr 2002 14:41:47 +1000 (EST) Received: from ozemail.com.au (ppp127.dyn147.pacific.net.au [210.23.147.127]) by wisma.pacific.net.au with ESMTP id OAA13294; Thu, 25 Apr 2002 14:41:45 +1000 (EST) Message-ID: <3CC78908.7050507@ozemail.com.au> Date: Thu, 25 Apr 2002 14:41:44 +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: caml-list@inria.fr CC: Andreas Rossberg 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> <3CC757B2.7030706@ozemail.com.au> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Argg.. my algorithm is wrong. Here is a counterexample: typedef x = x * int; typedef y = (y * int) * int; If you just unroll these types for a while, they look equal, but they aren't: in fact y might be considered a subtype of x. Type x is any cyclic list of n>0 ints. Type y is any non-empty cyclic list of an *even* number of ints. Y might be represented in C using struct y { y *next; int first; int second; }; Now I *really* need a proper algorithm .. Felix is extensional: in a product, we normally expand types, but we can't do that if the type is recursive. A pointer must be used not only at the fix point, but at any possible fixpoint of an equivalent definition...so any strongly connected components have to be refered to by a pointer I think .. this would solve the representation problem above (at least in this case) but the fact remains that the types above are not equal. A similar example: x2 = x * int; x3 = x2 * int; ... shows how to construct a type holding 'at least' a certain number of ints... and my algorithm also fails to distinguish these types. Here., the representations would be different .. there is no recursion in the 'top' part of the type, so an expanded struct would be used .. Hmmm.. does it show one type is a subtype of the other .. hmmm .. perhaps it shows that there exists a type which both types are subtypes of .. that sounds right .. -- 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