Re: [Caml-list] Re: [Q]: Co(ntra)variance and subtyping?

[Markus Mottl <markus@oefai.at>]

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