Type Systems

A type consists of a domain of values plus a set of operations[1]:

type = <domain, operations>

In a typed language expressions and values have types. Expressions produce values when they are evaluated. We expect the type of an expression to be equivalent to the type of value it produces when evaluated.

A type system is a set of primitive types together with a set of rules for introducing new types, and the following functions:

Type getType(Expression e, Context c) {
returns the type of value produced by e
}

boolean equals(Type t1, Type t2) {
return true if t1 is equivalent to t2
}

boolean subType(Type t1, Type t2) {
return true if t1 is a subtype of t2
}

For example, a types system S might contain the primitive types:

number, boolean, and error

as well as the following type introduction rules:

If T1 and T2 are types, then so are:
   T1 -> T2 = { f | domain(f) = T1 && range(f) = T2 }
   T1 x T2 = { (a, b) | a: T1 && b: T2 }
   T[] = { a | a[i]: T }

Type Equivalence

Let's introduce the following abbreviations:

T1 == T2 iff T1 and T2 are literally the same
T1 ~ T2 iff equals(T1, T2)
T1 <: T2 iff subType(T1, T2)
e:T iff T ~ getType(e, c) for some context c

Of course type equivalence satisfies the rules of any equivalence relationship:

T ~ T
T1 ~ T2 implies T2 ~ T1
T1 ~ T2 and T2 ~ T3 implies T1 ~ T3

Type systems can use name or structural equivalence. Structural equivalence in S means two types are equivalent if they have the same structure:

Assume T1 ~ T2 && T3 ~ T4, then
   T1 x T3 ~ T2 x T4
   T2 -> T4 ~ T1 -> T3
   T1[] ~ T2[]

Many type systems allow programmers to name new types in type declarations:

type Point = int x int
type Vector = int x int
type Metric = Vector->int
type Polygon = Point[]

Name equivalence says two types are equivalent if an only if they have the same name. Thus, even though Point and Vector are structurally equivalent, they are not name equivalent.

Subtypes, Inheritance, and Subsumption

If T1 <: T2, then an expression of type T1 can be used in any context where an expression of type T2 is expected. Formally:

e: T1 && T1 <: T2 => e: T2

This is called the Subsumption or Polymorphism Rule.

The Inheritance Rule says:

T1 <: T2 => ops(T1) is a subset of ops(T2)

The subtype relationship satisfies the rules for a partial ordering:

T1 ~ T2, then T1 <: T2
T1 <: T2 and T2 <: T3, then T1 <: T3

Our type system S also satisfy the rules:

boolean <: int

Assume T1 <: T2 && T3 <: T4, then
   T1 x T3 <: T2 x T4
   T2 -> T4 <: T1 -> T3
   T1[] <: T2[]

error <: T for all T

Example: Java

Java types are either primitive, reference, or method types.

The primitive types of Java are:

boolean = {false, true}
char = { '\uXXXX' | 0 <= X <= F }
byte = { n | -2^k <= n < 2^k for k = 8 }
short = { n | -2^k <= n < 2^k for k = 16 }
int = { n | -2^k <= n < 2^k for k = 32 }
long = { n | -2^k <= n < 2^k for k = 64 }
float = { n * 2^m | -2^-k <= n < 2^k, k = 23 && -2^-k <= m < 2^k, k = 8 }
double = { n * 2^m | -2^-k <= n < 2^k, k = 52 && -2^-k <= m < 2^k, k = 11 }

The reference types of Java are array types, interface types, and class types.

Subtypes and Subsumption

Here are the relationships between the primitive types, notice that boolean is incompatible with everything:

byte <: short <: int <: long <: float <: double
char <: int

For the reference types:

T1 extends T2 implies T1 <: T2
T1 implements T2 implies T1 <: T2
T1 <: T2 implies T1[] <: T2[]

Finally, if T1 is a primitive type and T2 is a reference type, then T1 <: T2 is never true, and T2 <: Object is always true.

Example

Of course we can use integers and floats in contexts where doubles are expected:

Math.cos(0);
Math.cos(0L);
Math.cos(.0F);
Math.cos(.0);

Example

Assume the following classes have been declared:

class Aircraft {
   void takeoff() { ... }
   void fly() { ... }
   void land() { ... }
}

class Airplane extends Aircraft { ... }
class Jet extends Airplane { ... }
class Blimp extends Aircraft { ... }
class Helicopter extends Aircraft { ... }

We have the following subclass relationships:

Jet <: Airplane <: Aircraft
Helicopter <: Aircraft
Blimp <: Aircraft

In other words, jets, airplanes, blimps, and helicopters can be used in contexts where aircraft are expected. For example, an array of aircraft can hold jets, airplanes, blimps, and helicopters:

Aircraft[] fleet = new Aircraft[4];
fleet[0] = new Airplane();
fleet[1] = new Helicopter();
fleet[2] = new Blimp();
fleet[3] = new Jet();

Such an array is called a heterogeneous container, because it contains different types of objects. Traversing a heterogeneous array is just like traversing a homogeneous array, because we know each object in the array inherits the methods of its super class:

for(int i = 0; i < 4; i++) {
   fleet[i].takeoff();
   fleet[i].fly();
   fleet[i].land();
}

As another example, the following method has an aircraft parameter:

class Pilot {
   void fly(Aircraft a) {
      a.takeoff();
      a.fly();
      a.land();
   }
   // etc.
}

But we can pass airplane, jet, helicopter, and blimp arguments to this method:

Pilot p = new Pilot();
p.fly(new Airplane());
p.fly(new Jet());
p.fly(new Helicopter());
p.fly(new Blimp());

