Skip to content

Lecture 10.1: Introduction to Type Checking

Overview

  • How do types and logic intersect?
  • Adding types to our calculator language

Recap

Last week we started our programming language module where we went over syntax and semantics of programming langauges and we grew a tiny calculator language into something that resembled a more traditional one by introducing control flow and variable binders. Syntax is how a program is represented, and semantics is what the program does.

Last week:

  • we parsed concrete syntax to abstract syntax;
  • we wrote an interpreter which mapped abstract syntax to the program's semantics;
  • and we saw that we could take the abstract syntax and begin to write specifications about our toy languages (like the commutativity of addition).

This last point is crucial and worth repeating: we can actually use programs themselves as data for our logical specifications!

But it wasn't all perfect, some complications arose when we added booleans: we could do silly things like false + false, which we expect to be an error. Ideally, we want our programs that we evaluate to be predictable and one of the key tools we have in reasoning about program behavior before we run it is statically checking the types.

Today, we are going to:

  • dive a little deeper into type checking; and
  • begin building a type checker.

How do types and logic intersect?

We've already seen and benefited a lot from static types in OCaml and think of them as a kind of specification: 

let f (x : int) : int
  = ...

The function signature alone says, "if you give me an int, I will give you an int."

If give a definition to f like

let f (x : int) : int
  = 3 * x

Then we would expect the following code to break the spec and throw a type error.

f("x")

The fundamental purpose of a type system is to ensure that, before we run this code, we will prevent all runtime errors. Thus, if the program type checks, we know we have a semantically valid program. This property (which we will discuss in more detail later) is type soundness: if a program type checks, it is "safe" to evaluate.

Adding Types to the Calculator Language

To begin adding types to the language, we first need to choose what our types are. For right now, our types will be TNat and TBool (the "T" prefix is just our naming convention for types). Why did we choose these types? Looking back to our set of values: 

type value =
  | Nat of int
  | Bool of bool
We see that our values are either natural numbers or booleans. One way to interpret types, in our context, is as a set of values: TNat is the set of values of the form Nat x, and TBool is the set of values of the form Bool b. Thus, we should have right away that constants have their expected types:

true : TBool
false : TBool
0 : TNat
1 : TNat

The next thing to do is to move from values having types to expressions having types. For example:

(true && false) : TBool
let x = true in x && false : TBool
let x = 42 in if x > 0 then true else false : TBool

We are guaranteed, via typing, that all of these programs evaluate to booleans. The purpose of typing is that, no matter how complicated the expression is, if it has type TBool, then it should evaluate to a boolean value.

Implementing the Type Checker

Let's now recall our language:

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

Our values are exactly the representatives values of our types that we expected. Let's add a new ADT for the types we want to work with:

type ty =
  | TNat
  | TBool

Our goal is then to design a function that computes the type for a given expression. We do so in the same way we ended up designing the evaluator. Remember from last week that the evaluator had the following shape:

module StringMap = Map.Make(String)
let rec eval (e : expr) (m : value StringMap.t) : value  = 
  match e with 
  | ...

Our evaluator did not just take in the expression, but also a mapping m for the environment: a way to assign variables to values. Thus, to evaluate

let x = 42 in let y = x + 1 in y
We first evaluated 42, then then evaluated let y = x + 1 in y under the environment {x |-> 42}. This then caused us to evaluate x + 1 under that environment (giving us 43). Finally, we evaluated y under the new environment {x |-> 42, y |-> 43}.

Type checking in the the same way. The only big difference (for now) is that we don't keep precise track of all the values, but just the types: 

let rec typeof (e : expr) (ty_env : ty StringMap.t) : ty option = 
  match e with
  | ...
Additionally, while evaluation threw a runtime error when trying to evaluate false + false, we don't want type checking to behave the same way. Instead, we want it to always succeed, but return None in the cases where type checking failed.

Let's now fill in some cases of this function. Values are straightforward: 

match e with 
| Value (Nat _) -> Some TNat
| Value (Bool _) -> Some TBool
| ...

Next, let's do variables and let bindings. These are handled almost exactly like we did for evaluation: the only difference is returning None instead of failing.

  | Var x -> StrMap.find_opt x ty_env
  | Let(x, e1, e2) ->
    (match typeof ctx e1 with
     | None -> None
     | Some t -> 
        let ctx = StrMap.add x ty ctx in
        typeof ctx e2)

We will finish this function in the next lecture.