Lecture 11: Type Checking

1 Introduction

As our language gets richer, we’re finding more reasons to reject programs that we do not want to compile: because names are not in scope correctly, or definitions hide existing definitions, or functions aren’t used with the proper number of arguments. To this list we can add another problem: using functions or operators with the wrong types of arguments. We’ve already seen the impact this has on our compiled output: we have to include tag-checking code before every operation, to ensure that the operands are plausible inputs. But such dynamic checking has drawbacks: while it’s convenient to start writing programs in a dynamically typed language, we pay the cost of repeated runtime checking, a lack of guarantees that hidden bugs aren’t still lingering in our code, and no clear attribution of how the implausible data managed to get to the operation that (mis)used it. Statically typed languages avoid these downsides, and so it makes sense for us to try to develop a type checker that can confirm, at compile time, whether or not a given input program is internally consistent with its usage of data.

As we’ll soon see, the challenge in designing a type system lies in balancing expressiveness, ergonomics, and decidability. There will always be programs that are correct, in the sense that they will never crash at runtime due to misuse of data, but that we cannot convince the compiler of their correctness. They may rely on intricate invariants, or subtle data and control-flow dependencies, that the type system isn’t rich enough to recognize and exploit. We could attempt to enhance the type system to do so, but then we force the programmer to supply enough evidence at all times to satisfy that new type system, and such evidence (in the form of type annotations) might be overwhelmingly tedious. Worse yet, some type safety properties just might not even be decidable1By Rice’s theorem, we’re inevitably out of luck if we wanted to get a correct and precise delineation between “correct” and “incorrect” programs., and it would be a shame to enhance our compiler’s type system to the point that it outright gets stuck in an infinite loop, trying to compile our program! It is not our goal right now to dive into advanced type system design, or to explore the various trade-offs in type system ergonomics. The type system we will develop here is one of the simpler ones, and understanding how it works will lay the groundwork for understanding more advanced systems.

2 Type systems as formal judgements

The informal goal of a type system is to confirm that a program obeys a certain self-consistency property. We can achieve this in many ways, but as with all the other phases of our compiler, the most convenient way to do so is by examining the syntax tree of our program, and locally confirming that each node of the tree obeys the property we want. Note that we have subtly moved the goalposts here: we are measuring a particular syntactic property of our program that is sufficient but not necessary to confirm that our program is type-sound. Our syntactic property will take the form of a judgement, i.e., “we hereby judge this expression to have our desired property, assuming the following preconditions.” We’ll develop the notation for this in stages.

2.1 Values

Let’s start with the simplest cases in our language. It’s safe to agree that all numbers in our language are, in fact, integers; likewise, true and false are booleans. We will simply annotate this as

\begin{equation*}\dfrac{}{n : \mathsf{Int}} \qquad\qquad \dfrac{}{b : \mathsf{Bool}}\end{equation*}

2.2 Primitives and derivation trees

Next, let’s look at one of the easier operations in our language, addition. Addition produces a number provided both of its arguments are numbers:

\begin{equation*}\dfrac{e_1 : \mathsf{Int} \quad e_2 : \mathsf{Int}}{e_1 + e_2 : \mathsf{Int}}\end{equation*}

Read this aloud as “If \(e_1\) has type \(\mathsf{Int}\) and \(e_2\) has type \(\mathsf{Int}\), then \(e_1 + e_2\) has type \(\mathsf{Int}\)”. In other words, the bar acts as an if-then, while the colon acts as the phrase “has type”. Looking again at the two rules for values above, we see they’re degenerate cases of this: there are simply no preconditions needed for determining that numbers or booleans have the appropriate types. We say that such typing rules are axioms.

How might we deduce that the expression \((3 + 4) + 5\) has type \(\mathsf{Int}\)? Since the premises of our rule for plus-expressions have the same form as our judgement does, we can simply join multiple uses of the rules we have into a derivation tree, where the root of the tree is the judgement we want to prove, and the leaves of the tree are all axioms.

\begin{equation*}\dfrac{\dfrac{\dfrac{}{3 : \mathsf{Int}} \quad \dfrac{}{4 : \mathsf{Int}}}{3 + 4 : \mathsf{Int}} \quad \dfrac{}{5 : \mathsf{Int}}}{(3 + 4) + 5 : \mathsf{Int}}\end{equation*}

Analogous rule hold for most of our other primitive operations. For example,

\begin{equation*}\dfrac{e_1 : \mathsf{Int} \quad e_2 : \mathsf{Int}}{e_1 < e_2 : \mathsf{Bool}}\end{equation*}

2.3 Type variables

However, some of our primitives are more complicated. For example, isbool accepts anything as its argument, and returns a boolean. We could write something like

\begin{equation*}\dfrac{e : \mathsf{Any}}{\mathtt{isbool}(e) : \mathsf{Bool}}\end{equation*}

and this would work, at least so far. But if we attempted the same thing with print, which accepts anything and returns it, we’d get

\begin{equation*}\dfrac{e : \mathsf{Any}}{\mathtt{print}(e) : \mathsf{Any}}\end{equation*}

...and now we have a problem. The result type of \(\mathsf{Any}\) isn’t an acceptable premise for most of our typing rules: it’s lost too much information about its argument. Instead, we need a way to indicate that these operators are “generic”, or parametric over the type of their argument. We typically use the Greek letter \(\tau\) to indicate a type, and so we would write

