Type systems

Recall from last lecture that we had a big issue with our lambda calculus. We were able to construct programs with undefined behavior, i.e. ones that would evaluate to a stuck state, by having free variables in our expressions, like

Moreover, we had no way to easily enforce higher-level constraints about our functions. For example, let’s say we had a function that would apply an argument twice to a function.

We could accidentally give this a function that only takes one argument¹, e.g.

Ideally, we could somehow restrict the allowable values for $f$ to the set of functions with two arguments (e.g. $f = \fun{x}{\fun{y}{\app{x}{y}}}$).

Invariants

The desired properties above are all examples of invariants, or program properties that should always hold true. Invariants are things like:

• In the function $\fun{n}{1/n}$, $n$ should be a number and $n \neq 0$.
• In my ATM program, customers should not withdraw more money than they have in their account.
• In my TCP implementation, neither party should exchange data until the initial handshake is complete.
• In the driver for my mouse, the output coordinates for the mouse should always be within the bounds of my screen.

There are three main considerations in the design of invariants:

1. Structure. What is the “language” of invariants? How can we write down a particular invariant?
2. Inference. Which invariants can be inferred from the program, and which need to be provided by the programmer?
3. Time of check. When, in the course of a program’s execution, is an invariant checked? Before the program is run?

For example, consider the humble assert statement. This is usually a built-in function that takes as input a boolean expression from the host language, and raises an error if the expression evaluates to false. In Python:

def div(m, n):
    assert(type(m) == int and type(n) == int)
    assert(n != 0)
    return m / n

For these kinds of asserts, the language of invariants is the same as the host language, i.e. a Python expression. This is quite powerful! You can do arbitrary computations while checking your invariants. These invariants are never inferred—you have to write the assert statements yourself². And lastly, assert statements are checked at runtime, when the interpreter reaches the assert. Nothing guarantees that an assert is checked before code relying on its invariant is executed (e.g. accidentally dividing and then asserting in the case above).

By contrast, now consider the traditional notion of a “type system” as you know it from today’s popular programming languages. For most type systems, the language of invariants is quite restricted—types specify that a variable is a “kind” of thing, e.g. n is an int, but cannot specify further that n != 0. Most stone-age programming languages require the programmer to explicitly provide type annotations (e.g. int n = 0), but modern languages increasingly use type inference to deduce types automatically (e.g. let n = 0). Lastly, types can be checked either ahead of time (“statically”, e.g. C, Java) or during program execution (“dynamically”, e.g. Python, Javascript)³.

Key idea: type systems and runtime assertions derive from the same conceptual framework of enforcing invariants, just with different decisions on when and how to do the checks.

In this course, our focus is going to be on static analysis: what invariants can we describe, infer, and enforce before ever executing the program? And by enforcement, I mean iron law. We don’t want our type systems to waffle around with “well, you know, I bet this n is going to be an integer, but I’m only like, 75% sure.” We expect Robocop type systems that tell us: I HAVE PROVED TO 100% MATHEMATICAL CERTAINTY THAT IN THE INFINITE METAVERSE OF BOUNDLESS POSSIBILITIES, THIS “n” IS ALWAYS AN INTEGER.

This is the core impetus behind most modern research in PL theory. Advances in refinement types, dependent types, generalized algebraic data types, module systems, effect systems, traits, concurrency models, and theorem provers have pushed the boundaries of static program analysis. Today, we can prove more complex invariants than ever before. While cutting-edge PL research is mostly beyond the scope of this course, you will be equipped with the necessary fundamentals to continue exploring this space.

Typed lambda calculus

To understand the formal concept of a type system, we’re going to extend our lambda calculus from last week (henceforth the “untyped” lambda calculus) with a notion of types (the “simply typed” lambda calculus). Here’s the essentials of the language:

First, we introduce a language of types, indicated by the variable tau ($\tau$). A type is either an number, or a function from an input type $\tau_1$ to an output type $\tau_2$. Then we extend our untyped lambda calculus with the same arithmetic language from the first lecture (numbers and binary operators)⁴. We drop the hat syntax for simplicity. Usage of the language looks similar to before:

Indeed, our operational semantics are just the lambda calculus plus arithmetic. Zero change from before.

An interpreter for free

A brief aside: the main reason we’re using OCaml in this course (as opposed to, say, Haskell or Scala) is that feels quite similar to the typed lambda calculus. In fact, if we change a few keywords, we can use OCaml to execute exactly the language described above. (See the OCaml setup guide to follow along). If we wanted to transcribe the two examples above:

