3 ms·

> I don't really see a need for square to extend a rectangle. Except that a square is-a rectangle! Especially in terms of geometry. So you should be able to us

> I don't really see a need for square to extend a rectangle. Except that a square is-a rectangle! Especially in terms of geometry. So you should be able to use this isomorphism in a type system as a perfect isomorphic mapping this is the entire purpose of the Liskov Substitution Principle. But the polymorphic result doesn't work polymorphically in a way that helps people reason about how the system works. It does things that are "correct" from a LSP and static typing system POV, but isn't helpful.

codygman 12y ago
I'll admit I'm a little rusty on my geometry, but I'm fairly sure I was never told that a square is a rectangle. If you mean insofar as operations on rectangles should work on squares, this could be accomplished with typeclasses.
- nickbauman 12y ago
  Ah ha! Now you see the problem. Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. And yet a discussion of it has emerged to whit this exchange. Gives one pause about the value of type systems for correctness eh?
  - codygman 12y ago
    > Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. Why do I care about whether or not it's normal way (for some people/languages) to use a type system in this way? I care about reality and having my types reflect it precisely. > Gives one pause about the value of type systems for correctness eh? I actually don't see how. It seems like you are saying "regardless of whether a square is a rectangle in reality, people (mis)use type systems to say this". Someone’s misuse of a tool doesn't call the tools value into question. Basically, I may not be able to model your exact relationships in the exact same way but I can model real world concrete things in the type-system which obtains the same or more flexibility and maintainability.
    - nickbauman 12y ago
      Exactly my point. This continuing misuse is VERY common even among experienced developers. The ongoing argument itself is a counterargument for type systems as being useful for correctness. At least it should give you some pause?
  - dragonwriter 12y ago
    > Whether or not a square is a rectangle in a Euclidian sense It is. A square is a rectangle whose length and width are equal. > it is a normal thing to use a type system in this way. It is a common mistake to misuse an OO type system this way -- to take an intuition about is-a relations of immutable objects and infer an is-a relationship about mutable cousins of those objects, which is almost always wrong without careful constraints on the mutations. It is this kind of mistake which is addressed by the Liskov Substitution Principle. Of course, that's the reason the LSP is usually taught fairly early on in any OO programming course, because the mistake is well-known. > Gives one pause about the value of type systems for correctness eh? No, type systems are great for enforcing correctness, but they are no better than the analysis behind the definition of the types. Of course, violating the LSP with a bad subtyping relationship is just as problematic without a static type system.
    - nickbauman 12y ago
      > It is a common mistake to misuse an OO type system this way. So common, I would argue, that it suggests there is a fundamental problem or question of utility with using type systems for correctness. You're right that this has nothing to do with a _static_ type system specifically but they're almost always used together that when you say "static" you are almost always heard as "statically typed", so the point is moot in my experience.
the_why_of_y 12y ago
Mathematically, a rectangle and a square are entities that do not have mutable state; any particular square in mathematics has a fixed width and height. If you define something that has a setWidth method, then it is not isomorphic to anything in mathematics! "is-a" is defined in terms of the operations that are valid. What semantics would you specify for the setWidth of a rectangle? The only reasonable contract for a general Rectangle is that setWidth sets the width but does not affect the height. Your proposed implementation of setWidth on a Square would violate that contract, and any other implementation would violate the invariant of the Square, and so it's clear that mutable Square "is-a" mutable Rectangle is simply not true. Basically the problem you are looking at is a variant of the reference typing problem, where you have, given S <: T, for writing Ref S <: Ref T and for reading Ref T <: Ref S, and in the general case of the read-write reference there is no subtype relationship between Ref S and Ref T.
dragonwriter 12y ago
> Except that a square is-a rectangle! Especially in terms of geometry. The thing in geometry that is called a "square" which is a special case of the thing in geometry which is called a "rectangle" is an immutable object whose side lengths and other features are part of its defining identity. Modeling this relationship works perfectly fine in an OO language -- but squares and rectangles of this type are immutable objects. A mutable square with operations which mutate the side lengths while preserving squareness is not a special case of a mutable rectangle with operations which mutate side lengths while preserving rectangleness without also preserving aspect ratio. The analytical problem here is mistakenly assuming an is-a relationship that applies to immutable entities in geometry applies to mutable objects whose mutation operations are defined in such a way that the is-a relationship does not logically hold. > So you should be able to use this isomorphism in a type system as a perfect isomorphic mapping this is the entire purpose of the Liskov Substitution Principle. Actually, the entire purpose of the Liskov Substitution Principle is to provide an analytical basis for excluding mistakes like subclassing a mutable "Rectangle" class for a mutable "Square" class with operations that aren't consistent with an is-a relationship simply because of an intuition about an is-a relationship between squares and rectangles in geometry which doesn't actually hold when you analyze the operations on the particular entities you are modelling (which are outside of the geometric definitions of squares and rectangle.) The LSP defines what can and cannot be a subclass, and it rules out the kind of mutable square to mutable rectangle relationship you have proposed in this thread.
- nickbauman 12y ago
  If LSP defines this why do people keep modeling things this way? More importantly, why do all the type systems let me create models this way. They have one job: to help me with correctness. Looks like that failed. So you see my point.