Example: Eta

Eta extends Zeta by adding a type system. The primitive Eta types are:

undefined, void, boolean, number, type

Assume t1, t2, t3, t4 are types, then so are:

t1 -> t2
t1 x t2, t1 x t2 x t3, t1 x t2 x t3 x t4, etc.

Type Values

We represent these types as objects, which become a new variety of value (see below):

class Type {
   public final static Type UNDEFINED = new Type("undefined");
   public final static Type VOID = new Type("void");
   public final static Type NUMBER = new Type("real");
   public final static Type BOOLEAN = new Type("boolean");
   public final static Type TYPE = new Type("type");
   // etc.
}
class MapType extends Type { ... }
class TupleType extends Type { ... }

We add a new abstract getType() method to the Phrase class:

public abstract class Phrase {
public abstract Type getType(Context c);
// etc.
}

In the case of Commands and Declarations, getType() returns void:

class Command extends Phrase {
public Type getType(Context c) { return Type.VOID; }
// etc.
}

class Declaration extends Phrase {
public Type getType(Context c) { return Type.VOID; }
// etc.
}

The getType() method might be called in any place where type checking is necessary. From the console:

class EtaConsole extends Console {
   public String execute() throws AppError {
      List tokens = Lex.scan(regExp, cmmd);
      Phrase phrase = Phrase.parse(tokens);
      Type type = phrase.getType(context);
      if (type.equals(Type.UNDEFINED)) {
         throw new AppError("Type error");
      }
      return phrase.exec(context);
   }
}

Or during elaboration of a declaration:

class Declaration {
   String symbol;
   Expression init;
   public String elab(Context context) throws AppError {
      Type type = init.getType(context);
      if (type.equals(Type.UNDEFINED)) {
         throw new AppError("Type error");
      }
      Object value = init.eval(context);
      context.put(symbol, value, type);
   }
}

Notice that the type of a symbol, as well as its value, are stored in the context.

Type Expressions

We add type expressions to Eta:

Of course the eval method returns a type object:

class TypeExpression extends Expression {
   public Type getType() { return Type.type; }
   public Object eval(Context context) {
      return appropriate instance of Type class
   }
   // etc.
}

Here's how we declare a new type:

[const vector (tuple number number number)]

Internally, this calls:

Type t = new TupleType(Type.NUMBER, Type.NUMBER, Type.NUMBER);
context.put("vector", t, Type.TYPE);

Declaring Parameters

We need to modify the syntax of expression and command abstracts. Now the type of the parameter must be declared. Here are some examples:

-> [const square (fun (x:number) (* x x))]
done
-> [var x 0]
done
-> [const inc (proc (y:number) {assign x (+ x y)})]
done

Implementing getType()

Of course getType() needs to be defined in every subclass of Expression. For the Literal subclasses, this is easy. For the Symbol subclass, we only look up the type in the environment. For function calls getType() should return the type of the function body. The type of square and proc should respectively be:

number->number
number->void

Type Class Declarations

class Type

public class Type {
   // Eta primitive types:
   public static final Type UNDEFINED = new Type("undefined");
   public static final Type VOID = new Type("void");
   public static final Type NUMBER = new Type("real");
   public static final Type BOOLEAN = new Type("boolean");
   public static final Type TYPE = new Type("type");
   private String name;
   public Type(String nm) { name = nm; }
   public String toString() { return name; }
   // name equivalence:
   public boolean equals(Object other) {
      if (other == null || !other.getClass().equals(getClass()))
         return false;
      Type t = (Type) other;
      return name.equals(t.toString());
   }
   public int hashCode() {
      return toString().hashCode();
   }
}

class MapType

class MapType extends Type {
   private Type domain, range;
   public Type getDomain() { return domain; }
   public Type getRange() { return range; }
   public MapType(Type d, Type r) {
      super("MapType");
      domain = d;
      range = r;
   }
   public String toString() {
      return domain.toString() + " -> " + range.toString();
   }
   // structural equivalence:
   public boolean equals(Object other) {
      if (other == null || !other.getClass().equals(getClass()))
         return false;
      MapType t = (MapType) other;
      return domain.equals(t.getDomain()) &&
            range.equals(t.getRange());
   }
}

class TupleType

class TupleType extends Type {
   private Vector componentTypes;
   public int size() { return componentTypes.size(); }
   public Type getComponentType(int i) {
      return (Type)componentTypes.elementAt(i);
   }
   public TupleType(Collection types) {
      super("TupleType");
      componentTypes = new Vector(types);
   }
   public TupleType(Type t1, Type t2) {
      super("TupleType");
      componentTypes = new Vector();
      componentTypes.add(t1);
      componentTypes.add(t2);
   }
   public TupleType(Type t1, Type t2, Type t3) {
      super("TupleType");
      componentTypes = new Vector();
      componentTypes.add(t1);
      componentTypes.add(t2);
      componentTypes.add(t3);
   }
   public String toString() {
      String result = "(" + getComponentType(0);
      for(int i = 1; i < size(); i++) {
         result += " x " + getComponentType(i);
      }
      return result + ")";
   }
   public boolean equals(Object other) {
      if (other == null || !other.getClass().equals(getClass()))
         return false;
      TupleType t = (TupleType) other;
      if (t.size() != size()) return false;
      for(int i = 0; i < size(); i++) {
         if (getComponentType(i).equals(t.getComponentType(i)))
            return false;
      }
      return true;
   }
}

[1] A domain is a simple set. In these notes I (reluctantly) take an operation to include its implementation.