$ ocaml
# (fun (x : int) -> x + 1) 2 ;;
- : int = 3
# (fun (f : int -> int) -> fun (x : int) -> f (x + 1)) (fun y -> y * 2) 5 ;;
- : int = 12

Of course, OCaml can do much more than this—it has strings, exceptions, if statements, modules, and so on. We’ll get there, all in due time. I point this out to show you that by learning the lambda calculus, you are actually learning the principles of real programming languages, not just highfalutin theory. When you go to assignment 3 and start on your first OCaml program, the language will feel more familiar than you may expect!

Type system goals

Before we dive into the type system, it’s worth asking the motivational question: what invariants of our language do we want to statically check? One way to answer this is by thinking of edge cases we want to avoid.

• Adding a number and a function: $1 + (\funt{x}{\tnum}{x})$
• Calling a function with the wrong type: $\app{(\funt{x}{\tfun{\tnum}{\tnum}}{x})}{0}$
• Incorrectly using a function argument: $\funt{x}{\tnum}{(\app{x}{0})}$

This is an important exercise, since it gives us an intuition for where errors might arise. However, even if we had a method for completely eliminating the edge cases we thought of, how can we know we caught all the cases? What if we just didn’t think of a possible error?

Remember that all of these issues fundamentally boil down to stuck states, or undefined behavior. We specified our operational semantics over “well-defined” programs, but that doesn’t prevent us from writing invalid programs. As before, the goal is to take a program and step it to a value. This leads us to a safety goal: if a program is well-defined, it should never enter a stuck state after each step. If we can formally prove that this safety goal holds for our language, then that means there are no missing edge cases!

The goal of a type system, then, is to provide a definition of “well-defined” such that we can prove whether a given program is well-defined without executing it. Formally, we need a new judgment (binary relation) “$e$ has type $\tau$”, written as $\hasType{e}{\tau}$. In the language above, it should be the case that $\hasType{(1+1)}{\tnum}$ and $\hasType{(\funt{x}{\tnum}{x+1})}{\tfun{\tnum}{\tnum}}$. To say an expression has a type is to say it is “well-defined” (or “well-typed”).

We can try and formally write type safety as the following theorem:

Type safety (strict): for all expressions $e$, if $e : \tau$, then $\exists e'$ such that $\evals{e}{e'}$ and $\val{e'}$.

This definition is a little too strict because it mixes two notions: totality and stuck-state-avoidance. This theorem is fine for total languages like arithmetic and the simply-typed lambda calculus, but we would also like to reason about type safety in languages that involve infinite loops and recursion like we’ll see tomorrow. So instead of the theorem above, we decompose the intuition of “avoiding stuck states” into the following two theorems:

1. Progress: if $\hasType{e}{\tau}$ then either $\val{e}$ or there exists $e'$ such that $\steps{e}{e'}$.
2. Preservation: if $\hasType{e}{\tau}$ and $\steps{e}{e'}$, then $\hasType{e'}{\tau}$.

Intuitively, progress says: if an expression is well-typed and is not a value, then we should be able to step the expression (it is not in a stuck state). However, this isn’t enough to prove our safety goal, since we also need preservation: if an expression is well-typed, when it steps, its type is preserved. For example, if we have an expression of number type, it shouldn’t turn into a function after being stepped. These two theorems are sufficient to prove that a well-typed expression will never enter a stuck state at any point during its execution.

Static semantics

In this conceptual framework of type systems, the first thing we need to do is define how we determine the type of an expression. In our grammar, we defined a type language, but now we need a type semantics (or “static semantics”). First, we’ll define the judgments for numbers:

As you can see, these are defined quite similarly to how we defined our operational semantics (or “dynamic semantics”). Each rule defines a different way to determine whether a particular expression has a particular type. Just like $\val{n}$, the $\text{T-Num}$ rule of $\hasType{n}{\tnum}$ is axiomatic—a numeric constant has type $\tnum$ under all conditions. $\text{T-Binop}$ says: if the two subexpressions are both numbers, then the binary operation on those subexpressions is also an number. From these two rules, we can construct a proof that $\hasType{(1 + 2 - 3)}{\tnum}$:

Ok, but what is this “$\nul \proves$” business? Or “$\Gamma$”? To typecheck expressions with variables, we need to introduce a “typing context” that maps variables to their types. Intuitively, when typechecking $\funt{x}{\tnum}{(1 + x)}$, we want to remember that a usage of $x$ can assume $\hasType{x}{\tnum}$. Formally, we write this as:

The notation $\typeJC{e}{\tau}$ means that “given the knowledge of $\ctx$, it is provable that $\hasType{e}{\tau}$.” The left hand side of the turnstile is a proof context (something we know), and the right hand side is a proof term (the thing we want to prove). $\ctx$ specifically represents our type context. It is a mapping from variables to types. We can add new mappings to our context⁵, indicated by $\ctx, \hasType{x}{\tau}$.

Let’s read through the rules again. $\text{T-Var}$ says that if our context says $\hasType{x}{\tau} \in \ctx$ then $x$ has type $\tau$. $\text{T-Lam}$ is the most complex: it says that to type-check a function, we want to type-check the body of the function $e$ assuming that $\hasType{x}{\tau_\msf{arg}}$, where $\tau_\msf{arg}$ is the type provided in the program syntax. Then, assuming our body typechecks to another type $\tau_\msf{ret}$, this becomes the return type of the function, so its entire type is $\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}$.

Note a subtlety here: $\tau_\msf{arg}$ is given to us from the program, while we have to compute $\tau_\msf{ret}$. Our typed lambda calculus mixes types that are explicitly annotated and implicitly inferred.

Lastly, the $\text{T-App}$ rule says: when calling a function, the function expression $e_\msf{lam}$ should be a function $\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}$, and the argument expression $e_\msf{arg}$ should be of the appropriate argument type $\tau_\msf{arg}$. Then, the result of applying the function is the result of the function, type $\tau_\msf{ret}$.

As an example of these rules, here is the proof that $\hasType{(\app{(\funt{x}{\tnum}{x+1})}{2})}{\tnum}$.

Proving type safety

At this point, you should understand the mechanics of our type system: how we define our typing rules, and how they can be used to construct proofs about the types of expressions. But it’s not sufficient just to have a type system, we need a good type system! Remember, we want to demonstrate that if a program is well-typed, then it will never enter a stuck state. To do that, we have to prove the progress and preservation theorems.

Rule induction

Last time, we talked about structural induction, and how an induction principle could be derived from the structure of a grammar. For example, if numbers are defined as:

Then our induction principle becomes:

Another way to see the mapping from the grammar to the induction principle is to rewrite the grammar in terms of inference rules.

The BNF notation is essentially an alternative way of saying the same thing. We define a judgment $\mathsf{Number}$ that says whether something has the number syntax. From this notation, we want to derive an induction principle for universal properties: $\forall n . \ n~\mathsf{Number}\implies P(n)$. To make such a principle, we can ask: what are all the ways that $n~\mathsf{Number}$ could have been derived? Then for each possible derivation, we have an induction hypothesis on the assumptions and a desired proof on the conclusion.

Here, because $n~\mathsf{Number}$ can be derived two ways, each contributes a case in the induction, either $P(Z)$ or $P(n) \implies P(S(n))$. This is the same as before, but rewritten so as to see how an inductive principle can be derived from inference rules as opposed to a grammar.

More generally, this idea is called rule induction, making inductive principles from inference rules. And we can apply the same idea to our typing judgment. If our theorem says “if $e : \tau$ then $P(e)$”, we can prove $P(e)$ by showing it inductively true for all derivations of $e : \tau$. Specifically:

Induction principle for static semantics: for all $\Gamma, e, \tau$ such that $\Gamma \vdash e : \tau$, then $P(e)$ if:

