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 OAA02998; Sun, 4 May 2003 14:30:44 +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 OAA03145 for ; Sun, 4 May 2003 14:30:42 +0200 (MET DST) Received: from mallaury.noc.nerim.net (smtp-100-sunday.noc.nerim.net [62.4.17.100]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h44CUgT15274 for ; Sun, 4 May 2003 14:30:42 +0200 (MET DST) Received: from karryall.dnsalias.org (karryall.dnsalias.org [62.4.18.180]) by mallaury.noc.nerim.net (Postfix) with ESMTP id 8D1E462D05; Sun, 4 May 2003 14:30:40 +0200 (CEST) Received: by karryall.dnsalias.org (Postfix, from userid 500) id 854361A0005; Sun, 4 May 2003 13:52:50 +0200 (CEST) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <16052.65298.366652.327622@karryall.dnsalias.org> Date: Sun, 4 May 2003 13:52:50 +0200 From: Olivier Andrieu To: John Max Skaller Cc: Subject: Re: [Caml-list] Two types of efficiency (Was Efficiency of 'a list) In-Reply-To: <3EB4C2BE.8020407@ozemail.com.au> References: <041d01c31208$f02327e0$0200a8c0@gateway> <3EB4C2BE.8020407@ozemail.com.au> X-Mailer: VM 7.14 under Emacs 21.2.1 X-Spam: no; 0.00; andrieu:01 caml-list:01 subtyping:01 covariance:01 disallows:01 recursion:01 variants:01 subtype:01 polymorphic:01 olivier:02 restrict:02 failing:02 similarly:03 invariant:03 arguments:03 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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 ? -- Olivier ------------------- 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