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 OAA15365; Sun, 18 Nov 2001 14:33:02 +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 OAA15420 for ; Sun, 18 Nov 2001 14:33:01 +0100 (MET) Received: from smtp.web.de (smtp01.web.de [194.45.170.210]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id fAIDX0v19159 for ; Sun, 18 Nov 2001 14:33:00 +0100 (MET) Received: from [149.225.99.51] (helo=pazo) by smtp.web.de with smtp (Exim 3.32 #26) id 165S4A-0002k9-00; Sun, 18 Nov 2001 14:32:58 +0100 Message-ID: <002001c17035$c722aa80$3363e195@pazo> Reply-To: "Andreas Rossberg" From: "Andreas Rossberg" To: "Clemens Hintze" , References: <20011116203745.A59514@qiao.in-berlin.de> Subject: Re: [Caml-list] [Q]: Co(ntra)variance and subtyping? Date: Sun, 18 Nov 2001 14:34:41 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 5.50.4133.2400 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4133.2400 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > - What does subtyping exactly mean in OCaml resp. functional > programming? OCaml has two separate notions of subtyping: - in the core language, to support objects - in the module language, for signature matching While subtyping for module types is rather standard from a superficial point of view, OCaml's treatment of subtyping in the core language is somewhat special because it does not provide so-called subsumption. Subsumption means that wherever a value of type t is expected you may freely provide a value of some subtype t'. This is not the case in OCaml: you have to explicitly coerce the value to the required supertype first. This is necessary to make type inference feasible. Note however that OCaml's object system rarely requires the use of subtyping, because it mainly relies on row polymorphism, which is more or less superior (although it admittedly complicates things to have both). > - What means covariance and contravariance of types and subtypes? Variance is a property of type constructor arguments. Take the "list" type constructor for example: it is said to be covariant in its argument because it comes with the following subtyping rule: t' < t => t' list < t list where "<" stands for "is subtype of". This means that you can use a t' list as a t list - the list type "varies" in the same direction as its argument, thus the term "covariance". The most important type constructor is "->", which has the following subtyping rule: t' < t and u' < u => (t -> u') < (t' -> u) Note the order of t and t' here: it goes in the opposite direction! Functions are covariant in their result type, but contravariant in their argument type. This may seem a bit funny at first (and in fact there are major programming languages that still insist on getting it plainly wrong - you already know one ;-) but it is the only sound rule. Intuitively it means that a function type is a subtype of another function type if it produces a more specific result while putting less requirements on its argument. In general, you have covariance for type components that are "produced" or "readable", and contravariance for components that are "consumed" or "writable". Another example of contravariance would be a polymorphic output channel. Of course, you cannot have both co- and contravariance for the same argument. So if some type component is both readable and writable then it has to be invariant. Consider arrays for example: there is no subtyping relation between any two array types t array and u array, no matter what relation t and u are in (with the only exception of t=u, then of course you trivially have `subtyping' in either direction). In fact, mutable types always have to be invariant (another thing that many popular OO languages do wrong - some at least do runtime checks for compensation, some just crash). > OTOH, these terms seem to be very important in dealing with OCaml or > functional programming. I hope my explanations clarified that these terms are mainly important if you do OO in the presence of polymorphic types. Functional programming in its purer forms usually does not use nor require subtyping, so need not bother with them ;-) Cheers, - Andreas ------------------- Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr