Skip to content

Lecture 10.2: More Type Systems

Recap

Last lecture, we had begun a discussion of what types are, how they intersect with logic, and we had begun adding types to our language. Today we will complete the type checker and begin to see what other statements we can make about programs without running them.

Bringing back our type-checker, we had just about added the types and begun to evaluate type inference: 

type op = | Add | Mul | And | Or | LT | EQ

type value =
  | Nat of int
  | Bool of bool

type expr =
  | Value of value
  | Var of string
  | Let of string * expr * expr
  | ITE of expr * expr * expr
  | App of op * expr list

type ty =
  | TNat
  | TBool

We wanted to write the following function typeof, and we had covered variables and let-binders

let rec typeof (ctx : ty_env) (e : expr) : ty option = ...
  match e with
  | Value (Nat _) -> Some TNat
  | Value (Bool _) -> Some TBool
  | Var x -> StrMap.find_opt x ctx
  | Let(x, e1, e2) ->
    (match typeof ctx e1 with
        | None -> None
        | Some t -> 
            let ctx = StrMap.add x ty ctx in
            typeof ctx e2)
  | ITE(g, t, f) -> ...
  | App (op, args) -> ...

If-then-else expressions are next. How should we handle programs that look like the following:

(if true then 10 else false) : ???
(if x then 10 else false) : ???
(if x then y else z) : ???

the key idea is that the guard (x above) must be a boolean, and y and z must have the same type. We can implement this directly:

  | ITE(g, t, f) ->
     (match typeof ctx g with
     | TNat -> None
     | TBool ->
       (match (typeof ctx t, typeof ctx f) with
         (Some tt, Some tf) -> if tt = tf then Some tt else None
         _ -> None))

Now, how to handle App? Let's remember how we handled it via evaluation. If we have App(op, args), we first evaluated all the subexpressions, to create a value list; then, we used a helper function eval_op : op -> value list -> value to evaluate the operation.

We will do the same to type check an App: 

  | App(op, args) -> type_of_op op (List.map (fun (e) -> type_of ctx e) args)

The idea here is that we are abstracting over specific values (like 1, 2, 3) with their types which looks precisely like the function signature. With this in mind, we can define type_of_op as 

let type_of_op (op : op) (args : (ty option) list) : ty option =
  match (op, args) with
  (Add, [Some TNat; Some TNat]) -> Some TNat
  (Mul, [Some TNat; Some TNat]) -> Some TNat
  (And, [Some TBool; Some TBool]) -> Some TBool
  (Or, [Some TBool; Some TBool]) -> Some TBool
  (LT, [Some TNat; Some TNat]) -> Some TBool
  (Not, [Some TBool]) -> Some TBool
  (EQ, [Some TNat; Some TNat]) -> Some TBool
  (EQ, [Some TBool; Some TBool]) -> Some TBool

  _ -> None

The rules for typing the operators are, in a sense, just "abstracted" versions of how they behave on values. For example, since we happen to know that App(Add, [e1; e2]) will always evaluate to a Nat if e1 and e2 evaluate to a Nat, then we can assign Add the corresponding typing rule. Our calculator language doesn't have first-class functions, but this rule for Add is something similar to TNat -> TNat -> TNat.

Type Soundness

Yesterday we motivated the discussion of types with an informal statement about the semantics and syntax of the program: "well typed programs don't crash." We said that this idea is something labelled type soundness and it informs us that types specify semantically valid program.

Now, as we discussed before, a type in our language can be thought of as represented by a mathematical set of values. So we can additionally write out this function: 

let interpret_ty (ty : ty) : value -> bool =
  match ty with 
  | TNat -> (fun v -> match v with  | Nat _ -> true  | Bool _ -> false)
  | TBool -> (fun v -> match v with | Nat _ -> false | Bool _ -> true)
For any type t and value v, interpret_ty t v returns true only if v is in the set of values that corresponds to t.

