12 Subtyping
So far in class we’ve explored parametric polymorphism and System-F as a means of achieving polymorphic behavior in programs. There is one other significant form of polymorphism that you are surely familiar with: inheritance, which we will briefly discuss in this lecture.
12.1 Inheritance
Consider the following small class hierarchy of animals in Java:
class Animal { |
void eat() { |
System.out.println("Animal is eating."); |
} |
} |
|
class Dog extends Animal { |
void bark() { |
System.out.println("Dog is barking."); |
} |
} |
|
class Cat extends Animal { |
void meow() { |
System.out.println("Cat is meowing."); |
} |
} |
In type systems with subtyping, some types are more informative than others. For instance, in the above hierarchy, we know that all Cats are Animals, but not vice versa. So, we say Cat is a subtype of Animal, and we write this using the notation Cat <: Animal. The symbol <: is called the subtype relation: it relates two types. The general principle of safe subtyping is that if S <: T, it should be the case that it is safe to use S whenever one would use T; this is called the principle of safe substitution.
For example, in the following snippet, we make use of the variable c of type Cat as if it had type Animal:
public class Main { |
public static void main(String[] args) { |
Cat c = new Cat(); |
animalEat(c); |
} |
|
static void animalEat(Animal a) { |
a.eat(); |
} |
} |
The subtyping relation has some structure that it should adhere to: it is a preorder on types, meaning:
Reflexivity: A type is a subtype of itself: S <: S
Transitivity: If S <: T and T <: W, then S <: W
12.2 An STLC with Inheritance
Let’s make a small simply-typed lambda calculus extended with the above class hierarchy:
> (define-type LType (animalT) (catT) (dogT) (numT) (FunT [arg : LType] [body : LType]))
> (define-type LExp (varE [s : Symbol]) (numE [n : Number]) (animalE [weight : Number]) (catE [weight : Number] [num-fish : Number]) (dogE [weight : Number] [num-bones : Number]) (count-fishE [e : LExp]) (count-bonesE [e : LExp]) (get-weightE [e : LExp]) (lamE [arg : Symbol] [typ : LType] [body : LExp]) (appE [e : LExp] [arg : LExp]))
Here is an interpreter for this lambda calculus:
> (subst : (LExp Symbol LExp -> LExp))
> (define (subst e1 x e2) (type-case LExp e1 [(varE s) (if (symbol=? s x) e2 (varE s))] [(lamE id typ body) (if (symbol=? x id) (lamE id typ body) (lamE id typ (subst body x e2)))] [(appE e1App e2App) (appE (subst e1App x e2) (subst e2App x e2))] [(count-fishE e) (count-fishE (subst e x e2))] [(count-bonesE e) (count-bonesE (subst e x e2))] [(get-weightE e) (get-weightE (subst e x e2))] [else e1])) > (interp : (LExp -> LExp))
> (define (interp e) (type-case LExp e [(varE s) (error 'runtime "unbound symbol")] [(lamE id typ body) (lamE id typ body)] [(numE n) (numE n)] [(appE e1 e2) (letrec [(e1V (interp e1)) (body (lamE-body e1V)) (id (lamE-arg e1V)) (argV (interp e2))] (interp (subst body id argV)))] [(count-bonesE e) (numE (dogE-num-bones (interp e)))] [(count-fishE e) (numE (catE-num-fish (interp e)))] [(get-weightE e) (type-case LExp (interp e) [(catE w f) (numE w)] [(dogE w b) (numE w)] [(animalE w) (numE w)] [else (error 'runtime "invalid get-weight")])] [(animalE w) (animalE w)] [(catE w f) (catE w f)] [(dogE w b) (dogE w b)]))
Let’s follow the type system design recipe to make a type checker for this language. Let’s make some tests, and let’s focus our attention on tests that exercise the new features of the language.
12.2.1 Expressivity Tests
Using a Cat in a position where an Animal is expected:
\texttt{(\texttt{get-weight}~\texttt{(Cat 3 4)})}
From this we can conclude that \texttt{Cat} <: \texttt{Animal}.
Providing a function whose argument is more general than required:
(\lambda x : (\texttt{Cat} \rightarrow \texttt{Num}) . x ~ (\texttt{Cat 2 0})) ~ (\lambda a : \texttt{Animal} . (\texttt{get-weight}~a))
From this, we can conclude that \texttt{Animal} \rightarrow \texttt{Num} <: \texttt{Cat} \rightarrow \texttt{Num}
Providing a function whose return type is more specific than required:
(\lambda x : (\texttt{Num} \rightarrow \texttt{Animal}) . (\texttt{get-weight}~(x ~ 5)) ~ (\lambda w : \texttt{Num} . (\texttt{Cat}~w~0))
From this we can conclude that \texttt{Num} \rightarrow \texttt{Cat} <: \texttt{Num} \rightarrow \texttt{Animal}.
12.2.2 Soundness tests
Calling get-bonesE on a non-dog: (get-bonesE (catE 10 20))
Calling get-fishE on a non-cat: (get-fishE (animalE 10))
Passing an Animal to a function that expects a Cat: (\lambda x : \texttt{Cat} . \texttt{(count-bones x)}) ~ (\texttt{Animal}~4)
Providing a function whose argument is less specific than specified: (\lambda x : (\texttt{Animal} \rightarrow \texttt{Num}) . x ~ (\texttt{Animal} ~ 4)) ~ (\lambda c : \texttt{Cat} . (\texttt{count-bones}~c))
Providing a function whose return value is more specific than specified: (\lambda f : (\texttt{Num} \rightarrow \texttt{Animal}) . ) ~ (\lambda w : \texttt{Num} . (\texttt{Cat}~w~0))
12.2.3 Typing Rules
Some additional useful terminology you may see: we say a subtyping relation is covariant if it preserves the existing ordering of subtypes and contravariant if it reverses it. For instance, consider the function type T_1 \rightarrow T_2.
If S_1 <: T_1, we have that T_1 \rightarrow T_2 <: S_1 \rightarrow T_2, so we say that function type subtyping is contravariant their argument type.
On the other hand, if S_2 <: T_2, we have that T_1 \rightarrow S_2 <: T_1 \rightarrow T_2, so we say that function type subtyping is covariant in return type.
\dfrac{~}{\Gamma \vdash n : \texttt{Num}}~\text{(T-Num)} \dfrac{ x : \tau \in \Gamma}{\Gamma \vdash x : \tau}~\text{(T-Var)} \dfrac{\Gamma, x : \tau_1 \vdash e : \tau_2} {\Gamma \vdash \lambda x : \tau_1 . ~ e : \tau_1 \rightarrow \tau_2}~\text{(T-Abs)} \dfrac{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1} {\Gamma \vdash e_1 ~ e_2 : \tau_2}~\text{(T-App)} \dfrac{\Gamma \vdash e : S \qquad S <: T}{\Gamma \vdash e : T}~\text{(T-Sub)}\dfrac{~}{S~<:~S}~\text{(T-Refl)}\dfrac{T_1 ~ <: ~ S_1 \qquad S_2 ~ <: ~ T_2} {S_1 \rightarrow S_2 ~ <: ~ T_1 \rightarrow T_2}~\text{(T-SubFun)}\dfrac{~}{\texttt{Cat} <: \texttt{Animal}}~\text{(T-SubCat)} \qquad \dfrac{~}{\texttt{Dog} <: \texttt{Animal}}~\text{(T-SubDog)}\dfrac{\Gamma \vdash e : \texttt{Cat}} {\Gamma \vdash (\texttt{count-fish}~e) : \texttt{Num}}~\text{(T-CountFish)}\dfrac{\Gamma \vdash e : \texttt{Dog}} {\Gamma \vdash (\texttt{count-bones}~e) : \texttt{Num}}~\text{(T-CountBones)}\dfrac{\Gamma \vdash e : \texttt{Animal}} {\Gamma \vdash (\texttt{get-weight}~e) : \texttt{Num}}~\text{(T-GetWeight)}\dfrac{~} {\Gamma \vdash (\texttt{Cat}~w~f) : \texttt{Cat}}~\text{(T-Cat)} \quad \dfrac{~} {\Gamma \vdash (\texttt{Dog}~w~b) : \texttt{Dog}}~\text{(T-Dog)}\dfrac{~}{\Gamma \vdash (\texttt{Animal}~w) : \texttt{Animal}}~\text{(T-Animal)}
An example derivation trees using theses typing rules:
\dfrac{\dfrac{ \dfrac{~}{\vdash (\texttt{Cat}~3~4) : \texttt{Cat}}~\text{(T-Cat)} } { \vdash (\texttt{Cat}~3~4) : \texttt{Animal}}~\text{(T-Sub)} } {\vdash (\texttt{get-weight}~(\texttt{Cat}~3~4)) : \texttt{Num}}~\text{(T-GetWeight)}
Notice how the (T-Sub) rule enables us to treat a Cat as if it is an Animal.
12.3 Invariance and a Deficiency in Java
Consider the following Java program:
class Main { |
public static void main(String[] args) { |
String[] strings = new String[2]; |
Object[] objects = strings; |
objects[0] = 12; |
strings[0].charAt(0); |
return; |
} |
} |
This program will compile, meaning that it type checks according to Java’s type checker, but it causes a runtime error! What happened?
In Java, the Object type is a special type that all other types are subtypes of, i.e., for any Java type T, it is the case that T <: Object.
In Java, lists are covariant in their type parameter, so List<A> <: List<B> if A <: B.
This means that we can use subsumption to assign objects = strings; this is simply upcasting.
Then, we can insert any object we want into objects! We insert 12. Then, using the original strings array, we call a function that only a string should have. This is clearly illegal, and causes a runtime error.
The reason Java permits this is historical, and dates back to a period before Java supported type parameters. It’s widely regarded as a flaw in its type system.