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 NAA02676; Mon, 19 Nov 2001 13:50:15 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA03345 for caml-list@pauillac.inria.fr; Mon, 19 Nov 2001 13:50:14 +0100 (MET) 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 NAA02472 for ; Mon, 19 Nov 2001 13:03:22 +0100 (MET) Received: from chopin.ai.univie.ac.at (chopin.ai.univie.ac.at [131.130.174.170]) by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id fAJC3K116930 for ; Mon, 19 Nov 2001 13:03:20 +0100 (MET) Received: (from markus@localhost) by chopin.ai.univie.ac.at (8.9.3/8.9.3/Debian 8.9.3-21) id NAA30360; Mon, 19 Nov 2001 13:03:15 +0100 Date: Mon, 19 Nov 2001 13:03:15 +0100 From: Markus Mottl To: Clemens Hintze Cc: caml-list@inria.fr Subject: Re: [Caml-list] Re: [Q]: Co(ntra)variance and subtyping? Message-ID: <20011119130314.B29501@chopin.ai.univie.ac.at> References: <20011116203745.A59514@qiao.in-berlin.de> <002001c17035$c722aa80$3363e195@pazo> <20011118101636.A38485@qiao.in-berlin.de> <20011117185051.A7607@qiao.in-berlin.de> <9t7v4d$gij$1@qrnik.zagroda> <20011119093329G.garrigue@kurims.kyoto-u.ac.jp> <20011119082446.B79776@qiao.in-berlin.de> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i In-Reply-To: <20011119082446.B79776@qiao.in-berlin.de>; from cle-ocaml@qiao.in-berlin.de on Mon, Nov 19, 2001 at 08:24:46 +0100 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Clemens Hintze schrieb am Montag, den 19. November 2001: > I want to thank you all, who have contributed to answer my questions > about co(ntra)variance. Now I will have to read it all for a few times > (I guess a dozent will enough ;-) to try to understand what you gurus > tried to tell me ;-)) Maybe a small excursion to logic makes things easier to understand. Just consider types as propositions about values, for example "x is an integer" or "f maps a foo to a bar". Let's focus on the latter case: foo -> bar (1) Whenever we find a case where "foo" holds (whenever we have a value of type "foo"), then this implies "bar" (the result of function "f" will be "bar"). We now add further elements to the type "bar", getting type "super_bar" (it is a super type of the former by definition). Logically speaking, this means: bar -> super_bar (2) Together with proposition (1), this allows us to derive: foo -> super_bar (3) One can prove this easily (e.g. using truth tables) by showing that the following is a tautology (holds irrespective of our interpretation of "foo" and "bar"): (foo -> bar) /\ (bar -> super_bar) -> (foo -> super_bar) (4) Therefore, if some context expects a function of type "foo -> super_bar", (expects that "foo -> super_bar" holds), then it is sound to substitute a function of type "foo -> bar" in it, given that "bar -> super_bar" holds. The term that applies here is "covariance", because making the proposition "bar" weaker (letting it apply to additional cases, i.e. making it less strict) also makes "foo -> bar" weaker (and vice-versa). Let's consider adding elements to "foo" now, getting super type "super_foo": foo -> super_foo (5) Would it be sound to assume the following? - (foo -> bar) /\ (foo -> super_foo) -> (super_foo -> bar) (6) Just try to prove this a tautology, and you'll quickly find out that it isn't! It is also not an invalid argument (i.e. not false in general), its satisfiability "depends". Surely, nobody would want to have computer programs whose correctness "depends" on possibly unpredictable eventualities! In which cases can we safely assume that (6) holds? This is only the case when our value of type "super_foo" is still a "foo" (which actually means that "super_foo" must be a subtype of "foo"!): super_foo -> foo (7) But together with (5) this means that both types must be equivalent: super_foo <-> foo (8) Not very interesting a case for programmers. But this one looks much nicer: (sub_foo -> foo) /\ (foo -> bar) -> (sub_foo -> bar) (9) Because we can easily prove that this is valid, we see that we have to make the proposition "foo" stronger (apply to a subset only) to make "foo -> bar" weaker (apply more generally). We call this requirement of making something "stronger" to get something "weaker" (and vice-versa) "contravariance" as opposed to "covariance", which goes with weaker/weaker (more general / more general) and stronger/stronger (more specific / more specific). Some OO-languages (e.g. Eiffel) assume that (6) always holds (is a tautology). But this is unsound as we have seen, and one can therefore find cases, where static type safety will break, which will either crash the program or require expensive runtime checks. I hope the logicians among you will now clean out all flaws in my example... :-) Regards, Markus Mottl -- Markus Mottl markus@oefai.at Austrian Research Institute for Artificial Intelligence http://www.oefai.at/~markus ------------------- 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