# Subtypes in Object-Oriented Languages

Type in an object-oriented language:
A collection of operation signatures, where each signature consists of the operation name, the types of the arguments, and the type of the result(s)
We will say that an object is of an abstract type if it has the properties defined by that type. Abstract types can allow us to do static type checking in an object-oriented language, while preserving the dynamic binding of names to operations. For example, we can statically check that we can invoke method m for some object, even though we don't know which method will be invoked.

## Covariant vs. Contravariant vs. Equivariant Rule

How do we decide when an object of a given type S can be used when an object of type T is expected?

The contravariant rule for subtyping is used in Emerald, Cecil, Trellis/Owl, and other languages.

The covariant rule is used in Eiffel, and in Java for arrays (as a special case).

The equivariant rule is used in Java for everything but arrays. (Also sometimes called the invariant rule.)

#### Contravariant rule:

S is a subtype of T if:

1. S provides all the operations that T does (and maybe some more)
2. For each operation in T, the corresponding operation in S has the same number of arguments and results
3. The types of the results of S's operations are subtypes of the types of the corresponding results of T's operations
4. The types of the arguments of T's operations are subtypes of the types of the corresponding arguments of S's operations (note the reversal of T and S here)
N.B. If S=T, then S is a subtype of T.

#### Covariant rule:

same as above, except for 4:

1. The types of the arguments of S's operations are subtypes of the types of the corresponding arguments of T's operations

#### Equivariant rule:

S is a subtype of T if:

1. S provides all the operations that T does (and maybe some more)
2. For each operation in T, the corresponding operation in S has the same number of arguments and results
3. The types of the results of S's operations are the same as the types of the corresponding results of T's operations
4. The types of the arguments of T's operations are the same as the types of the corresponding arguments of S's operations
Note that in Java, if we have two operations with the the same name and number of arguments, but different types of the arguments, Java views these as two different operations (overloading), rather than as a conflict.

#### Examples

```Type Color

Type GrayScaleColor (a subtype of Color)

Type Number
subtypes Float, Integer
// in this example I'm assuming numbers are full-fledged objects

Type Point
x(): Number
y(): Number

Type ColoredPoint
x(): Number
y(): Number
mycolor() : Color

Type GrayScalePoint
x(): Number
y(): Number
mycolor() : GrayScaleColor
```
Under all of the rules, ColoredPoint is a subtype of Point -- anywhere a Point is needed, we can use a ColoredPoint.

Under the contravariant and covariant rules, GrayScalePoint is a subtype of ColoredPoint Point -- anywhere a ColoredPoint is needed, we can use a GrayScalePoint. However, the equivariant rule says that GrayScalePoint is not a subtype of ColoredPoint, because mycolor has a different signature in the two types.

Example code:

```  p : ColoredPoint;
c : Color
p := new GrayScalePoint();

c := p.mycolor;

q , r : Point;
a : Number;
q := new ColoredPoint();
r := new GrayScalePoint();
a := q.x + r.x;
```
Example with a method with an argument:
```Type Point
x(): Number
y(): Number
setDotSize(c : Integer);

Type ColoredPoint
x(): Number
y(): Number
setDotSize(c : Number);
```
Observe the argument type for setDotSize. The contravariant rule says that ColoredPoint is still a subtype of Point.
```    p1, p2 : Point;
c : ColoredPoint;
p1 := new Point();
c := new ColoredPoint();
p2 := c;   // legal because ColoredPoint is a kind of Point
p1.setDotSize(3);
p2.setDotSize(4);
c.setDotSize(4.5);  // legal because a float is a kind of number
```
However, the following statements would give compile-time errors:
```    p1.setDotSize(3.5);
p2.setDotSize(3.5);  // ok in dynamically typed language
```
However, in a dynamically typed language, the first statement would still fail, but the second would be OK.

Now consider:

```Type ColoredPoint
x(): Number
y(): Number
mycolor() : Color
setcolor(c : Color);

Type GrayScalePoint
x(): Number
y(): Number
mycolor() : GrayScaleColor
setcolor(c : GrayScaleColor);
```
Under the contravariant rule there is no longer a subtype relation between ColoredPoint and GrayScalePoint. Example:
```    c : ColoredPoint;
c := new GrayScalePoint();  /* compile time error */
c.setcolor(yellow);  /* an error would occur if we tried this */
```

However, under the covariant rule GrayScalePoint would still be a subtype of ColoredPoint, and the above program would type check correctly, and in the absence of a runtime type check, would lead to errors.

### Java Examples

```    class Point {
public int x;
public int y;
}

class ColoredPoint extends Point {
public Color mycolor;
}

interface PointMaker {
Point makePoint();
}

interface PointEater {
void eat(Point p);
}

interface ColoredPointMaker {
ColoredPoint makePoint();
}

interface ColoredPointEater {
void eat(ColoredPoint p);
}
```
The following alternate declaration for ColoredPointMaker would be illegal:
```    interface ColoredPointMaker extends PointMaker {
ColoredPoint makePoint();
}
```
The following alternate declaration for ColoredPointEater is OK, and says that a ColoredPointEater must provide two different eat methods:
```    interface ColoredPointEater extends PointEater {
void eat(ColoredPoint p);
}
```
Both these declarations are legal:
```    class PtMaker1 implements PointMaker {
Point makePoint() {
return new Point();
}
}
class PtMaker2 implements PointMaker {
Point makePoint() {
return new ColoredPoint();
}
}
```
The following is illegal under Java's equivariant type rule. (It would be legal under the covariant and contravariant rules.)
```    class PtMaker3 implements PointMaker {
ColoredPoint makePoint() {
return new ColoredPoint();
}
}
```
The following is also illegal under Java's equivariant type rule. (It would be legal under the contravariant rule, but not the covariant rule. It would be type safe.)
```    class Eater1 implements ColoredPointEater {
void eat (Point p) {
}
}
```
Finally, the following is illegal under Java's equivariant type rule. (It would be legal under the covariant rule, but not the contravariant rule. It would not be type safe unless there were a runtime check.)
```    class Eater2 implements PointEater {
void eat (ColoredPoint p) {
}
}
```

### Java Arrays and Subtyping

Subtyping with arrays:

if X extends Y then also X[] extends Y[]

This version of the subtyping relation uses the covariant rule, and is actually unsound! So Java introduces a runtime check, as described in the Notes on Pizza.