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)

Covariant vs. Contravariant vs. Equivariant Rule

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:

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)

Covariant rule:

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:

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

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 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;  

Type Point
  x(): Number
  y(): Number
  setDotSize(c : Integer);

Type ColoredPoint
  x(): Number
  y(): Number
  setDotSize(c : Number);

    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

    p1.setDotSize(3.5);
    p2.setDotSize(3.5);  // ok in dynamically typed language

Now consider:

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

Type GrayScalePoint
  x(): Number
  y(): Number
  mycolor() : GrayScaleColor
  setcolor(c : GrayScaleColor);

    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);
    }

    interface ColoredPointMaker extends PointMaker {
      ColoredPoint makePoint();
    }

    interface ColoredPointEater extends PointEater {
      void eat(ColoredPoint p);
    }

    class PtMaker1 implements PointMaker {
      Point makePoint() {
	 return new Point();
      }
    }
    class PtMaker2 implements PointMaker {
      Point makePoint() {
	 return new ColoredPoint();
      }
    }

    class PtMaker3 implements PointMaker {
      ColoredPoint makePoint() {
	 return new ColoredPoint();
      }
    }

    class Eater1 implements ColoredPointEater {
      void eat (Point p) {
      }
    }

    class Eater2 implements PointEater {
      void eat (ColoredPoint p) {
      }
    }

Java Arrays and Subtyping

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.