codygman 12y ago

I'll admit I'm a little rusty on my geometry, but I'm fairly sure I was never told that a square is a rectangle. If you mean insofar as operations on rectangles should work on squares, this could be accomplished with typeclasses.

nickbauman 12y ago
Ah ha! Now you see the problem. Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. And yet a discussion of it has emerged to whit this exchange. Gives one pause about the value of type systems for correctness eh?
- codygman 12y ago
  > Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. Why do I care about whether or not it's normal way (for some people/languages) to use a type system in this way? I care about reality and having my types reflect it precisely. > Gives one pause about the value of type systems for correctness eh? I actually don't see how. It seems like you are saying "regardless of whether a square is a rectangle in reality, people (mis)use type systems to say this". Someone’s misuse of a tool doesn't call the tools value into question. Basically, I may not be able to model your exact relationships in the exact same way but I can model real world concrete things in the type-system which obtains the same or more flexibility and maintainability.
  - nickbauman 12y ago
    Exactly my point. This continuing misuse is VERY common even among experienced developers. The ongoing argument itself is a counterargument for type systems as being useful for correctness. At least it should give you some pause?
- dragonwriter 12y ago
  > Whether or not a square is a rectangle in a Euclidian sense It is. A square is a rectangle whose length and width are equal. > it is a normal thing to use a type system in this way. It is a common mistake to misuse an OO type system this way -- to take an intuition about is-a relations of immutable objects and infer an is-a relationship about mutable cousins of those objects, which is almost always wrong without careful constraints on the mutations. It is this kind of mistake which is addressed by the Liskov Substitution Principle. Of course, that's the reason the LSP is usually taught fairly early on in any OO programming course, because the mistake is well-known. > Gives one pause about the value of type systems for correctness eh? No, type systems are great for enforcing correctness, but they are no better than the analysis behind the definition of the types. Of course, violating the LSP with a bad subtyping relationship is just as problematic without a static type system.
  - nickbauman 12y ago
    > It is a common mistake to misuse an OO type system this way. So common, I would argue, that it suggests there is a fundamental problem or question of utility with using type systems for correctness. You're right that this has nothing to do with a _static_ type system specifically but they're almost always used together that when you say "static" you are almost always heard as "statically typed", so the point is moot in my experience.

the_why_of_y 12y ago

Mathematically, a rectangle and a square are entities that do not have mutable state; any particular square in mathematics has a fixed width and height. If you define something that has a setWidth method, then it is not isomorphic to anything in mathematics! "is-a" is defined in terms of the operations that are valid. What semantics would you specify for the setWidth of a rectangle? The only reasonable contract for a general Rectangle is that setWidth sets the width but does not affect the height. Your proposed implementation of setWidth on a Square would violate that contract, and any other implementation would violate the invariant of the Square, and so it's clear that mutable Square "is-a" mutable Rectangle is simply not true. Basically the problem you are looking at is a variant of the reference typing problem, where you have, given S <: T, for writing Ref S <: Ref T and for reading Ref T <: Ref S, and in the general case of the read-write reference there is no subtype relationship between Ref S and Ref T.

dragonwriter 12y ago

> Except that a square is-a rectangle! Especially in terms of geometry. The thing in geometry that is called a "square" which is a special case of the thing in geometry which is called a "rectangle" is an immutable object whose side lengths and other features are part of its defining identity. Modeling this relationship works perfectly fine in an OO language -- but squares and rectangles of this type are immutable objects. A mutable square with operations which mutate the side lengths while preserving squareness is not a special case of a mutable rectangle with operations which mutate side lengths while preserving rectangleness without also preserving aspect ratio. The analytical problem here is mistakenly assuming an is-a relationship that applies to immutable entities in geometry applies to mutable objects whose mutation operations are defined in such a way that the is-a relationship does not logically hold. > So you should be able to use this isomorphism in a type system as a perfect isomorphic mapping this is the entire purpose of the Liskov Substitution Principle. Actually, the entire purpose of the Liskov Substitution Principle is to provide an analytical basis for excluding mistakes like subclassing a mutable "Rectangle" class for a mutable "Square" class with operations that aren't consistent with an is-a relationship simply because of an intuition about an is-a relationship between squares and rectangles in geometry which doesn't actually hold when you analyze the operations on the particular entities you are modelling (which are outside of the geometric definitions of squares and rectangle.) The LSP defines what can and cannot be a subclass, and it rules out the kind of mutable square to mutable rectangle relationship you have proposed in this thread.

nickbauman 12y ago
If LSP defines this why do people keep modeling things this way? More importantly, why do all the type systems let me create models this way. They have one job: to help me with correctness. Looks like that failed. So you see my point.