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.
Let 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 Q[S].
We write 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 in S, then s is also in T. More loosely, we will say that every object s in S corresponds to exactly one object t in T. In other words, S implies T, or 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.
Apocalisp 
Please correct me if I’m wrong, but doesn’t Curry-Howard says that all types are props and all programs are proofs, not the other way around? I mean, given any language, one can concoct infinite interpretations for predicates over terms, not all of them realizable as types.
If that is true (and again, please correct me if it’s not), then we can’t generalize from “let q(x) be a property provable about objects x of type T” to the higher order type Q[T].
Rafael:
Yes we can. I’m using Q[A] to mean the proposition that q(x) holds for all x in A.
In other words, for all x in A there exists a program q(x) of some type Q[A].
Put another way, we could say that q has type (A => P). That is, for all x in A, there exists a proof of P by q(x). Therefore, if there exists a function f of type (B => A), then for all y in B there exists a proof of P by q(f(y)).
All this is saying is that implication is contravariant in its antecedent.
I think you’re wrong that some provable properties over terms are not realizable as types. They may not be realizable in the given language’s type system, but they’re still types. If a proposition is provable, then its proof is a program, and the proposition is a type for that program.
As a matter of fact, you are incorrect. It’s called Curry-Howard *Isomorphism*, or correspondence. That means it goes both ways.
Thanks for this reply, Daniel, it made me think trough my rudimentatry understanding of Curry-Howard and model theory. I understood C-W as an isomorphism between propositions (defined by logical connectives) and types (implication and function types, conjunction and products, disjunction and sums, etc.). The problem I had with the OP was the implied equivalence between predicates and propositions.
My mistake was that I didn’t realize that in any interpretation of a logical language every predicate *can* be described by a proposition. What tripped me was the thought of extensional definitions of predicates, but I believe these can be reduced to simple disjunctions, given an equality predicate or a characteristic predicate for every element of the domain.
Of course, I wouldn’t be surprised if I’m still wrong :)
I’m having trouble with “The set of all values in S is a subset of the values in T”
To say that S is a subtype of T to me means that S is not a subset of T, but a superset. S includes the definition of T and adds to it.
Am I missing something? Thanks.
Yeah, subtyping is confusing like that. Imagine a typical class hierarchy where, say, Button is a subtype of Widget. Not all Widgets are Buttons, but all Buttons are Widgets. So the set of all Buttons is smaller than the set of all Widgets, and the latter contains every object in the former.
However, the set of all functions that can accept Widgets is smaller than the set of functions that can accept Buttons. Every function that accepts a Widget can also accept Buttons, but a function that accepts a Button cannot accept just any Widget. So the set of functions of type Button => A (for some type A) is a superset of the functions of type Widget => A. This is probably what you’re thinking of.
I think you’re missing the point. The fact that the LSP is a trivial fact when interpreting subtyping as a function is exactly what allows you to interpret subtyping like that in the first place.
Think of the LSP as something that *defines* what subtyping really means, so that the usual type theoretic results may apply in an object oriented context.
Your reasoning is correct, but you started from the wrong premise, i.e. that the LSP is a “result”. The LSP is not a theorem, it’s more of a “modelling” principle that helps you determine when to use inheritance in API design.
I think the principle is even simpler than that.
Could you tie this into the conversation about Equal on the FJ mailing list?
Equal[Person] personEq = Equal.p3Equal().comap( new F[Person, P3[String, String, Int]]() { public P3[String, String, Int] f(Person p) { return p.toP(); // assume this does the obvious }});So if comap is type Q[T] => (S => T) => Q[S], we have Equal.p3Equal() of type Q[T], and F[Person, P3[…]] is of type (S => T). So T=P3 and S=Person.
I can see that. Person is one thing that a triple of (String,String,int) can represent.
What does Equal[Person] mean then? I think it’s Q[_]. Q[P3] means one can compare P3s for equality, Q[Person] means can compare Person`s for equality, and comap goes from one to the other with the help of the conversion function.
I think all of that is right, but please correct any parts that aren’t.
To go a little further, can we look at comap vs map?
Usually, coX is the dual of X, so I’m expecting that there should be map function that reverses the positions of Q[S] and Q[T]. And, of course, there is: Q[S] => (S => T) => Q[T] is the obvious map definition (easiest pictured when Q means list-of).
Does this mean that map represents covariance?
I usually think of covariance meaning that the return values of methods inherited from parent types can become more specific, and contravariance to mean that method arguments inherited from parent types can become more general.
That’s in “OO” language though. What’s the proper translation to the language of functions?
Dan,
That’s all exactly right!
Short answer: In the language of functions, covariance is exactly what you said: (S => T) => Q[S] => Q[T]. That type signature means “Q is covariant”. And contravariance is (T => S) => Q[S] => Q[T]. See my article: https://apocalisp.wordpress.com/2009/08/27/hostility-toward-subtyping/
Long answer:
In “OO” terms, imagine if your “this” type is R. And we could define Q this way (Scala):
type Q[A] = A => R
Then Q is contravariant, and we could rewrite (T => S) => Q[S] => Q[T] as:
(T => S) => (S => R) => T => R
Here, T is “more specific” than S, so any function that takes an S could take a T instead (because we can always turn that T into an S).
However, if we did:
type Q[A] = R => A
Then Q is covariant, and we could rewrite as:
(S => T) => (R => S) => R => T
Here, T is “more general” than S. And so any function that returns an S could also return a T (because we could always turn that S into a T).
More technical answer (still in the language of functions):
A category has objects and directed edges between objects (arrows).
The category of types has ordinary types as the objects, and functions as the arrows between types.
A functor is a mapping between categories.
A covariant functor Q maps every type T to a corresponding type Q[T], and every function of type (A => B) to a corresponding function of type (Q[A] => Q[B]). In terms of programming, such a functor maps the category of types to itself.
Every category has an opposite, in which all the arrows are inverted.
A contravariant functor is then simply a mapping from the category of types to its opposite. For example, a contravariant functor Q maps every type T to a corresponding type Q[T], but every function of type (A => B) to a corresponding function (Q[B] => Q[A]).
Thanks! That was very informative, especially the category theory at the end.
My algebra ends at about Sylow’s Theorem (intro group theory) so any category theory explained in terms I’m more familiar with definitely helps.
When you invert the arrows of a category whose morphisms are functions, don’t you end up with morphisms which aren’t necessarily functions? If f: A -> B is not injective, then what is f^op?
Tom: The opposite category has morphisms going the other way, and composition is also reversed. A morphism in Set^op from A to B is a function from B to A.
But my question is, if f is a non-injective or non-surjective function in category C (in other words it’s non-bijective), then what can its opposite, f^op, be in C^op? If f is not surjective, then f^op can’t be a total function, and if f is not injective then f^op can’t even be a partial function, since some of its inputs map to more than one output. I feel certain that I’m misunderstanding something fundamental here, but reversing the arrows in a category of functions seems like it would result in a category of relations which are not necessarily functions.
Oh wait, I see it now. I should’ve read your response more carefully. I morphism from A to B in Set^op is a function from B to A. That makes sense.
There is a difference between the pure functional and the functional + OO approach, and that is that in the OO+Functional approach, a value s can be of two types simultaneously, if the one type is a subclass of the other, whereas it cannot in the pure functional approach. So we can express that Socrates is a Man, and Man is a subtype of Animal, and so that Socrates is an Animal too in the OO approach, but not automatically in the functional one. (Or at least not in such a simple way).
I started a discussion on this a while back on the Homotopy Type Theory Group, and the answers there are very helpful:
https://groups.google.com/forum/#!topic/hott-cafe/kkDH_gcydRQ