9 Types III: Type Soundness
In this lecture we will (1) more deeply explore the consequences and properties of types and (2) grow our type system.
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".
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, consider IfLang, and recall its type system we designed in figure 13 and its operational semantics in figure 10.
Suppose e is a well-typed simply-typed IfLang program. 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.
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 Types 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 (Progress): For any well-typed IfLang program e, either (1) e can take a single step, or (2) e is a value.
Lemma (Preservation): If e : \tau and e \rightarrow e{}’, then e{}’ : \tau.
Together, these two lemmas imply type soundness and hence establish that our small-step interpreter never encounters runtime errors. The proof of type soundness using these lemmas is as follows:
Suppose e is a well-typed IfLang program and e\rightarrow^*e’.
If we can show that e’ is well-typed, then by the progress lemma, it is not stuck.
Base case (E-Refl): The E-Refl rule is a base case since it has no premises, and it says e’ = e. By assumption, we can immediately conclude e’ is well-typed.
Inductive case (E-Trans). By induction we (1) e \rightarrow e{}’{}’{}’ \rightarrow^* e{}’{}’, and (2) our inductive hypothesis, which says that if e{}’{}’{}’ has type \tau then so does e{}’{}’. By preservation, we have that e{}’{}’ is well-typed, and so the inductive hypothesis concludes.
9.1.2 Proof of Progress Lemma
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. There are also richer notions of type safety than the syntactic notion of type safety that we discuss here: see this blog post.
(T-Num). In this case, e must be a number, which is a value.
(T-Bool). In this case, e must be a Boolean, which is a value.
- (T-Ite). In this case, e = \texttt{(if g thn els)}, and our inductive hypothesis says that g, thn, and els are not stuck. Now, we do case analysis on the inductive hypothesis for g:
Case 1: g is a value. By canonical forms, it is either true or false. If it is true, we step using the (E-IteT) rule; if it is false, we step using the (E-IteF) rule.
Case 2: g can step. In this case, we step using the (E-IteStep) rule.
The proof for (T-Add) is very similar to the case for (T-Ite) and so we elide it.
9.2 MutLang: A Language with Mutable State
Let’s put everything together, all of our formal tools and techniques, to quickly prototype a new language and explore the consequences of its type system.
Abstract syntax:
> (define-type RefLang (letE [id : Symbol] [assgn : RefLang] [body : RefLang]) (unboxE [e : RefLang]) (boxE [e : RefLang]) (setboxE [e1 : RefLang]) (varE [id : Symbol]) (numE [n : Number]))
Surface syntax:
‹expr›
::=
( let ‹ident› ‹expr› ‹expr› )
|
( box ‹ident› )
|
( unbox ‹expr› )
|
( set-box ‹expr› ‹expr› )
|
‹num›
|
‹ident›
Small-step semantics:
\dfrac{~}{\langle \rho, n \rangle \rightarrow \langle \rho, n \rangle}~\text{(E-Num)}\dfrac{\langle e_1, \rho \rangle \rightarrow \langle e_1{}’, \rho{}’ \rangle} {\langle \rho, (\texttt{let}~x~e_1~e_2) \rangle \rightarrow \langle \rho{}’, (\texttt{let}~x~e_1{}’~e_2) \rangle}~\text{(E-Let1)}\dfrac{~} {\langle \rho, (\texttt{let}~x~v_1~e_2) \rangle \rightarrow \langle \rho, e_2[x \mapsto v_1] \rangle}~\text{(E-Let2)}\dfrac{\langle e_1, \rho \rangle \rightarrow \langle e_1{}’, \rho{}’ \rangle} {\langle \rho, (unboxE [e : RefLang]) \rangle \rightarrow }
Figure 16: Small-step semantics for MutLang, defines a relation \langle \rho, e \rangle \rightarrow \langle \rho{}’, e{}’ \rangle.
9.2.1 Typechecking MutLang
\dfrac{~}{\Gamma \vdash n : \texttt{Num}}~\text{(T-Num)}\dfrac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}~\text{(T-Var)}\dfrac{\Gamma \vdash e_1 : \tau_1 \qquad \Gamma, x : \tau_1 \vdash e_2 : \tau_2 }{\Gamma \vdash \texttt{(let }x~e_1~e_2 \texttt{)} : \tau_2}~\text{(T-Let)}
Theorem (Type soundness for MutLang): For any well-typed MutLang e, either (1) e is a value, or e can take a step.
9.3 Consequences of Mutable State
(define my-fun (box (lambda (x) (+ x 1)))) (define loopy (lambda (x) ((unbox my-fun) x))) (set-box! my-fun loopy)