This allows us to finally state type soundness. We will just do so for closed programs (those which don't have unbound variables):

Given an e : expr,

  • If typeof StrMap.empty e = Some _, then eval StrMap.empty e won't crash; and
  • If typeof StrMap.empty e = Some t, then interpret_ty t (eval StrMap.empty e) = true.

Static Analysis

What we are doing with type checking is a form of static analysis: a way of analyzing code without running it. Our static analysis currently is quite simple. For example, we can now prove that e := (if false then 23 else 2 + 2) will always evaluate to a natural number. Why? Because typeof will assign it the type TNat; and via type soundness, this means interpret_ty TNat (eval StrMap.empty e) must hold.

While this is already quite useful (it is how OCaml works!) we can now extend it to handle more interesting properties. Right now, what does our type system say about addition? It only says the following:

  • If a is a TNat and b is a TNat, then a + b is a TNat.

But we know many more properties about addition. For example, how it works on even and odd natural numbers:

  • If a is even and b is even, a + b is even;
  • If a is even and b is odd, a + b is odd;
  • If a is odd and b is even, a + b is odd;
  • If a is odd and b is odd, a + b is even.

We can do the same for multiplication:

  • If a or b is even, then a * b is even; and
  • If a and b are both odd, then a * b is odd.

By enumerating the cases like above, we can derive a way to apply type checking to analyzing even/odd numbers. The way to do so is to split the type TNat into three types: a type for Even, a type for Odd, and a type for Any (both even or odd). We do so by keeping TNat, but adding a notion of kind:

type ty =
  | TNat of kind
  | TBool
and kind = | Any | Even | Odd

Thus, the set of all natural numbers is now TNat Any; while the sets of even and odd natural numbers is TNat Even and TNat Odd, respectively.

Given this new grammar of types, we can now repeat the exercise of thinking about how we should assign types to expressions. As it so happens, the rules for variables and let bindings stay exactly the same. Now, starting with values:

0 : TNat Even
1 : TNat Odd
52 : TNat Even
false : bool

As we can see, for values, we don't need to actually use the type TNat Any. Since we have the precise value, we can just compute mod 2 and see if it is even or odd!

Next, let's do if-then-else. What type should this have below? Assume b is a boolean that is in the typing environment.

if b then 0 else 2 : TNat Even

What about this?

if b then 1 else 3 : TNat Odd

Ok. What about this?

if b then 0 else 3 : TNat Any

Why did we get TNat Any? The left-hand side has type TNat Even, while the right-hand side has type TNat Odd. Our old rules for type checking would actually reject this program, because the types aren't equal. But this is of course overly pessimistic; we know it should type check, but just type check with the Any annotation.

The idea for type checking if-then-else is we need to unify the two types to find a type that captures both sides. How we do the unification is we find the "best" type that is a superset of the two types on either side:

let unify_type (t1 : ty) (t2 : ty) : ty option = 
  match t1, t2 with
   | TNat Even, TNat Even -> Some (TNat Even)
   | TNat Odd, TNat Odd -> Some (TNat Odd)
   | TNat _, TNat _ -> Some (TNat Any) (* In the two other cases *)
   | TBool, TBool -> Some TBool
   | _, _ -> None

This means our typing for if-then-else will now look like this:

  | ITE (g, t, f) ->
    (match typeof ctx g with
    | Some TBool ->
      (match (typeof ctx t, typeof ctx f) with
      | Some t1, Some t2 -> unify_type t1 t2
      | _, _ -> None)
    | _ -> None)

If the guard has type TBool, and type checking succeeds on the two branches, then we try to unify the two branches. If unification succeeds, we return the unified type; in all other cases, we return None.

Checking Operators

Next, we need to abstract our operators from working on naturals, to additionally working on these new types. Let's formalize our intuition for Even, Odd, and Any: 

Addition:
  Even + Even = Even
  Even + Odd  = Odd
  Odd + Even  = Odd
  Odd + Odd   = Even
  _   + Any   = Any
  Any + _     = Any

The two extra cases for Any represent the fact that when I add a natural number to something of type TNat Any, I don't know whether it's even or odd; thus, the best I can do is say that I don't know what the result is either, other than it's a natural number.

We can build a similar table for multiplication 

Multiplication:
  Even * Even = Even
  Even * Odd  = Even
  Odd  * Even = Even
  Odd  * Odd  = Odd
  Any  *   _  = Any
  _    * Any  = Any

We can now formalize these tables into OCaml:

Let's begin by encoding the above properties of our arithmetic operators on even and odd numbers. 

let add_kinds (lhs : kind) (rhs : kind) :  kind =
  match (lhs, rhs) with
  | (Even, Even) -> Even
  | (Even, Odd)  -> Odd
  | (Odd , Even) -> Odd
  | (Odd , Odd)  -> Even
  | _  -> Any

let mul_kinds (lhs : kind) (rhs : kind) :  kind =
  match (lhs, rhs) with
  | (Even, Even) -> Even
  | (Even, Odd)  -> Even
  | (Odd , Even) -> Even
  | (Odd , Odd)  -> Odd
  | _  -> Any

We now can adapt our type_of_op function accordingly: 

let type_of_op (op : op) (args : ty option list) : ty option =
  match (op, args) with

  | (Add, [Some (TNat s1); Some (TNat s2)]) -> Some (TNat (add_kinds s1 s2))
  | (Mul, [Some (TNat s1); Some (TNat s2)]) -> Some (TNat (mul_kinds s1 s2))

  | (And, [Some TBool; Some TBool])       -> Some TBool
  | (Or , [Some TBool; Some TBool])       -> Some TBool
  | (LT , [Some (TNat _); Some (TNat _)]) -> Some TBool
  | (EQ , [Some e1; Some e2])             -> Some TBool

  | _                                     -> None

The rest of the type checker looks the same as before, adjusting as appropriate for each TNat type: 

type ty_env = ty StrMap.t
let rec typeof (ctx : ty_env) (e : expr) : ty option =
  match e with
The main change is that when we statically analyze a known value, we annotate it as, not only a nat, but also as Even or Odd depending on the value we see: 
  | Value (Nat n) -> Some (TNat (if (n mod 2) = 0 then Even else Odd))

The rest of the code is the same as before:

  | Value (Bool _) -> Some TBool
  | Var x -> StrMap.find_opt x ctx
  | Let (x, e1, e2) ->
    (match typeof ctx e1 with
    | None      -> None
    | Some t1   ->
      let ctx = StrMap.add x t1 ctx in
      typeof ctx e2)
    | _ -> None)
  | App (op, args) -> typeof_op op (List.map (typeof ctx) args)

For the full file, please see 10.2.ml.