How to think about polymorphism with subtyping

Question

The Liskov Substitution Principle states:

Invariants of the supertype must be preserved in a subtype.

I'm particularly interested with the intersection of this principle and polymorphism. In particular subtype-polymorphism though, in fact, this seems to be the case with parametric polymorphism and Haskell type classes.

So, I know that functions are subtypes when their arguments are contravariant and their return types covariant. We can assume that methods are just functions with an implicit "self" argument. However, this seems to imply that if a subclass overrides a method of the parent, it is no longer a subtype, as one of it's methods is no longer a subtype.

For example. Take the following pseudo-code:

class Parent:
    count : int
    increment : Parent -> ()
    {
        count += 1
    }

class Child inherits Parent:
    increment : Child -> ()
    {
        count += 2
    }

So going back to the LSP: can we say that a property of Parent.increment() should hold for Child.increment() even though these two don't obey a strict subtyping relation?

More generally my question is: how do the rules of subtyping interface with the more specific arguments of polymorphic functions and what is the correct way of thinking about these two concepts together?

Answer 1

Quoting Wikipedia's article on Liskov Substitution Principle

More formally, the Liskov substitution principle (LSP) is a particular definition of a subtyping relation, called (strong) behavioral subtyping [...]

Behavioral subtyping is a stronger notion than typical subtyping of functions defined in type theory, which relies only on the contravariance of argument types and covariance of the return type. Behavioral subtyping is trivially undecidable in general [...]

There are a number of behavioral conditions that the subtype must meet:

• Preconditions cannot be strengthened in a subtype.
• Postconditions cannot be weakened in a subtype.
• Invariants of the supertype must be preserved in a subtype.

Thus LSP is a stronger definition for sub-typing, that relies on features beyond type-theory.

In your example, this rises and falls on your invariant.

calling increment will increase count by **exactly 1**

Obviously Child can't be expressed in terms of Parent since the invariant is broken. This can't be deduced from syntax alone.

LSP should lead you to define Parent and Child separately, having them both inherit from Incrementable which has a weaker post condition.