10.1.1 Type Systems🔗

A type system is a collection of rules that ascribe types to expressions. The rules prove statements of the form:

e : t

The process of applying these rules is called type checking, or simply typing. Different languages have different type systems, which is why OCaml, Java, Python, and Ruby disagree about what programs are acceptable.

10.1.2 Recall: Inference Rules🔗

Recall from operational semantics that we used inference rules to define the judgment A; e ⇒ v ("expression e evaluates to value v in environment A"). For example, the rule for let:

\frac{A;\, e_1 \Rightarrow v_1 \qquad A,x{:}v_1;\, e_2 \Rightarrow v_2} {A;\; \texttt{let}\; x = e_1\; \texttt{in}\; e_2 \Rightarrow v_2}

We use the same inference rule notation to specify static semantics, i.e., the rules for type checking.

10.1.3 The Type Checking Judgment🔗

The central judgment for type checking is:

G ⊢ e : t

read as "e has type t in context G." We define inference rules for this judgment, one rule per form of expression.

Binop (Add, ID "x", Binop (Add, ID "y", ID "z"))

10.1.4 Type Checking Rules🔗

Our goal is to define inference rules for every form of expression. The MicroOCaml expression type is:

type expr =
    Int of int
  | Bool of bool
  | ID of var
  | Fun of var * exptype * expr
  | Not of expr
  | Binop of op * expr * expr
  | If of expr * expr * expr
  | App of expr * expr
  | Let of var * expr * expr
  | Record of (label * expr) list
  | Select of label * expr

TODO: Add typechecking example

We give one rule for each constructor.

10.1.5 Typing Derivations🔗

Just as evaluation uses derivation trees, type checking produces typing derivations: trees of rule applications that witness why an expression is well-typed.

A typing derivation is a proof that an expression is well-typed in a particular context. The proof consists of a tree of valid rule applications, with no obligations left unfulfilled at the leaves.

Example: Derive the type of fun x:Int → (x+2).

G,x:int ⊢ x:int    G,x:int ⊢ 2:int
-------------------------------------------
G,x:int ⊢ x+2:int
-------------------------------------------
G ⊢ fun x:int → (x+2) : int → int

10.1.6 Type Safety🔗

A well-typed program is one accepted by the language’s type system.

A program goes wrong when the language’s semantics gives no definition for what happens — the behavior is undefined. For example, in C, accessing char buf[4]; buf[4] = ’x’; is undefined behavior. If such a program were to run, anything could happen.

A type-safe language is one in which, for every program:

well-typed ⟹ well-defined

In the famous words of Robin Milner (1978): "Well-typed programs never go wrong." OCaml and Java are type-safe languages. C and C++ are not.

10.1.7 Static vs. Dynamic Type Checking🔗

We can view dynamically typed languages as a degenerate form of static typing: every expression is given the static type Dyn, all operations are permitted on Dyn values, and unsupported operations raise a well-defined runtime exception. In this sense, a dynamically typed language is uni-typed — it has one static type for everything.

10.1.8 Perfect Type System? Impossible🔗

while also trying to eliminate all run-time exceptions such as using an integer as a function, accessing an array out of bounds, or dividing by zero.

Doing so would be undecidable — by reduction to the halting problem. Consider while (...) {...} arr[-1] = 1;. Detecting whether the array access is ever reached is tantamount to proving that the while loop terminates, which is undecidable in general. Every practical type system therefore makes a trade-off, accepting some false positives (rejecting valid programs) in exchange for decidability.

10.1.9 The Debate: Static vs. Dynamic🔗

Having carefully stated the facts, we can now consider the arguments about which approach is better. Each claim has a counterargument — the debate is genuinely unresolved and depends on context.

(* Ruby *)
a = [1, 1.5]

(* OCaml requires an explicit variant type *)
type t = Int of int | Float of float
let a = [Int 1; Float 1.5]

(* Ruby — must guard every argument *)
def cube(x)
  if x.is_a?(Numeric)
    x * x * x
  else
    "Bad argument"
  end
end

(* OCaml — type checker guarantees x is int *)
let cube x = x * x * x

(* Ruby — fine at runtime *)
if e1 then "lady" else [7, "hi"]

(* OCaml — type error: branches have different types *)
if e1 then "lady" else (7, "hi")  (* does not type-check *)

type tort =
    Int of int
  | String of string
  | Cons of tort * tort
  | Fun of (tort -> tort)
  | ...

if e1 then String "lady"
       else Cons (Int 7, String "hi")

(* Ruby — bug not detectable until run *)
def pow(x, y)
  if y == 0 then 1
  else x * pow(y - 1)  (* bug: should be pow(x, y-1) *)
  end
end

(* OCaml — type error caught immediately *)
let pow x y =
  if y = 0 then 1
  else x * pow (y-1)   (* does not type-check *)

(* OCaml — type-checks fine, but wrong! *)
let pow x y =
  if y = 0 then 1
  else x + pow x (y-1)   (* oops: + instead of * *)

10.2.1 The Liskov Substitution Principle🔗

Subtyping formalizes the intuition that "every B is an A" — for example, every Circle or Square is a Shape. This idea was articulated precisely by Barbara Liskov (Turing Award 2008):

Let P(x) be a property provable about objects x of type T. Then P(y) should be true for objects y of type S, where S is a subtype of T.

In other words: if S is a subtype of T, then an S can be used anywhere a T is expected. This is a kind of polymorphism and is the foundation of object-oriented subclassing.

10.2.2 The Subtype Relation🔗

