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 NAA30798; Mon, 5 May 2003 13:04:35 +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 NAA30483 for ; Mon, 5 May 2003 13:04:33 +0200 (MET DST) Received: from mail1.tpgi.com.au (mail.tpgi.com.au [203.12.160.57]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h45B4WT00768 for ; Mon, 5 May 2003 13:04:32 +0200 (MET DST) Received: from ozemail.com.au (syd-ts18-2600-074.tpgi.com.au [203.58.21.74]) (authenticated (0 bits)) by mail1.tpgi.com.au (8.11.6/8.11.6) with ESMTP id h45B4K423040; Mon, 5 May 2003 21:04:21 +1000 Message-ID: <3EB6452E.8030100@ozemail.com.au> Date: Mon, 05 May 2003 21:04: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: Olivier Andrieu CC: caml-list@inria.fr Subject: Re: [Caml-list] Two types of efficiency (Was Efficiency of 'a list) References: <041d01c31208$f02327e0$0200a8c0@gateway> <3EB4C2BE.8020407@ozemail.com.au> <16052.65298.366652.327622@karryall.dnsalias.org> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; ozemail:01 caml-list:01 andrieu:01 subtyping:01 covariance:01 disallows:01 recursion:01 3.06:01 expr:01 toxteth:01 glebe:01 2037,:01 9660:01 0850:01 ocaml:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Olivier Andrieu wrote: > John Max Skaller [Sunday 4 May 2003] : > > Similarly, subtyping of polymorphic variants is invariant > > in the arguments, when covariance is sound and more useful. > > This is a real pain for me, since it destroys the main use > > I hoped to obtain for polymorphic variants: > > > > type x = [`A | `B of x] > > type y = [`A | `B of y | `C] > > > > x *is* a subtype of y, but the type system > > disallows it, failing to recognise that every `B x > > of type x is also a `B y of y. Typically I have > > say a term for an expression and I want to eliminate > > some cases by say a term reduction, but I can't restrict > > the resultant type as desired because there's no way > > to 'narrow' the type recursion. > > # type x = [`A | `B of x] ;; > type x = [ `A | `B of x] > # type y = [`A | `B of y | `C] ;; > type y = [ `A | `B of y | `C] > # fun a -> (a :x :> y) ;; > - : x -> y = > > Doesn't that mean that x is a subtype of y ? Indeed. Hmm .. has this changed since 3.04? [I just installed the CVS version which is 3.06+31 (2003/5/2)] Let me try a more comprehensible example. type expr1 = [`Prim | `Add of expr1 * expr1 | `Plus of expr1 * expr1] type expr2 = [`Prim | `Add of expr2 * expr2] let lift e = (e : expr2 :> expr1) ;; let rec r (e:expr1): expr2 = match e with | `Prim -> `Prim | `Add (a,b) -> `Add (r a,r b) | `Plus (a,b) -> `Add (r a, r b) ;; And it works. It didn't before! So thx for pointing this out, and thx to the ocaml team for doing this work. Now I'll go off and try to use it. It will simplify my code a lot: at present I have a lot of cases I know won't occur, because they've been "reduced out" by a prior term rewriting routine, but the typing didn't allow this to be expressed. A lot of nasty | _ -> assert false terms will be eliminated: getting rid of wildcard matches should improve compile time error diagnosis considerably. Kind of a pity I can't write: type expr1 = [expr2 | `Plus expr1 * expr1] but it would lift the wrong recursion out. -- 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