Overview
- what is Subtyping?
- what is Liskov Substitution Principle?
- what's the problem?
- how to solve this mistake of type system
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
.
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
What's the problem
Square is a special Rectangle where all four sides are equal in length. Thus we might write down:
public 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.
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
s
type 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
Square
constraint was broke by the statement.
Choose one and work with it, that's all, have a nice day.
Top comments (0)