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 KAA07676; Thu, 25 Apr 2002 10:53:17 +0200 (MET DST) 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 KAA06305 for ; Thu, 25 Apr 2002 10:53:16 +0200 (MET DST) Received: from indyio.rz.uni-sb.de (indyio.rz.uni-sb.de [134.96.7.3]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g3P8rEr04734 for ; Thu, 25 Apr 2002 10:53:14 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:xWaH+5p7yfc3Yg94+bV1kvdBsHs71CLC@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id KAA3569849 for ; Thu, 25 Apr 2002 10:53:12 +0200 (CEST) Received: from uni-sb.de (uni-sb.de [134.96.7.230]) by mars.rz.uni-sb.de (8.8.8/8.8.4/8.8.2) with ESMTP id KAA100390439 for ; Thu, 25 Apr 2002 10:53:12 +0200 (CEST) Received: from cs.uni-sb.de (cs.uni-sb.de [134.96.252.31]) by uni-sb.de (8.12.2/2002030600) with ESMTP id g3P8rBd20776; Thu, 25 Apr 2002 10:53:11 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:n3dH1ME+nGLOpUO1ImqNhBv0aFU3yMEc@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002030600) with ESMTP id g3P8rAW23067; Thu, 25 Apr 2002 10:53:11 +0200 (CEST) Received: from ps.uni-sb.de (grizzly.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.12.3/2002040900) with ESMTP id g3P8r9619356; Thu, 25 Apr 2002 10:53:09 +0200 (CEST) X-Authentication-Warning: email: Host grizzly.ps.uni-sb.de [134.96.186.68] claimed to be ps.uni-sb.de Received: from ps.uni-sb.de (zoidberg.ps.uni-sb.de [134.96.186.121]) by ps.uni-sb.de (8.11.6/8.11.0) with ESMTP id g3P8rAh18433; Thu, 25 Apr 2002 10:53:10 +0200 Message-ID: <3CC7C448.97542B67@ps.uni-sb.de> Date: Thu, 25 Apr 2002 10:54:32 +0200 From: Andreas Rossberg Organization: =?iso-8859-1?Q?Universit=E4t?= des Saarlandes X-Mailer: Mozilla 4.78 [en] (X11; U; Linux 2.4.9-21 i686) X-Accept-Language: de, en MIME-Version: 1.0 To: John Max Skaller 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> <3CC757B2.7030706@ozemail.com.au> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk John Max Skaller wrote: > > >>>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; But that's not the point. You do the same in ML. Still, if you allow arbitrary (probably higher-order) type declarations of the above form to be mutually recursive, it is unknown whether you can still decide type equivalence. > so the compiler doesn't have to deal directly with the type functions, > other than to apply them to create instance types. It has, because reduction of an application of a recursive type function may yield new redexes. In general, this procedure does not terminate. Using non-uniform recursion you can create type terms that correspond to irrational trees. > >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? Not really, but the OCaml sources are relatively readable :-) > .. let me guess, the fixpoints aren't allowed > inside the lambdas .. ok .. I have a picture of it in my head .. Not sure what you call "the fixpoints" (in your sources you called the actual fixpoint construct "Bind" and used "Fix" for recursive refs). Using the correct terminology the restriction is that lambdas are not allowed under fixpoints. > >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 :-) Why not use standard graph algorithms then? > 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. Huh? These types ARE equal: they both have the same infinite unrolling. The rational trees representing them are equal in the theories I know of - speaking of even or odd does not make any sense for infinite counts. -- 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