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 UAA05192; Tue, 23 Mar 2004 20:09:08 +0100 (MET) 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 UAA06710 for ; Tue, 23 Mar 2004 20:09:06 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by concorde.inria.fr (8.12.10/8.12.10) with ESMTP id i2NJ93Hd009375 for ; Tue, 23 Mar 2004 20:09:04 +0100 Received: from [192.168.1.200] (ppp114-118.lns1.syd3.internode.on.net [150.101.114.118]) by smtp3.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id i2NJ8vUK061438; Wed, 24 Mar 2004 05:38:58 +1030 (CST) Subject: Re: [Caml-list] extensible records again From: skaller Reply-To: skaller@users.sourceforge.net To: Michael Vanier Cc: skaller@users.sourceforge.net, caml-list In-Reply-To: <20040322055430.A45C89BBA2@orchestra.cs.caltech.edu> References: <20040321062143.BE7D29BBA2@orchestra.cs.caltech.edu> <405D4D77.2030403@columbia.edu> <20040321084008.429279BBA2@orchestra.cs.caltech.edu> <405DBE78.5020609@columbia.edu> <20040321223401.392519BBA2@orchestra.cs.caltech.edu> <1079926276.3165.49.camel@pelican.wigram> <20040322055430.A45C89BBA2@orchestra.cs.caltech.edu> Content-Type: text/plain Message-Id: <1080069240.4708.39.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 24 Mar 2004 06:14:01 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at concorde by Joe's j-chkmail ("http://j-chkmail.ensmp.fr")! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 extensible:01 sourceforge:01 2004:99 vanier:01 covariant:01 subtyping:01 fixpoints:01 failwith:01 jacques:01 fixpoints:01 recursively:01 reductions:01 abstractions:01 statically:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk X-Status: X-Keywords: X-UID: 333 On Mon, 2004-03-22 at 16:54, Michael Vanier wrote: > > The main downside is that to make covariant subtyping > > you need to use fixpoints, which is fine for a single > > parameter but unworkable for a more complex term > > structure. > > Forgive my ignorance, but what do you mean by this? At the moment you can do this: type x = [`A | `B ] type y = [a | `C ] so that y is a subtype (extension) of x. You can even match: match aY with | #x as xv -> xv | _ -> failwith "Not an x" to reduce aY to an x. This works fine as written because y is a 'flat' extension of x: the type constructors are invariant in their arguments (vacuously in the example, since none of the constructors have any arguments). But now consider a recursive type: type x = [`A of x | `B] type y = [ `A of y | `B | `C of y] Jacques Garrigue showed me a solution using fixpoints where the you don't want to write out all the terms of x in y again: type 't x1 = [`A of 't | `B] type 't x2 = [`C of 't] (* the extension *) type 't y1 = ['t x1 | 't x2] (* combine the parts *) type x = 't x1 as 't (* fixate *) type y = 't y1 as 't A real world example: terms of some language may included 'syntactic sugar' which can be removed recursively by rewriting rules/term reductions. For example Felix uses an extended type term which allows lambda abstractions in types. We'd like to indicate *statically* that a term has been reduced. The difficulty is that there seems to be an almost combinatorial explosion in how much you have to write in the number of parameters. In the above example there is only one, indicated by 't. In Felix, I want to partition expressions, types, patterns, statements, and a few other kinds of terms into one or more classes and use some combinations of these: but all these terms are mutually recursive: statements can contain expressions and types and patterns, patterns have 'when' expressions, types may contain "typeof(expression)" as a type, and statements can be considered as expressions.. So I end up with a rather large number of parameters on each of the fine grained components I want to combine: something like: type 'expr 'typ 'pat 'stat expr1 = .... ... type 'expr 'typ 'pat 'stat typ1 = ... ... In the 'flat' case I don't have to write out the parameters. And if I forget the covariant refinement and just use the supertype everywhere, losing the benefit of extra static type checking, I can just declare all these terms once and make them all mutually recursive. I want to have my cake and eat it too :D I want to write: type x = [`A of x | `B ] type y = [a | `C ] and have it 'know' that the `A in type y takes an y argument, not an x. Perhaps this can be done as so: type x = [`A of +x | `B ] where the '+' indicates that the argument is covariant. -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net ------------------- 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