LSP (was Re: Function.prototype.bind)
On Wed, Sep 10, 2008 at 3:55 PM, Graydon Hoare <graydon at mozilla.com> wrote:
Mark S. Miller wrote:
On Wed, Sep 10, 2008 at 12:49 AM, Brendan Eich <brendan at mozilla.org> wrote:
Method overriding in classical OOP breaks [LSP].
How? I don't understand.
LSP is a formulation of subtyping, and it's one that few languages follow. This is (oddly) the second time it's been brought up on this list. It's really a bit of a non sequitur here, particularly since there is hardly anything resembling a type system in ES3 anyways. But for our edification (and to keep the term from re-emerging)...
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition. [...]
I see. Thanks for the clarification. I had not understood LSP as a property for a language to enforce, but rather as a design rule for programmers. Nominal types usually correspond to some behavioral expectations -- a contract if you will -- that are used to coordinate the expectations of implementers of a type and clients of a type. However, these contracts are rarely written down, and hardly ever written down in machine understandable form. So I agree that enforced LSP is unrealistic, because one can't enforce conformance to expectations that aren't written down. But, as a programmer, one can endeavor to only claim that an X is a kind of Y when X satisfies all the expectations that clients of Y expect. If this isn't LSP, it is at least design by contract with nominal types as contract names. It is still a good design rule in languages (like JavaScript) with nominal subtyping (via instanceof).
Mark S. Miller wrote:
still a good design rule ...
Yup,
in languages (like JavaScript) with nominal subtyping (via instanceof).
Oh goodness, don't say that while the type theorists are in the room!
On Wed, Sep 10, 2008 at 4:12 PM, Graydon Hoare <graydon at mozilla.com> wrote:
in languages (like JavaScript) with nominal subtyping (via instanceof).
Oh goodness, don't say that while the type theorists are in the room!
;)
Graydon Hoare wrote:
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition.
What? For example, what would you have to delete from Java, ignoring the parts where a program can examine itself like reflection?
Waldemar
On Mon, Sep 22, 2008 at 6:25 PM, Waldemar Horwat <waldemar at google.com> wrote:
Graydon Hoare wrote:
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition.
What? For example, what would you have to delete from Java, ignoring the parts where a program can examine itself like reflection?
I don't know that I would phrase it in terms of deleting functionality from the language, but it's pretty clear that Java's notion of subtyping is not Liskov's. Here's a simple illustration:
doodleproject.sourceforge.net/articles/2000/liskovSubstitutionPrinciple.html
Waldemar Horwat wrote:
Graydon Hoare wrote:
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition.
What? For example, what would you have to delete from Java, ignoring the parts where a program can examine itself like reflection?
The big one is "method overriding in subtypes", though as you say there are various other cases such as reflection. If I have a program that uses some type:
class Mul { int f(int x, int y) { return x * y; } }
I can form a subtype such that substituting the subtype for the supertype in some program will likely change the behavior of the program:
class NotTheMulYoureLookingFor extends Mul { int f(int x, int y) { return x + y; } }
There was once a line of work on "ADT" languages that aimed to formulate subtyping in more restrictive terms. Liskov's work was generally in that lineage. Ours is not.
Waldemar Horwat wrote:
Graydon Hoare wrote:
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition.
What? For example, what would you have to delete from Java, ignoring the parts where a program can examine itself like reflection?
The big one is "method overriding in subtypes", though as you say there are various other cases such as reflection. If I have a program that uses some type:
class Mul { int f(int x, int y) { return x * y; } }
I can form a subtype such that substituting the subtype for the supertype in some program will likely change the behavior of the program:
class NotTheMulYoureLookingFor extends Mul { int f(int x, int y) { return x + y; } }
What does this have to do with your claim about the Liskov property? Where in this example do you take an object o1 of type NotTheMulYoureLookingFor and prove that there is no object o2 of type Mul that satisfies the Liskov property?
Waldemarwaldemar at google.com wrote:
Waldemar Horwat wrote:
Graydon Hoare wrote:
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition. What? For example, what would you have to delete from Java, ignoring the parts where a program can examine itself like reflection? The big one is "method overriding in subtypes", though as you say there are various other cases such as reflection. If I have a program that uses some type:
class Mul { int f(int x, int y) { return x * y; } }
I can form a subtype such that substituting the subtype for the supertype in some program will likely change the behavior of the program:
class NotTheMulYoureLookingFor extends Mul { int f(int x, int y) { return x + y; } }
What does this have to do with your claim about the Liskov property? Where in this example do you take an object o1 of type NotTheMulYoureLookingFor and prove that there is no object o2 of type Mul that satisfies the Liskov property?
This is seriously belaboring a point, but ... I'll try again. The LSP describes this subtype relationship here iff:
for every object o1 of type NotTheMulYoureLookingFor: there is an object o2 of type Mul: such that for all programs P: the behavior of P(o2) is the same as P(o1)
The only wiggle room I can see here is if you're saying that instances like o1 are also "objects of type Mul", such that you can let o2=o1 and trivially satisfy it. But that reading seems totally backwards: the LSP is a principle for defining a subtype relation; it hardly seems useful to incorporate an existing subtype relation into its use of the phrase "object o2 of type T".
I think we're possibly talking past each other, or discussing different things? Possibly I've just misunderstood the issue all this time. All I'm saying is that in Java -- and most contemporary OO languages -- the subtype relation is defined (roughly) between classes in a way that is not very much like the way I usually interpret the LSP. Substituting an instance of a subclass doesn't preserve behavior of programs that previously used instances of the superclass. You can cook up some pair of classes that are substitutable in the Liskov sense -- and it's a good guideline during class design -- but it's not the way "subtype" (or at least "subclass") is defined in these languages.
(In later papers -- presumably when it was clear that subtypes in many languages were going to carry dynamic function tables -- Liskov and others revisited this issue, and arrived at the formalism of combining method contracts during overriding, such as is done in Sather, D and Eiffel. Java doesn't to that either. There's really very modest constraints on the behavior of a method.)
This is seriously belaboring a point, but ... I'll try again. The LSP describes this subtype relationship here iff:
for every object o1 of type NotTheMulYoureLookingFor: there is an object o2 of type Mul: such that for all programs P: the behavior of P(o2) is the same as P(o1)
The only wiggle room I can see here is if you're saying that instances like o1 are also "objects of type Mul", such that you can let o2=o1 and trivially satisfy it.
Yes, that's what it means here. The LSP applies because you can let o1=o2. This is not always a trivial transformation because in some languages values of different types are not necessarily compatible.
Waldemarwaldemar at google.com wrote:
This is seriously belaboring a point, but ... I'll try again. The LSP describes this subtype relationship here iff:
for every object o1 of type NotTheMulYoureLookingFor: there is an object o2 of type Mul: such that for all programs P: the behavior of P(o2) is the same as P(o1)
The only wiggle room I can see here is if you're saying that instances like o1 are also "objects of type Mul", such that you can let o2=o1 and trivially satisfy it.
Yes, that's what it means here. The LSP applies because you can let o1=o2. This is not always a trivial transformation because in some languages values of different types are not necessarily compatible.
But then the LSP is saying ... that you should define "subtype" as "the relation between any two things that are subtypes". It's vacuous if you read it that way. I think that is not the correct reading at all.
Mark S. Miller wrote:
LSP is a formulation of subtyping, and it's one that few languages follow. This is (oddly) the second time it's been brought up on this list. It's really a bit of a non sequitur here, particularly since there is hardly anything resembling a type system in ES3 anyways. But for our edification (and to keep the term from re-emerging)...
Quoting Liskov[1]:
"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T."
Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition. Very few languages define "subtype" this way. It's somewhat supported via contract-based OO type systems (Eiffel, Sather and D, for example) in the sense that it holds for all and only the "behavior" you remembered to encode as a contract, and your contracts never fail; but in general as soon as you have behavior overriding (or first class functions at all) your subtype rule probably violates LSP.
(It'd be lovely if we all wrote in languages that treated subtypes this way; we'd have far fewer bugs. Wake me up when we get there!)
-Graydon
[1] portal.acm.org/citation.cfm?id=62141
Mark S. Miller wrote: > On Wed, Sep 10, 2008 at 12:49 AM, Brendan Eich <brendan at mozilla.org> wrote: >> On Sep 9, 2008, at 11:51 PM, Mark S. Miller wrote: >> >>>> LSP is not preserved by many cases in OO languages. Is it important here? >>> I think it's a valuable property >> It's come up before, but is it a sacred cow? > > Mu? > >> Method overriding in classical >> OOP breaks it. > > How? I don't understand. LSP is a formulation of subtyping, and it's one that few languages follow. This is (oddly) the second time it's been brought up on this list. It's really a bit of a non sequitur here, particularly since there is hardly anything resembling a type system in ES3 anyways. But for our edification (and to keep the term from re-emerging)... Quoting Liskov[1]: "What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T." Think it over. Imagine what you'd have to delete from any language you use, for its "subtype" relation to conform to that definition. Very few languages define "subtype" this way. It's somewhat supported via contract-based OO type systems (Eiffel, Sather and D, for example) in the sense that it holds for all and only the "behavior" you remembered to encode as a contract, and your contracts never fail; but in general as soon as you have behavior overriding (or first class functions at all) your subtype rule probably violates LSP. (It'd be lovely if we all wrote in languages that treated subtypes this way; we'd have far fewer bugs. Wake me up when we get there!) -Graydon [1] http://portal.acm.org/citation.cfm?id=62141