Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] [Q]: Co(ntra)variance and subtyping?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2001-11-19 (12:50)
From: Markus Mottl <markus@o...>
Subject: Re: [Caml-list] Re: [Q]: Co(ntra)variance and subtyping?
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

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

Let's consider adding elements to "foo" now, getting super type

  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

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

   (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... :-)

Markus Mottl

Markus Mottl                                   
Austrian Research Institute
for Artificial Intelligence        
Bug reports:  FAQ:
To unsubscribe, mail  Archives: