# liskov substitution principle seems to have two conventional meanings

This is a question about the semantics of the name, rather than about the principle itself. What is the Liskov Substitution Principle (LSP)?

LSP seems to have two meanings in the literature I've seen. One statement is the rule that determines whether one function type is a subtype of another? I.e, A->Y is a subtype of B->X, if B is a subtype of A and Y is a subtype of X. The other statement is that in an object oriented language, a method in subclasses should be element of the subtype of the type of the method in the parent class.

The principle that B<:A, X<:Y implies A->X <: B->Y was a known principle well before the name "Liskov Substitution Principle" was ever coined. I have found references to this principle from the early 80s.

For example, https://cl-su-ai.cddddr.org/msg04614.html, here is an email from 1987 where the author describes what he calls "PROBLEM II". It is the definition and justification for the definition of arrow types described above. Furthermore, this presentation, http://www.softwarepreservation.org/projects/LISP/crisp_ibm370_sdc/CRISP-talk.pdf, claims it was known in the early 1970s.

• I've never seen the subtyping rule for functional types $A\to B$ being referred to as LSP. Where did you found that being called LSP? – chi Sep 13 '18 at 18:32
• Here is one thing I found. apocalisp.wordpress.com/2010/10/06/… – Jim Newton Sep 13 '18 at 22:00
• Maybe I'm wrong. Perhaps this was simply a misconception I had which was never challenged. What is the contravariance subtype rule for arrow types called? – Jim Newton Sep 13 '18 at 22:02

I don't think either of these is the Liskov substitution principle. My understanding of the principle is that for $S$ to be a subtype of $T$, it must be the case that we can substitute a value of type $S$ anywhere a value of type $T$ is required without compromising the correctness of our program.