10.1.3.1 Typing Contexts🔗

For example, x:Int, y:Bool, z:Int is a context where x and z have type Int and y has type Bool.

Intuition: if expression e has free variables x, y, z, we need a context G that assigns types to at least those variables. Without such a context, we cannot type-check e. For example, the expression

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

requires a context G mapping x, y, and z to Int.

When G is empty, we write ⊢ e : t (omitting G).

10.1.4.1 Booleans🔗

Boolean constants always have type Bool, regardless of context:

\frac{}{G \vdash \texttt{true} : \texttt{Bool}} \qquad \frac{}{G \vdash \texttt{false} : \texttt{Bool}}

match e with
| Bool _ -> TBool

10.1.4.2 Integers🔗

Integer constants always have type Int, regardless of context:

\frac{}{G \vdash n : \texttt{Int}}

match e with
| Int _ -> TInt

10.1.4.3 Variables🔗

A variable x has whatever type the context assigns to it:

\frac{}{G \vdash x : G(x)}

This corresponds to looking up x in the typing context, just as evaluation looks up x in the runtime environment.

match e with
| ID x -> lookup gamma x

10.1.4.4 Binary Operators🔗

\frac{G \vdash e_1 : t_1 \quad G \vdash e_2 : t_2 \quad \text{optype}(\mathit{op}) = (t_1, t_2, t_3)} {G \vdash e_1\; \mathit{op}\; e_2 : t_3}

So e1 op e2 has type t3 when e1 has type t1, e2 has type t2, and op takes t1 × t2 and returns t3.

match e with
| Binop (Add, e1, e2) | Binop (Sub, e1, e2) | Binop (Mult, e1, e2) ->
    if typecheck e1 = TInt && typecheck e2 = TInt then TInt
    else raise TypeError
| Binop (Greater, e1, e2) | Binop (Less, e1, e2)
| Binop (GreaterEqual, e1, e2) | Binop (LessEqual, e1, e2) ->
    if typecheck e1 = TInt && typecheck e2 = TInt then TBool
    else raise TypeError
| Binop (Equal, e1, e2) | Binop (NotEqual, e1, e2) ->
    if typecheck e1 = typecheck e2 then TBool else raise TypeError
| Binop (And, e1, e2) | Binop (Or, e1, e2) ->
    if typecheck e1 = TBool && typecheck e2 = TBool then TBool
    else raise TypeError

10.1.4.5 eq0 and Conditionals🔗

For eq0 (test if integer equals zero):

\frac{G \vdash e : \texttt{Int}} {G \vdash \texttt{eq0}\; e : \texttt{Bool}}

match e with
| Eq0 e1 -> if typecheck e1 = TInt then TBool else raise TypeError

For if expressions, the condition must be Bool and both branches must have the same type:

\frac{G \vdash e_1 : \texttt{Bool} \quad G \vdash e_2 : t \quad G \vdash e_3 : t} {G \vdash \texttt{if}\; e_1\; \texttt{then}\; e_2\; \texttt{else}\; e_3 : t}

Note that e2 and e3 must have exactly the same type t. This is why if true then 0 else false is ill-typed in OCaml.

match e with
| If (cond, e1, e2) ->
    if typecheck cond = TBool then
      if typecheck e1 = typecheck e2 then typecheck e1
      else raise TypeError
    else raise TypeError

10.1.4.6 Let🔗

\frac{G \vdash e_1 : t_1 \quad G, x{:}t_1 \vdash e_2 : t_2} {G \vdash \texttt{let}\; x = e_1\; \texttt{in}\; e_2 : t_2}

If e1 has type t1, then we extend the context with x:t1 and type-check e2 in that extended context. The whole expression has type t2, the type of the body.

match e with
| Let (x, e1, e2) ->
    let t = typecheck e1 in
    let _ = Hashtbl.add gamma x t in
    typecheck e2

10.1.4.7 Functions🔗

Since the function fun x:t1 → e declares the argument type explicitly, we extend the context with x:t1 and type-check the body e:

\frac{G, x{:}t_1 \vdash e : t_2} {G \vdash \texttt{fun}\; x{:}t_1 \to e : t_1 \to t_2}

If the body has type t2 under the assumption that x:t1, then the function has type t1 → t2.

match e with
| Fun (x, t, e1) ->
    let _ = Hashtbl.add gamma x t in
    let t' = typecheck e1 in
    TArrow (t, t')

10.1.4.8 Function Application🔗

\frac{G \vdash e_1 : t_1 \to t_2 \quad G \vdash e_2 : t_1} {G \vdash e_1\; e_2 : t_2}

If e1 has function type t1 → t2 and the argument e2 has type t1, then the application e1 e2 has type t2.

match e with
| App (f, arg) -> (
    let f_type = typecheck f in
    let arg_type = typecheck arg in
    match f_type with
    | TArrow (t0, t1) -> if arg_type = t0 then t1 else raise TypeError
    | _ -> raise TypeError)

10.1.4.9 Records and Field Selection🔗

For record construction:

\frac{G \vdash e_1 : t_1 \quad \cdots \quad G \vdash e_n : t_n} {G \vdash \{l_1 = e_1, \ldots, l_n = e_n\} : l_1{:}t_1,\ldots,l_n{:}t_n}

For field selection e.l_i:

\frac{G \vdash e : \{l_1{:}t_1,\ldots,l_n{:}t_n\}} {G \vdash e.l_i : t_i}

match e with
| Record lst -> TRec (List.map (fun (l, e) -> (l, typecheck e)) lst)
| Select (lbl, e) -> (
    match typecheck e with
    | TRec lst -> List.assoc lbl lst
    | _ -> raise TypeError)

10.1.4.10 Full Typechecking Code🔗

typecheck.ml

type op =
  | Add
  | Sub
  | Mult
  | Div
  | Concat
  | Greater
  | Less
  | GreaterEqual
  | LessEqual
  | Equal
  | NotEqual
  | Or
  | And

type var = string
type label = Lab of var

type exptype =
  | TInt
  | TBool
  | TArrow of exptype * exptype
  | TRec of (label * exptype) list
  | TBottom

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

exception TypeError

let gamma = Hashtbl.create 1367
let lookup = Hashtbl.find

let rec typecheck e =
  match e with
  (* lookup returns the first mapping of x in gamma *)
  | ID x -> lookup gamma x
  | Int _ -> TInt
  | Bool _ -> TBool
  | Binop (Add, e1, e2) | Binop (Sub, e1, e2) | Binop (Mult, e1, e2) ->
      if typecheck e1 = TInt && typecheck e2 = TInt then TInt
      else raise TypeError
  | Binop (Equal, e1, e2) ->
      if typecheck e1 = typecheck e2 then TBool else raise TypeError
  | Binop (And, e1, e2) | Binop (Or, e1, e2) ->
      if typecheck e1 = TBool && typecheck e2 = TBool then TBool
      else raise TypeError
  | Not e1 -> if typecheck e1 = TBool then TBool else raise TypeError
  | If (cond, e1, e2) ->
      if typecheck cond = TBool then
        if typecheck e1 = typecheck e2 then typecheck e1 else raise TypeError
      else raise TypeError
  | Fun (x, t, e1) ->
      let _ = Hashtbl.add gamma x t in
      let t' = typecheck e1 in
      TArrow (t, t')
  | App (f, arg) -> (
      let f_type = typecheck f in
      let arg_type = typecheck arg in
      match f_type with
      | TArrow (t0, t1) -> if arg_type = t0 then t1 else raise TypeError
      | _ -> raise TypeError)
  | Let (x, e1, e2) ->
      let t = typecheck e1 in
      let _ = Hashtbl.add gamma x t in
      typecheck e2
  | Record lst -> TRec (List.map (fun (l, e) -> (l, typecheck e)) lst)
  | Select (lbl, e) -> (
      match lbl with
      | Lab _x -> (
          match typecheck e with
          | TRec lst -> List.assoc lbl lst
          | _ -> raise TypeError))
  | _ -> raise TypeError

For example,

typecheck (Let ("x", Int 3, Binop (Add, ID "x", Int 1)))

typecheck (Let ("x", Bool true, Binop (Add, ID "x", Int 1)))

10.1.7.1 Soundness and completeness:🔗

• Soundness: if a term type-checks, its execution will be well-defined. Type safety is a soundness property.

• Completeness: if a term is well-defined, it type-checks. Static type systems are rarely complete — consider if true then 0 else 4+"hi": the else branch is unreachable, so the program is well-defined, but OCaml rejects it because the branches have different types.

• Dynamic type systems are often complete: all expressions are well-defined (possibly raising a runtime exception), and all expressions have the static type Dyn.

Another way to think about it: soundness means the type checker never approves something unsafe — no false negatives at runtime. Completeness means the type checker never rejects something safe — no false rejections. The tradeoff:

Static type systems give up completeness to provide stronger guarantees — ruling out type errors entirely, not just ensuring well-defined behavior. As shown above, you cannot have all three of termination, soundness, and completeness simultaneously.

10.1.9.1 Claim 1: Convenience🔗

Dynamic is more convenient: Dynamic typing lets you build a heterogeneous list or return "a number or a string" without workarounds:

(* 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]

Static is more convenient: With static types, you can assume data has the expected type without cluttering code with runtime checks or having errors far from the logical mistake:

(* 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

10.1.9.2 Claim 2: Expressiveness🔗

Static prevents useful programs: Any sound static type system forbids some programs that do nothing wrong. A program like:

(* 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 *)

Static always has workarounds: Rather than paying the time, space, and late-error costs of tagging everything, statically typed languages let programmers "tag as needed." Ruby tags everything implicitly (uni-typed); OCaml lets you tag explicitly only where needed:

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")

10.1.9.3 Claim 3: Bug Detection🔗

Static catches bugs earlier: Static typing catches many simple bugs at compile time. Since such bugs are always caught, there is no need to test for them; you can "lean on" the type-checker:

(* 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 *)

Static catches only easy bugs: Static typing often catches only "easy" bugs. You still need to test your functions, and tests should find those bugs too:

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

The type checker was no help here — the logic error is invisible to it.

10.1.9.4 Claim 4: Performance🔗

10.1.9.5 Claim 5: Code Reuse🔗

Code reuse easier with dynamic: Without a restrictive type system, more code can be reused with data of different types. If you use cons cells for everything, libraries that work on cons cells are universally useful. Collections libraries are amazingly useful but often require complicated static types — polymorphism and generics are hard to understand, but they are trying to provide what dynamic typing gives naturally.

Code reuse easier with static: The type system serves as "checked documentation", making the contract with others’ code easier to understand and use correctly. Signatures tell you exactly what a function expects and returns.

10.1.9.6 The Age-Old Debate🔗

Static vs. dynamic typing is ultimately too coarse a question. A better question is: what should we enforce statically? For example, OCaml checks array bounds and division-by-zero at run time, not statically — these are legitimate trade-offs.

There is ongoing research into gradual typing: flexible languages that allow static types in some parts of the program and dynamic checking in others (e.g., TypeScript, Pyret, Typed Racket). Whether programmers use such flexibility well is an open question.

10.2.5.1 Width Subtyping🔗

A record with more fields is a subtype of a record with fewer fields. Intuitively, the type {x:Nat} describes "all records that have at least a field x of type Nat." A record with more fields satisfies a more demanding specification — it belongs to a smaller set of values, making it a subtype.

\{l_i : T_i^{\;i \in 1..n+k}\} <: \{l_i : T_i^{\;i \in 1..n}\} \quad (S-RcdWidth)

10.2.5.2 Depth Subtyping🔗

It is also safe to allow the types of individual fields to vary, as long as corresponding field types are in the subtype relation:

\frac{\text{for each}\; i \quad S_i <: T_i} {\{l_i : S_i^{\;i \in 1..n}\} <: \{l_i : T_i^{\;i \in 1..n}\}} \quad (S-RcdDepth)

Example: {x:{a:Int, b:Int}, y:{m:Int}} <: {x:{a:Int}, y:{}}

10.2.5.3 Permutation Subtyping🔗

The order of fields in a record does not affect how we can safely use it — the only thing we can do with a record is project its fields, which is order-insensitive:

\frac{\{k_j : S_j^{\;j \in 1..n}\}\; \text{is a permutation of}\; \{l_i : T_i^{\;i \in 1..n}\}} {\{k_j : S_j^{\;j \in 1..n}\} <: \{l_i : T_i^{\;i \in 1..n}\}} \quad (S-RcdPerm)

Note: S-RcdPerm, combined with S-Trans and S-RcdWidth, lets us drop fields from anywhere in a record, not just at the end.

10.2.5.4 Subtyping Derivation Example🔗

Using S-RcdWidth and S-RcdDepth together, we can derive:

                    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.3.4.1 A Simple Type Inference Example🔗

simple_type_infer.ml

type exptype =
  | TInt
  | TBool
  | TArrow of exptype * exptype
  | Guess_t of int * exptype option ref

type op = Add | Sub | Mult | Equal | NotEqual
type var = string

type expr =
  | Int of int
  | Binop of op * expr * expr
  | Bool of bool
  | If of expr * expr * expr
  | ID of var
  | Fun of var * expr
  | App of expr * expr
  | Let of var * expr * expr

type 'a env = (var * 'a) list

exception TypeError of string

let error (s : string) = raise (TypeError s)
let extend (env : 'a env) (x : var) (v : 'a) : 'a env = (x, v) :: env

let rec lookup (env : 'a env) (x : var) : 'a =
  match env with
  | [] -> error ("unbound variable " ^ x)
  | (y, v) :: rest -> if x = y then v else lookup rest x

let fresh_guess =
  let guess_counter = ref 0 in
  fun () : exptype ->
    let c = !guess_counter in
    guess_counter := c + 1;
    Guess_t (c, ref None)

(* path compression -- compress a path of constrained guesses, so that 
     the guess refers to the most constrained type. *)
let rec compress (t : exptype) : exptype =
  match t with
  | Guess_t (_, ({ contents = Some t' } as r)) ->
      let t'' = compress t' in
      r := Some t'';
      t''
  | Guess_t (_, { contents = None }) | TInt | TBool | TArrow (_, _) -> t

let rec string_of_exptype t =
  match compress t with
  | TInt -> "int"
  | TBool -> "bool"
  | TArrow (t1, t2) ->
      "(" ^ string_of_exptype t1 ^ "->" ^ string_of_exptype t2 ^ ")"
  | Guess_t (i, { contents = None }) -> Printf.sprintf "?%d" i
  | Guess_t (_, { contents = Some t }) -> string_of_exptype t

(* occurs check -- determine if a guess is in a type *)
let rec occurs (r : exptype option ref) (t : exptype) : bool =
  match t with
  | Guess_t (_, r') -> r == r'
  | TArrow (t1, t2) -> occurs r t1 || occurs r t2
  | TInt | TBool -> false

let rec unify (t1 : exptype) (t2 : exptype) : unit =
  if t1 == t2 then ()
  else
    match (compress t1, compress t2) with
    | Guess_t (_, ({ contents = None } as r)), t
    | t, Guess_t (_, ({ contents = None } as r)) ->
        if occurs r t then
          error
            (Printf.sprintf "occurs check failed:  %s <> %s"
               (string_of_exptype t1) (string_of_exptype t2))
        else r := Some t
    | TArrow (t1a, t1b), TArrow (t2a, t2b) ->
        unify t1a t2a;
        unify t1b t2b
    | TBool, TBool -> ()
    | TInt, TInt -> ()
    | t1, t2 ->
        error
          (Printf.sprintf "unify failure: %s <> %s" (string_of_exptype t1)
             (string_of_exptype t2))

let rec infer (e : expr) (env : exptype env) : exptype =
  match e with
  | Int _ -> TInt
  | Bool _ -> TBool
  | ID x -> lookup env x
  | Binop (Add, e1, e2) | Binop (Sub, e1, e2) | Binop (Mult, e1, e2) ->
      unify (infer e1 env) TInt;
      unify (infer e2 env) TInt;
      TInt
  | Binop (Equal, e1, e2) | Binop (NotEqual, e1, e2) ->
      unify (infer e1 env) (infer e2 env);
      TBool
  | If (e1, e2, e3) ->
      unify (infer e1 env) TBool;
      let t2 = infer e2 env in
      let t3 = infer e3 env in
      unify t2 t3;
      t2
  | Let (x, e1, e2) -> infer e2 (extend env x (infer e1 env))
  | Fun (x1, e1) ->
      let g = fresh_guess () in
      TArrow (g, infer e1 (extend env x1 g))
  | App (e1, e2) ->
      let t1 = infer e1 env in
      let t2 = infer e2 env in
      let g = fresh_guess () in
      unify t1 (TArrow (t2, g));
      g

(* 3 + 4*2 *)
let e1 = Binop (Add, Int 3, Binop (Mult, Int 4, Int 2))
let e2 = Binop (Equal, Int 3, Binop (Mult, Int 4, Int 2))
let e3 = If (Bool true, Int 3, Int 4)
let e4 = Let ("x", Int 1, Binop (Add, Int 10, ID "x"))
let e5 = Let ("f", Fun ("x", Binop (Add, Int 3, ID "x")), App (ID "f", Int 4))
let e6 = Fun ("x", Fun ("y", If (ID "x", ID "y", Bool false)))
let e7 = Fun ("x", Fun ("y", If (ID "x", Bool true, ID "y")))
let e8 = Fun ("x", ID "x")

(* let polymorphism 

let f = fun x->x in f ( (f 1) = 5)

*)
let e9 =
  Let
    ( "f",
      Fun ("x", ID "x"),
      App (ID "f", Binop (Equal, Int 5, App (ID "f", Int 1))) )

let e10 = Fun ("x", Binop (Add, Int 2, ID "x"))
let e11 = Fun ("f", App (ID "f", Int 2))
let e12 = Fun ("x", Binop (Add, ID "x", ID "x"))
let e13 = App (e11, e12)
let () = print_endline (string_of_exptype (infer e13 []))

10.3.4.2 Constraint Generation🔗

Constraint generation traverses the AST. At each node it assigns fresh type variables to unknowns and emits constraints derived from the typing rules. The constraints are then solved by unification.

Example 1: fun x → 2 + x

(* Fun node: assign fresh 'a to x, infer body with x:'a in context *)
let 'a = fresh () in
let t_body = infer (2 + x) (env[x := 'a]) in
(* result *) TArrow ('a, t_body)

(* Binop node (2 + x): + requires both sides to be Int *)
unify (infer 2 env) TInt;    (* TInt = TInt — ok *)
unify (infer x env) TInt;    (* 'a = TInt  — constraint: 'a := Int *)
(* result *) TInt

After solving: ’a = Int, so t_body = Int and the function has type Int → Int.

Example 2: fun f → f 2 (polymorphic)

(* Fun node: assign fresh 't to f, infer body with f:'t in context *)
let 't = fresh () in
let t_body = infer (f 2) (env[f := 't]) in
(* result *) TArrow ('t, t_body)

(* App node (f 2): infer types of f and 2, introduce fresh 'r for result *)
let t1 = infer f env in   (* t1 = 't *)
let t2 = infer 2 env in   (* t2 = Int *)
let 'r = fresh () in
unify t1 (TArrow (t2, 'r));  (* 't = Int → 'r — constraint: 't := Int → 'r *)
(* result *) 'r

After solving: ’t = Int → ’r, so the function has type (Int → ’r) → ’r, written (Int → ’a) → ’a with a generic type variable.