The Liskov Substitution Principle is a much cited result by those who believe in the myth of “object-oriented programming”. But the LSP is like many things in the OO mythos that become “invisible or simpler” when looked at from the perspective of the properties of functions (which is what programming really is about).
Let’s remind ourselves of the LSP:
Let q(x) be a property provable about objects x of type T. Then q(y) should be true for objects y of type S where S is a subtype of T.
Q[A] be a property provable about objects of type
A. By Curry-Howard, a proof of this property is a program, and the property that it proves is a type.
So we translate “let q(x) be a property provable about objects x of type T” to just
Q[T]. We translate “q(y) should be true for objects y of type S” to
X => Y to mean “X implies Y”, or “if X, then Y”. Let’s translate “S is a subtype of T” into these terms. It means that the set of all values in
S is a subset of the values in
T. So if you have a value
s is also in
T. More loosely, we will say that every object
S corresponds to exactly one object
T. In other words,
S => T. This is precisely the type of functions from S to T, and we will consider every function of this type to be a proof that
S => T.
We’re now ready to state the Liskov Substitution Principle:
For all T, S. Q[T] => (S => T) => Q[S]
Read it as: If the property Q holds for all values of type T, then if every object of type S maps to exactly one object of type T, the property Q holds for all values of type S.
This is exactly the type of
comap for a contravariant functor. So LSP just says “predicates are contravariant”. And what’s more,
comap literally boils down to function composition in practise. So it’s almost completely trivial.