\begin{equation*}\dfrac{e : \mathsf{\tau}}{\mathtt{isbool}(e) : \mathsf{Bool}} \qquad\qquad \dfrac{e : \mathsf{\tau}}{\mathtt{print}(e) : \mathsf{\tau}}\end{equation*}

Every time the same type-variable appears in a rule, it must mean the same type. So the latter rule says, “If \(e\) has type \(\tau\), then \(\mathtt{print}(e)\) does too.”

Likewise, == compares any two values and returns a boolean. We have a choice to make: we could permit the two values to be of distinct types, or we could require that they be of the same type. Since the former situation is guaranteed to produce false as an answer, most type systems require that equality take two arguments of the same type:

\begin{equation*}\dfrac{e_1 : \mathsf{\tau} \quad e_2 : \mathsf{\tau}}{e_1 == e_2 : \mathsf{Bool}}\end{equation*}

2.4 Variables

How might we handle variables and let-bindings? We don’t seem to have enough information in our typing judgement to keep track of what variables are in scope, and of what types. So we need to generalize our judgement form to

\begin{equation*}\Gamma \vdash e : \mathsf{\tau}\end{equation*}

which is read, “In context \(\Gamma\), expression \(e\) has type \(\tau\).” A context is simply a list of bindings of variable names to types. We’ll use it as follows:

\begin{equation*}\dfrac{\Gamma(x) = \tau}{\Gamma \vdash x : \mathsf{\tau}} \qquad\qquad \dfrac{\Gamma \vdash e : \mathsf{\tau_1} \quad \Gamma, x : \tau_1 \vdash b : \mathsf{\tau_2}}{\Gamma \vdash (\mathtt{let\:} x : \tau_1 = e \mathtt{\:in\:} b)_{\tau_2} : \mathsf{\tau_2}}\end{equation*}

The first rule confirms that a variable has a given type if the context maps that variable to that type. The second rule manipulates the context: first, it typechecks the let-binding itself in the original context \(\Gamma\). Assuming that succeeds, it typechecks the body at the desired type (\(\tau_2\)) in a context that has been enhanced with the binding for \(x\).

(Note that if we had not provided \(\tau_1\) or \(\tau_2\) as part of the syntax of our program, then we would have had to guess what they were, in order to derive the premises of this rule. This is why languages without type inference require the programmer to annotate the types of their variables, or return types of their functions, etc.)

All of our other rules do not manipulate bindings, so they just pass the context through unchanged. For example,

\begin{equation*}\dfrac{\Gamma \vdash e_1 : \mathsf{\tau} \quad \Gamma \vdash e_2 : \mathsf{\tau}}{\Gamma \vdash e_1 == e_2 : \mathsf{Bool}}\end{equation*}

2.5 Functions and function calls

Suppose we have a function definition and use:

def add(x : Int, y : Int) -> Int:
  x + y

add(3, 5) : Int

In order to check this program, we need to know the type for add. It’s not enough to merely record that it is a function; we need to know that it takes two arguments, both of which must be Ints, and that it returns an Int. We will write this as a type \((\mathsf{Int}, \mathsf{Int} \rightarrow \mathsf{Int})\). Conversely, when we apply a function, we need to be sure that the application supplies the correct number of arguments, of the correct types, and then we can derive the final type as needed. Formally, the application typing rule looks as follows:

\begin{equation*}\dfrac{\Gamma \vdash f : \mathsf{(\tau_1, \ldots, \tau_n \rightarrow \tau_r)} \quad \Gamma \vdash e_i : \mathsf{\tau_i}}{\Gamma \vdash f(e_1, \ldots, e_n) : \mathsf{\tau_r}}\end{equation*}

To typecheck a function body, we simply bind all the arguments at their annotated types and add them to \(\Gamma\), then typecheck that the body has the requested result type:

\begin{equation*}\dfrac{\Gamma, x_1 : \tau_1, \cdots, x_n : \tau_n \vdash b : \mathsf{\tau_r}}{\Gamma \vdash \mathtt{def\:}f(x_1, \ldots, x_n)\:\:\mathtt{{-}{>}}\:\tau_r\mathtt{\::\:}body : \mathsf{(\tau_1, \cdots, \tau_n \rightarrow \tau_r)}}\end{equation*}

2.6 Typechecking entire programs

When considering an entire program, there are no variables in scope. So our program must type-check in the empty context.

Once we’ve typechecked a function definition, though, we must add it to our resulting context for the rest of the program.

3 Implementing the type system

We need a type definition to describe the syntax of our types:

type 'a typ =
  | TyVar of string * 'a (* type variables like tau_1 *)
  | TyCon of string * 'a (* type constants like Int or Bool *)
  | TyArr of 'a typ list * 'a typ (* Arrow types, containing argument types and return type *)
  | TyApp of 'a typ * 'a typ list (* Type applications, like `int list`, if we add them *)

We’ll also consider a constructor TyBlank of 'a, to indicate that the programmer neglected to provide a type annotation.

Our type checker will effectively be a function

let rec type_check_prog env prog : bool =
  match prog with
  | Program(defns, body, typ, _) ->
    let env' = ... do stuff with the definitions ... in
    type_check_exp env' body typ
and type_check_exp env exp typ : bool =
  ...

that takes an initial environment (wherein we include any primitive operator types), the expression to check, and the desired type, and returns whether the expression has that type or not. We can elaborate this type by returning an type error message if the program fails to typecheck.

1By Rice’s theorem, we’re inevitably out of luck if we wanted to get a correct and precise delineation between “correct” and “incorrect” programs.