# 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
`s`

type to`Rectangle`

, the problem of this solution is if we write`r = 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.