• T-Num: Assume $e = n, \tau = \tnum$. Show $P(n)$.
• T-Binop: Assume $e = e_L \oplus e_R$ and $e_L : \tnum, e_R : \tnum$. Show $P(e_L) \wedge P(e_R) \implies P(e)$.
• T-Var: Assume $e = x$ and $x : \tau \in \Gamma$. Show $P(x)$.
• T-Lam: Assume $e = \funt{x}{\tau_\msf{arg}}{e'}$ and $\tau = \tfun{\tau_\msf{arg}}{\tau_\msf{ret}}$ and $\Gamma, x : \tau_\msf{arg} \vdash e' : \tau_\msf{ret}$. Then show that $P(e') \implies P(e)$.
• T-App: Assume $e = \app{e_\msf{lam}}{e_\msf{arg}}$ and $\typeJ{\ctx}{e_\msf{lam}}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$ and $\typeJ{\ctx}{e_\msf{arg}}{\tau_\msf{arg}}$. Show $P(e_\msf{lam}) \wedge P(e_\msf{arg}) \implies P(e)$.

Preservation proof

First we will prove preservation by rule induction on the static semantics:

Preservation: if $\typeJ{\nul}{e}{\tau}$ and $\steps{e}{e'}$ then $\typeJ{\nul}{e'}{\tau}$.

Note that the progress and preservation theorems are defined with respect to “closed terms”, i.e. expressions which don’t need a type context at the top level to prove their type. Or put another way, expressions with no free variables. We show that here by saying that the fact $e : \tau$ must be proved with no context $\ctx$.

Proof. By rule induction on the static semantics.

1. T-Var: if $x : \tau$ and $\steps{x}{e'}$ then $\hasType{e'}{\tau}$.

   This is vacuously true, since $\typeJC{x}{\tau} \iff \ctx \neq \nul$, so the typing context cannot be empty. Our theorem says the typing context must be empty, so our condition is never met.

2. T-Num: if $\hasType{n}{\tnum}$ and $\steps{n}{e'}$ then $\hasType{e'}{\tnum}$.

   This is vacuously true, since there is no rule to step a number $n$.

3. T-Binop: if $\hasType{e_L \oplus e_R}{\tnum}$ and $\steps{e_L \oplus e_R}{e'}$ then $\hasType{e'}{\tnum}$.

   First, by the premises of the $\text{T-Binop}$ rule, we know $\hasType{e_L}{\tnum}$ and $\hasType{e_R}{\tnum}$.

   Second, by the inductive hypothesis (IH), we get to assume preservation holds true for $e_L$ and $e_R$. For example, if $\steps{e_L}{e_L'}$ then we know $\hasType{e_L'}{\tnum}$ (and likewise for $e_R$).

   Third, we case on the three ways in which a binary operation can step:

   1. D-Binop-1: assume $\steps{e_L}{e_L'}$, so $\steps{e_L \oplus e_R}{e_L' \oplus e_R}$. By the IH, $\hasType{e_L'}{\tnum}$, so by $\text{T-Binop}$ we have that $\hasType{e_L' \oplus e_R}{\tnum}$.

   2. D-Binop-2: assume $\val{e_L}$ and $\steps{e_R}{e_R'}$, so $\steps{e_L \oplus e_R}{e_L \oplus e_R'}$. By the IH, $\hasType{e_R'}{\tnum}$, so by $\text{T-Binop}$ we have that $\hasType{e_L \oplus e_R'}{\tnum}$.

   3. D-Binop-3: assume $e_L = n_L$ and $e_R = n_R$ and $n' = {n_L}\oplus{n_R}$, so $\steps{n_L \oplus n_R}{n'}$. By $\text{T-Num}$ we have that $\hasType{n'}{\tnum}$.

   Hence, in every case, we have shown that $\hasType{e'}{\tnum}$ for all possible $e'$, and the preservation theorem holds for $\text{T-Binop}$.

4. T-Lam: if $\hasType{(\funt{x}{\tau_\msf{arg}}{e})}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$ and $\steps{\funt{x}{\tau_\msf{arg}}{e}}{e'}$ then $\hasType{e'}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$.

   This is vacuously true, since there is no rule to step a function value.

5. T-App: if $\hasType{\app{e_\msf{lam}}{e_\msf{arg}}}{\tau}$ and $\steps{\app{e_\msf{lam}}{e_\msf{arg}}}{e'}$ then $\hasType{e'}{\tau}$.

   First, by the premises of $\text{T-App}$, we know $\hasType{e_\msf{lam}}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$ and $\hasType{e_\msf{arg}}{\tau_\msf{arg}}$.

   Second, by the IH, we know that preservation holds for $e_\msf{lam}$ and $e_\msf{arg}$.

   Third, we case on the two ways an application can step:

   1. D-App-Step: assume $\steps{e_\msf{lam}}{e_\msf{lam}'}$, so $\steps{\app{e_\msf{lam}}{e_\msf{arg}}}{\app{e_\msf{lam}'}{e_\msf{arg}}}$. By the IH, $\hasType{e_\msf{lam}'}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$, so by $\text{T-App}$, we know $\hasType{\app{e_\msf{lam}'}{e_\msf{arg}}}{\tau_\msf{ret}}$.

   2. D-App-Sub: assume $e_\msf{lam} = \funt{x}{\tau}{e_\msf{body}}$, so $\steps{\app{e_\msf{lam}}{e_\msf{arg}}}{\subst{x}{e_\msf{arg}}{e_\msf{body}}}$.

      By the inversion of ($\text{T-Lam}$), we know $\tau = \tau_\msf{arg}$ and $\typeJ{\hasType{x}{\tau_\msf{arg}}}{e_\msf{body}}{\tau_\msf{ret}}$.

      By the substitution typing lemma⁶, $\typeJ{\hasType{x}{\tau_\msf{arg}}}{e_\msf{body}}{\tau_\msf{ret}} \implies \hasType{\subst{x}{e_\msf{arg}}{e_\msf{body}}}{\tau_\msf{ret}}$.

   Hence, preservation holds in either case.

Since preservation holds for all typing rules, then it holds for the entire language. $\blacksquare$

Progress proof

Finally, we will prove progress:

Progress: if $\typeJ{\nul}{e}{\tau}$ then either $\val{e}$ or there exists $e'$ such that $\steps{e}{e'}$.

