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.
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.
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.
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:
e is a number n or lambda \lambda x . e. In both of these cases, e is a value, so it steps to itself and our theorem holds.
e is an application (e_1 ~ e_2). Our inductive hypothesis tells us that e_2 runs to some value v_2. By the assumption that e is well-typed and our inductive hypothesis, it follows that e_1 \rightarrow^* \lambda x . e_b. So, we can apply (E-Beta) to show that e \rightarrow^* e_b[x \mapsto v_2]. However, now we are stuck; our inductive hypothesis does not tell us anything about how e_b[x \mapsto v_2] behaves and whether or not there is something that it can step to, because it is not necessarily the case that e_b[x \mapsto v_2] is a subterm of e.
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.