Either OOP or Liskov (choose one)

A while ago I read some Abadi-Cardelli, and illustrated what I learned by an example how Java does not have subsumptions principle (that is, if A is a subtype of B, an instance of A can be safely substituted everywhere where an instance of A is required).

So I had posted a blog entry with the example.

There's another post on this on blogger.

A deeper look into the issue can be found in "Is the Java Type System Sound? by Sophia Drossopoulou and Susan Eisenbach.
The paper shows that no, it is not, and also builds a sublanguage of Java where subsumption holds.

From this article I've got the following demonstration sample:

    class A {}

    class A1 extends A {}

    class B {

          char f(A x) { System.out.println("f(A." + x + ")"); return 'f'; }

          int f(A1 y) { System.out.println("f(A1." + y + ")"); return 12345; }

          void g(A1 z) { System.out.println("Called g"); System.out.println(f(z)); System.out.println("out of g"); }

          void h(A u, A1 v) { System.out.println("Called h"); System.out.println(f(u)); System.out.println(f(v)); System.out.println("out of h"); }

    }



    @Test

    public void testJavaSubsumption() {

        new B().g(new A1());

        new B().h(new A1(), new A1());

   }

The output is here:

Called g

f(A1.pigi.examples.library.tests.QueriesTest$A1@6526804e)

12345

out of g

Called h

f(A.pigi.examples.library.tests.QueriesTest$A1@42b1b4c3)

f

f(A1.pigi.examples.library.tests.QueriesTest$A1@20d2906a)

12345

out of h

I wonder though how long will the Earth population hold to the popular belief that one can have both OOP, with reasonable enough "dispatch", and substitution principle. One cannot.

Questions?

P.S. Actually, the issue was discussed in details By Oleg Kiselyov a while ago: http://okmij.org/ftp/Computation/Subtyping/.