On this page:
9.1 Type Soundness
9.1.1 Proving Type Soundness Syntactically
9.1.2 Proof of Progress
9.2 Towards Normalization of STLC
9.2.1 A Failed Argument
8.15

9 Types III: Type Soundness🔗

In this lecture we will more deeply explore the consequences and properties of types.

9.1 Type Soundness🔗

One of our key properties of type systems is that they are sound, i.e., a sound type checker will reject programs that cause runtime errors in our interpreters. This property is best summarized by the famous quote from Robin Milner that "well-typed programs don’t go wrong". We will be using the syntax of the STLC that we gave in figure 10 and type system that we defined in figure 13 We will use the semantics that we introduced in figure 7; these small-step semantics were for the call-by-value lambda calculus, and we will assume that these semantics work the same way for STLC (ignoring the typing annotation for lambda terms, because it is semantically irrelevant).

How can we establish that a type checker is sound? Well, one way is to very thoroughly test our type checker implementation with lots of example programs. This can work, especially for fairly small programming languages, but as our languages get increasingly complex it starts to become very challenging to design sufficiently comprehensive test suites to cover all possible programs.

An alternative to exhaustive testing of our type checkers is to formally prove that our type checker eliminates all bad programs. This technique of proving type checkers formally sound is a pillar of type system design.

What does it mean to "formally prove a type system sound"? Well, suppose we have some well-typed simply-typed lambda calculus program e. e might take many steps before it steps to a value, e -> e -> e -> ... -> v. Recall that the way that we encode errors in our formal semantics is by getting "stuck", meaning that there is a term e that is not a value but has no applicable small-step rule. This leads to our notion of formal type soundness:

Take a moment to reflect on our notation and formal language we’ve been developing in the course so far. The statement of this theorem is very mathematically precise and crystalizes the intent of the maxim "well-typed programs don’t go wrong". The main payoff in developing formalism is being able to turn such intuitive statements into precise facts that can be checked.

Definition (Type Soundness of STLC): For any simply-typed lambda calculus program \vdash e : \tau that is well-typed in the empty context, if e \rightarrow^* e{}’ and e{}’ cannot step anymore, then e{}’ is a value and \vdash e{}’ : \tau.

Read this definition carefully, and note how it implies that it is impossible for e to get stuck along some chain of small step evaluations while satisfying this definition. This is a very powerful and desirable property for a type system to have!

9.1.1 Proving Type Soundness Syntactically🔗

This technique for proving type soundness was introduced in:

Wright, Andrew K., and Matthias Felleisen. "A syntactic approach to type soundness." Information and computation 115.1 (1994): 38-94.

If you want more details on this proof technique, see Chapter 9 of Typse and Programming Languages.

Establishing the type soundness of type systems is one of the core themes of programming languages research and development, and has animated much of the formal development of languages. One of the principle techniques we have for establishing type soundness relies on establishing the following 2 lemmas that together imply type soundness:

Lemma (Single-step progress of terms): For any STLC program e that is well-typed in the empty environment, either (1) e is a value, or (2) there exists some e{}’ such that e \rightarrow e{}’.

Lemma (Stepping preserves types): If \Gamma \vdash e : \tau and e \rightarrow e{}’, then \Gamma \vdash e{}’ : \tau.

Together, these two lemmas go by the shortened names "progress" and "preservation". Let’s examine the consequences of these two lemmas. The progress lemma tells us that our small-step program step never has runtime errors for well-typed programs. But, we aren’t done: a small-step interpreter works by repeatedly calling step until a fixed point is reached. To ensure that this interpreter is well-behaved, we need to ensure that stepping a term doesn’t change its type: this is ensured by the preservation lemma. So, together, these two lemmas ensure that our small-step interpreter never encounters runtime errors.

9.1.2 Proof of Progress🔗

Let’s see an example of why one of these two lemmas is true: we will prove the progress lemma correct. Our argument will be by induction on the typing derivation tree of \vdash e : \tau.

First, the base cases. Since we’re doing an inductive argument on the typing derivation, each case of our argument will correspond with a particular application of a typing rule:
  • The (T-Num) casee Suppose \dfrac{~}{\vdash e : \texttt{Num}}~\text{(T-Num)}

    In this case, we know that e is value and by the (E-Num) rule must step to itself.

  • The (T-Lam) case. Suppose \dfrac{\Gamma, x : \tau_1 \vdash e : \tau_2}{\vdash \lambda x : \tau_1 . e : \tau_1 \rightarrow \tau_2}~\text{(T-Lam)}.

    Once again this case is straightforward, since lambdas are values.

  • The (T-Var) case. The assumption of the progress lemma says that e is well-typed in the empty environment, so we cannot encounter the (T-Var) case, since this would not be well-typed in the empty environment.

  • The (T-App) case. Suppose \dfrac{ \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \vdash e_2 : \tau_1} {\vdash e_1 ~ e_2 : \tau_2}~\text{(T-App)}.

    Then, by our inductive hypothesis, we are in one of three cases:
    • Both e_1 and e_2 are values. By the well-typedness of of the application, we know that e_1 must be a lambda abstraction (this fact is often called the canonical forms property) and e_2 must be a valid argument, so we can apply the the (E-Beta) rule to take a step.

    • e_1 is a value but e_2 isn’t. Then, (E-App2) applies to take a step.

    • e_1 can take a step. Then, (E-App1) applies to take a step.

Type soundness isn’t everything. There are many widely-used type systems in the wild today that are not type sound, including TypeScript and Java. Nonetheless, type soundness has proven to be a useful "north star" for type systems and has been influential in designing practical type systems.

9.2 Towards Normalization of STLC🔗

Last lecture we saw that we could not find a type for the self-application function \omega = \lambda x . x ~ x. This was interesting, but it left open the question: is there some term that may run forever in the lambda calculus? Here we will explore this question in a bit more detail, and see a formal argument for why all simply-typed lambda calculus programs terminate.

9.2.1 A Failed Argument🔗

This section is based off of these lectures from Amal Ahmed and Chapter 12 of Types and Programming Languages.

Our goal is to prove the following theorem:

Theorem (Normalization): For any well-typed STLC program e, there exists some value v such that e runs to v, i.e. e \rightarrow^* v.

A way you might try to prove this is by performing induction on the abstract syntax, just like how we proved termination of IfLang. This argument breaks down into the following cases:

We will return to the challenge of proving normalization of STLC later if there is time (or, I will add some notes on it if there is no time to go over it in class). Nonetheless, this incomplete proof is a critical step on the path to understanding normalization, and is also an interesting example of a proof by induction failing because the induction hypothesis is not strong enough to conclude that the theorem holds.