A type S is a subtype of T, written S <: T, when any term of type S can safely be used in a context where a term of type T is expected.

10.2.3 The Subsumption Rule🔗

The bridge between subtyping and typing is the subsumption rule (T-Sub):

\frac{G \vdash e : S \quad S <: T} {G \vdash e : T} \quad (T-Sub)

If e has type S and S <: T, then e also has type T. For example, if we establish {x:Int, y:Int} <: {x:Int}, then any record {x=0, y=1} that has type {x:Int, y:Int} can also be used as type {x:Int}.

10.2.4 Subtyping Is a Preorder🔗

The subtype relation is formalized as a collection of inference rules deriving statements of the form S <: T, pronounced "S is a subtype of T" (or "T is a supertype of S"). The relation must always be a preorder: reflexive and transitive.

Reflexivity (S-Refl):

S <: S \quad (S-Refl)

Transitivity (S-Trans):

\frac{S <: U \quad U <: T} {S <: T} \quad (S-Trans)

These rules follow directly from the principle of safe substitution.

10.2.5 Record Subtyping🔗

Records support three forms of subtyping, corresponding to three independent dimensions of flexibility.

                    S-RcdWidth              S-RcdWidth
{a:Nat,b:Nat} <: {a:Nat}        {m:Nat} <: {}
                                              S-RcdDepth
  {x:{a:Nat,b:Nat}, y:{m:Nat}} <: {x:{a:Nat}, y:{}}

10.2.6 Function Subtyping🔗

Since functions can be passed as arguments to other functions, we also need a subtyping rule for function types.

\frac{T_1 <: S_1 \quad S_2 <: T_2} {S_1 \to S_2 <: T_1 \to T_2} \quad (S-Arrow)

Notice the key asymmetry: the argument types are contravariant (the subtype relation is reversed in the left premise), while the result types are covariant (the relation runs in the same direction).

10.2.7 The Top Type🔗

It is convenient to have a type that is a supertype of every type. We introduce Top:

S <: \texttt{Top} \quad (S-Top)

Top is the maximum element of the subtype relation. Every type is a subtype of Top, but Top itself has no interesting operations. (In Java, Object plays this role.)

10.3.1 Type Checking vs. Type Inference🔗

• Type checking: use declared types to verify correctness.

  let apply (f:('a->'b)) (x:'a):'b = f x

  The programmer supplies all types; the checker verifies them.

• Type inference: infer the most general types that could have been declared, and type-check the code without explicit type annotations.

  let apply f x = f x

  The algorithm discovers that f : ’a -> ’b, x : ’a, and the result is ’b.

10.3.2 History🔗

• 1958: Curry and Feys invented the original type inference algorithm for the simply typed lambda calculus

• 1969: Hindley extended the algorithm to a richer language and proved it always produces the most general type

• 1978: Milner independently developed the equivalent Algorithm W during his work designing ML

• 1982: Damas proved the algorithm is complete

Today, Hindley–Milner type inference is used in ML, OCaml, Haskell, F#, and many other languages.

10.3.3 Basic Idea🔗

For fun f → f (f 3): since f is applied to 3 : Int and also applied to the result of f 3, the result of f 3 must also be Int, so f : Int → Int and the whole expression has type (Int → Int) → Int.

10.3.4 The Type Inference Algorithm🔗

The Hindley–Milner algorithm works in three phases:

• Step 1: Parse — construct the AST

• Step 2: Generate constraints — traverse the AST and emit type constraints from the environment (literals, built-in operators) and from the form of parse tree nodes (application, abstraction, etc.)

• Step 3: Solve constraints — use unification to solve the system of constraints and determine the types of all expressions

(* Fun node *)
x: g = fresh_guess ()
(* g → infer (x+2) (extend env x:g) *)

(* Binop node (x+2): *)
unify (infer x env) TInt;   (* x must be Int *)
unify (infer 2 env) TInt;   (* 2 must be Int *)
TInt                          (* result is Int *)

(* Fun node *)
f: t = fresh_guess ()
(* t → infer (f 2) (extend env f:t) *)

(* App node (f 2): *)
let t1 = infer f env in  (* t1 = t *)
let t2 = infer 2 env in  (* t2 = Int *)
let t3 = fresh_guess () in
unify t1 (t2 → t3);      (* t = Int → t3 *)
t3                         (* result: 'a where t = Int → 'a *)

10.3.5 Unification🔗

Unification is an algorithmic process for solving equations between symbolic expressions (types). Given two type expressions, unification finds a substitution mapping type variables to types that makes them equal.

Unification is used for pattern matching and type inference alike. When the algorithm cannot unify two types, it reports a type error.

10.3.6 Complex Example🔗

Consider:

let square = fun z → z * z in
fun f → fun x → fun y →
if (f x y) then (f (square x) y)
else (f x (f x y))

Final type: (Int → Bool → Bool) → Int → Bool → Bool.

10.3.7 Most General Type (Principal Type)🔗

Type inference produces the most general type (also called the principal type). For example:

let rec map f lst =
  match lst with
    [] -> []
  | hd :: tl -> f hd :: (map f tl)
val map : ('a -> 'b) -> 'a list -> 'b list = <fun>

The inferred type (’a -> ’b) -> ’a list -> ’b list is the most general possible — less general types like (int -> int) -> int list -> int list are all instances of it, obtained by substituting concrete types for the type variables.

10.3.8 Varieties of Polymorphism🔗

10.3.9 Complexity🔗

10.3.10 Summary: Key Points🔗