Proof. By rule induction on the static semantics.

1. T-Var: if $\hasType{x}{\tau}$ then either $\val{x}$ or there exists $e'$ such that $\steps{e}{e'}$.

   This is vacuously true, since a variable $x$ cannot have a type $\tau$ without a typing context $\ctx$.

2. T-Num: if $\hasType{n}{\tnum}$ then either $\val{n}$ or there exists $e'$ such that $\steps{n}{e'}$.

   By D-Num, $\val{n}$.

3. T-Binop: if $\hasType{e_L \oplus e_R}{\tnum}$ then either $\val{e_L \oplus e_R}$ or there exists $e'$ such that $\steps{e_L \oplus e_R}{e'}$.

   First, by the premises of the $\text{T-Binop}$ rule, we know $\hasType{e_L}{\tnum}$ and $\hasType{e_R}{\tnum}$.

   Second, by the inductive hypothesis (IH), we get to assume progress holds true for $e_L$ and $e_R$. For example, if either $\val{e_L}$ or $\steps{e_L}{e_L'}$.

   Third, we case on the different possible states of $e_L$ and $e_R$ derived from the IH:

   1. $\steps{e_L}{e_L}'$: then by D-Binop-L, $\steps{e_L \oplus e_R}{e_L' \oplus e_R}$.

   2. $\val{e_L} \wedge \steps{e_R}{e_R}'$: then by D-Binop-R, $\steps{e_L \oplus e_R}{e_L \oplus e_R'}$.

   3. $\val{e_L} \wedge \val{e_R}$: because $\hasType{e_L}{\tnum}$ and $\hasType{e_R}{\tnum}$, then by inversion on D-Num we know $e_L = n_L$ and $e_R = n_R$. Therefore by D-Binop-Op, $\steps{n_L \oplus n_R}{n'}$ for $n' = n_L \oplus n_R$.

   In each case, the expression steps, so progress holds.

4. T-Lam: if $\hasType{(\funt{x}{\tau_\msf{arg}}{e})}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$ then either $\val{(\funt{x}{\tau_\msf{arg}}{e})}$ or there exists $e'$ such that $\steps{(\funt{x}{\tau_\msf{arg}}{e})}{e'}$.

   By D-Lam, $\val{(\funt{x}{\tau_\msf{arg}}{e})}$.

5. T-App: if $\hasType{\app{e_\msf{lam}}{e_\msf{arg}}}{\tau}$ then either $\val{\app{e_\msf{lam}}{e_\msf{arg}}}$ or there exists $e'$ such that $\steps{\app{e_\msf{lam}}{e_\msf{arg}}}{e'}$.

   First, by the premises of $\text{T-App}$, we know $\hasType{e_\msf{lam}}{\tfun{\tau_\msf{arg}}{\tau_\msf{ret}}}$ and $\hasType{e_\msf{arg}}{\tau_\msf{arg}}$.

   Second, by the IH, we know that progress holds for $e_\msf{lam}$ and $e_\msf{arg}$.

   Third, we case on the different possible states of $e_\msf{lam}$ derived from the IH:

   1. $\steps{e_\msf{lam}}{e_\msf{lam}'}$: then by D-App-Step, $\steps{\app{e_\msf{lam}}{e_\msf{arg}}}{\app{e_\msf{lam}'}{e_\msf{arg}}}$

   2. $\val{e_\msf{lam}}$: then by inversion on D-Lam, $e_\msf{lam} = \funt{x}{\tau}{e_\msf{body}}$. By D-App-Sub, $\steps{\app{e_\msf{lam}}{e_\msf{arg}}}{\subst{x}{e_\msf{arg}}{e_\msf{body}}}$.

   In each case, the expression steps, so progress holds.

Since progress holds for all typing rules, then it holds for the entire language. $\blacksquare$