A wrong question: Is a Square a Rectangle?
Overview
- what is Subtyping?
- what is Liskov Substitution Principle?
- what's the problem?
- how to solve this mistake of type system
1. What is Subtyping?
A common misunderstanding is OOP must have subtyping and generic at
the same time, but they are independent features, generic is just a
type-level function with takes a type, generates a type. Subtyping is
a relationship between type, when we say A <: B, which means A is a
subtype of B. In Java, we use concrete syntax extends or
implements.
2. What is Liskov Substitution Principle(LSP)?
LSP said
if S is a subtype of T, then objects of type T in a program may be replaced with objects of type S without altering the program
3. What's the problem
Square is a special Rectangle where all four sides are equal in length. Thus we might write down:
class Rectangle { double x, y; Rectangle(double initX, double initY) { x = initX; y = initY; } public void setX(double x) { this.x = x; } public void setY(double y) { this.y = y; } } class Square extends Rectangle { Square(double initX, double initY) throws SquareException { super(initX, initY); if (initX != initY) { throw new SquareException(initX, initY); } } }
Ok, so we can have following program:
Square s = new Square(2, 2); Rectangle r = s; r.setX(10);
Oops, s is not a square anymore, this correctly follows LSP but
incorrect generally. To solve this, we revert the relationship between
Square and Rectangle, now we have:
class Square { double x; } class Rectangle extends Square { double y; }
Now setX and setY both will not affect the Square, imagine a
method double area(), LSP was broken(now Square returns x*x and
Rectangle returns x*y). So now we have more problem.
4. Solution
Here is a solution: refinement type. By using refinement type, we can
claim type Square = Rectangle when (x = y). Then problem solved, when
programming if we can't proof x = y this predicate then compiler won't
think that is a Square but a Rectangle. Since Square is a
Rectangle, method in Rectangle still can be using by Square, thus
we didn't lose our power. However, program like s.setX(v), would need
to prove v = y, to prove it is a Square. Here we have two choices:
- change
stype toRectangle, the problem of this solution is if we writer = s; r.setX(v), compiler might not work for this(this is also why I'm designing controllable-refinement), mutable semantic always needs more effort. - throw compile error that
Squareconstraint was broke by the statement.
Choose one and work with it, that's all, have a nice day.