Soundness, Informally

The previous chapters built a checker and claimed that a program it accepts cannot stop on a type error. The claim is about the evaluator, and the evaluator never sees a type. In this program, make_adder takes an integer n and returns a lambda that adds n to its argument; main binds its own n to a string, makes the adder, and calls it:

fn make_adder(n: Int) -> fn(Int) -> Int = |x| x + n;

fn main() {
    let n = "five";
    let add5 = make_adder(5);
    println(add5(1));                                   // 6
}

The checker typed the body x + n once, inside make_adder, where n is the parameter and has type Int. When add5(1) runs, the evaluator’s addition arm receives two values and matches each against Value::Int, with a branch that raises a TypeError for anything else. At that moment main has a variable n holding "five".

The program raises these questions:

• What exactly is promised? The evaluator can stop in many ways, a division by zero among them. Which of them does an accepted program avoid?
• Why does a fact about the text hold for the run? The checker saw x + n once, before anything ran. The evaluator meets it with environments, closures, and a store that exist only at run time. What makes the n the body reads an integer?
• What does a mistake in the checker look like? If one rule accepts something it should not, where does the program fail, and what does the failure point at?

The guarantee was first proved for ML. The proof began by giving every meaningless operation, such as applying a number as if it were a function, a result of its own, which no type describes.

Going wrong

The first chapter of this part quoted the title of §3.7 of Robin Milner’s “A Theory of Type Polymorphism in Programming” (1978): “Well-Typed Expressions Do Not Go Wrong”. Before proving anything about his small language, Milner defined what its programs mean: “We give an ordinary denotational semantics for Exp, in which we include a value “wrong,” which corresponds to the detection of a failure at run-time. In this small language, the only failures are the occurrence of a non-Boolean value as the condition of a conditional, and the occurrence of a nonfunctional value as the operator of an application.“ Where Bridger’s rules have no derivation for if 1 { … }, Milner’s semantics gives it the meaning wrong.

Milner then defined when a value possesses a type, written $v:\mu$, and stated the reading that Pascal’s report had given for variables: “If we temporarily identify a type with the set of values which possess it”, each type is a set of values. Integers possess int; a function possesses a function type when it maps every value of the parameter type to a value of the result type. wrong possesses nothing: “In fact “wrong” has no type.“ His Theorem 1, Semantic Soundness, says that the meaning of a well-typed expression, in an environment whose values possess the types the checker assumed for them, possesses the expression’s type. The guarantee follows as a corollary, “since wrong has no type”: a meaning that has a type is not wrong.

The rest of this chapter follows the same argument for Bridger. It has two parts. The first gives types to values, which the evaluator produces, as well as to expressions, which the checker reads. The second proves that evaluation takes a well-typed expression only to a value of the same type. The guarantee then follows, because each failure is a value that has no type.

What the guarantee says

Bridger’s semantics has no wrong. Program Semantics made a stuck expression one with no derivation, and also observed that an expression that runs forever has none either, so “has a derivation” cannot separate the two. The interpreter can. Its evaluator, asked to evaluate a stuck expression, returns a RuntimeError, and those errors play the part of Milner’s wrong. Some of them are the failures types predict, and the guarantee is stated in terms of those:

Stated informally, for a Bridger program built from the forms of Parts II through VI:

Soundness. If the checker accepts a program, then running it does one of three things: it finishes, it runs forever, or it stops with an error from the right-hand column. It never stops with an error from the left-hand column.

The guarantee says nothing about which of the three happens, or about whether the value is the one the programmer wanted. Running forever is allowed, and so is 10 / (5 - 5). What it rules out is the evaluator reaching an arm with a value of a kind the arm cannot use.

Why it holds

The checker and the evaluator work on different things. The checker has an expression, a context $\Gamma$ of types, and the typing rules. The evaluator has the same expression, an environment $\rho$ of values, a store $\sigma$ of cells, and the evaluation rules. An argument for soundness has to say how the two sides correspond at every point of a run, and then show that each evaluation rule keeps the correspondence.

Values have types

Milner’s first step is to give types to values. For Bridger’s values:

$$\frac{n\in \mathbb{Z}}{⊢n:\text{Int}}(\text{V-Int})\frac{b\in \{\text{true},\text{false}\}}{⊢b:\text{Bool}}(\text{V-Bool})\frac{⊢v_1:{\tau }_1\cdots ⊢v_n:{\tau }_n}{⊢(v_1,\dots ,v_n):({\tau }_1,\dots ,{\tau }_n)}(\text{V-Tuple})$$

and in the same way strings have type String, () has type (), and a list has type $[\tau ]$ when every element has type $\tau$. A closure carries no type; it holds a lambda and the environment the lambda captured. A closure has a function type when its body, checked in a context that describes the captured environment, has the result type:

$$\frac{{\rho }^{\prime }:{\Gamma }^{\prime }{\Gamma }^{\prime },x_1:{\tau }_1,\dots ,x_n:{\tau }_n⊢e:\tau }{⊢⟨\lambda x_1\dots x_n.e,{\rho }^{\prime }⟩:\text{fn}({\tau }_1,\dots ,{\tau }_n)\to \tau }(\text{V-Clo})$$

${\rho }^{\prime }:{\Gamma }^{\prime }$ reads ${\rho }^{\prime }$ agrees with ${\Gamma }^{\prime }$: every name ${\Gamma }^{\prime }$ gives a type, ${\rho }^{\prime }$ binds to a value of that type. Formally, for each $x:\tau$ in ${\Gamma }^{\prime }$, ${\rho }^{\prime }(x)$ is defined and $⊢{\rho }^{\prime }(x):\tau$. (As in $\text{T-Lam}$, the context for the body also sets ${\tau }_{ret}$ to $\tau$.)

A location gets its type from a store typing $\Sigma$, which maps each allocated location to the type of what it holds. $\ell$ has type $\text{ref}⟨\tau ⟩$ when $\Sigma (\ell )=\tau$, and the store agrees with the store typing, $\sigma :\Sigma$, when each location’s contents have the type $\Sigma$ gives it. Since a tuple, a list, or a closure’s environment can hold a location, the judgment $⊢v:\tau$ depends on $\Sigma$ throughout; the rules above leave it out to keep the notation light. $\Sigma$ exists only in the argument. Nothing in the interpreter builds one; it records what the checker’s types say about each cell the program has made so far.

A value of type Int, by these rules, is an integer, since $\text{V-Int}$ is the only rule whose conclusion has type Int. A value of a function type is a closure (or a native function of the prelude, typed by its signature) taking that many arguments. Each type’s rules describe the one shape of value an evaluation arm expecting that type will find.

The invariant

The argument proves a claim about every expression the evaluator is ever asked to evaluate, by induction over the evaluator’s run, which is the tree of its recursive calls. Each case assumes the claim for the calls the arm makes on subexpressions, its premises, and proves it for the arm itself:

Suppose $\Gamma ⊢e:\tau$, $\rho :\Gamma$, and $\sigma :\Sigma$. If evaluating $e$ in $\rho$ and $\sigma$ ends, it ends in one of two ways:

• with an error from the right-hand column; or
• with a result and a store ${\sigma }^{\prime }$. The store agrees with some ${\Sigma }^{\prime }$ that keeps the type of every location in $\Sigma$ and may add new locations, ${\sigma }^{\prime }:{\Sigma }^{\prime }$. The result is either $\mathsf{Val}v$ with $⊢v:\tau$, or $\mathsf{Ret}v$ with $⊢v:{\tau }_{ret}(\Gamma )$.

The $\mathsf{Ret}$ case is the return outcome that Appendix D’s judgment carries. A return leaves the function early, so its value has the function’s return type, which $\text{T-Return}$ checked; the return expression itself may have any type where it stands.

Soundness follows. The checker accepted every declaration, so main’s body is well-typed in the top-level context ${\Gamma }_0$; the program’s environment ${\rho }_0$ agrees with ${\Gamma }_0$, and the store starts empty. A left-hand-column error is not among the ways the claim lets a run end.

For the top-level functions the agreement ${\rho }_0:{\Gamma }_0$ is circular, as ${\rho }_0$ itself is. To type a closure in ${\rho }_0$ by $\text{V-Clo}$, the argument needs ${\rho }_0:{\Gamma }_0$, and that in turn needs every closure in ${\rho }_0$ to be typed. $\text{T-Fn}$ checked every function body in ${\Gamma }_0$, so each closure’s body is well-typed in the context its environment is meant to agree with, and the sketch takes the agreement as given. A full proof has to define the agreement carefully so that the circle is well founded.

Cases from the evaluator

Each arm of the evaluator is one case of the induction. The arms below use, in turn, the rules for values, the closure’s environment, and the store typing.

Addition. $\text{T-Arith}$ gave $e_1+e_2$ the type Int because each operand has type Int. The evaluator’s arm evaluates $e_1$. By the claim for that call, the result is either an error from the right-hand column, which the arm passes on, or a value $v_1$ with $⊢v_1:\text{Int}$, and a value of type Int is an integer. The same holds for $v_2$. The arm’s match on Value::Int therefore succeeds for both operands, and its TypeError branch is unreachable. The sum is an integer, of type Int. (A $\mathsf{Ret}$ from an operand is passed on unchanged, and has ${\tau }_{ret}$ by the claim.) Every operator arm goes this way.

A call. $\text{T-App}$ typed $e_0(e_1,\dots ,e_n)$ with $e_0$ of type $\text{fn}({\tau }_1,\dots ,{\tau }_n)\to \tau$ and each $e_i$ of type ${\tau }_i$. By the claim, $e_0$ evaluates to a value of that function type, which is a closure of $n$ parameters, so NotAFunction and ArityMismatch are unreachable. The arguments evaluate to values $v_i$ with $⊢v_i:{\tau }_i$. By $\text{V-Clo}$ there is a ${\Gamma }^{\prime }$ with ${\rho }^{\prime }:{\Gamma }^{\prime }$, and the body $e_b$ has type $\tau$ in ${\Gamma }^{\prime }$ extended with the parameters. $\text{E-App}$ runs the body in ${\rho }^{\prime }[\vec{x}\mapsto \vec{v}]$, which agrees with that extended context, so the claim applies to the body, and its result has type $\tau$ whether it finishes normally or by return, since the body’s context set ${\tau }_{ret}$ to $\tau$.

In the opening program the closure is $⟨\lambda x.x+n,[n\mapsto 5]⟩$, and ${\Gamma }^{\prime }$ is $n:\text{Int}$, the context in which the checker typed x + n. The n the body reads comes from the captured environment, which agrees with the context the body was checked in. main’s n never enters it.

A cell. $\text{T-Ref}$ gives ref e the type $\text{ref}⟨\tau ⟩$ when $e$ has type $\tau$. $\text{E-Ref}$ allocates a fresh location $\ell$ holding $e$’s value; extend $\Sigma$ with $\ell :\tau$ and the store still agrees, and $\ell$ has type $\text{ref}⟨\tau ⟩$. $\text{T-Assign}$ requires the value written into a $\text{ref}⟨\tau ⟩$ to have type $\tau$, so an assignment leaves the store agreeing with the same $\Sigma$, and deref reads back a value of type $\tau$. A location’s type is fixed when the cell is made, and every write keeps to it.

Where the argument depends on the language

The case for a call used the closure’s own environment. Under the dynamic-scope rule $\text{E-App-Dyn}$, the body runs in the caller’s environment extended with the parameters. That environment agrees with the caller’s context, which may bind the body’s free names at types other than the ones the body was checked with, and the case fails: in the opening program, the body would read main’s n, a string, and the addition arm would raise a TypeError. Under lexical scope, the environment a body runs in always agrees with the context in which the checker typed that body.

The case for a cell used a fixed type per location. Function types and polymorphism described a checker that generalized let r = ref []; and let two uses of r instantiate its element type differently. The cell would then need two types in $\Sigma$, and no single $\Sigma$ makes the store agree.

A generic function’s body was checked with its type parameters standing as types of their own, equal only to themselves. Its closure is used at a different type at each call, and the call case needs the body to have the instantiated type, fn(Int) -> Int for id(1). It does: a body that uses its T values only in ways that work for every type stays well-typed when T is replaced by any particular type. Showing that for every rule is one of the lemmas a full proof states and this sketch does not.

Bridger’s guarantee

From Milestone M5, the checker runs before the evaluator. The evaluator itself is unchanged from M4, and the checker passes it nothing, so a program the checker accepts runs exactly as it ran on the M4 evaluator. Soundness is a promise about that run: it never reaches a left-hand-column error.

The evaluator keeps its TypeError branches, as the first chapter of this part noted. They report a stuck program in the milestones without a checker, and from M5 they report any ill-typed program that a bug in the checker lets through.

What a soundness bug looks like

Suppose the arm for if checked the else branch but never required its type to agree with the then branch. This declaration would be accepted:

fn pick(c: Bool) -> Int = if c { 1 } else { "one" };

fn main() {
    println(pick(true) + 1);
    println(pick(false) + 1);
}

A correct checker reports expected Int, found String at "one". The flawed one accepts the program, which then runs as the M4 evaluator runs it:

2
  × type error: expected Int, found String
   ╭─[pick.brg:5:13]
 4 │     println(pick(true) + 1);
 5 │     println(pick(false) + 1);
   ·             ───────┬───────
   ·                    ╰── here
 6 │ }
   ╰────

The error points at the addition in main, where the string was finally used. The value of the wrong type was let through by the if in pick, and the two places can be much further apart. A checker that generalized let r = ref []; would accept this program:

fn main() {
    let r = ref [];
    r := [1];
    r := deref r ++ ["one"];
    println(deref r);
    println(len(deref r));
    for x in deref r { println(x + 1); }
}

When run, it would print [1, "one"] and 2, then 2 from the first pass of the loop, and would stop with a TypeError at x + 1 on the second. The list [1, "one"] has no type: no $\tau$ makes $⊢[1,\text{"one"}]:[\tau ]$ hold. Printing it and taking its length succeed, because neither looks at the elements, and the program fails only when an arm finally needs one element to be an integer.

A soundness bug therefore shows up as a left-hand-column error in a program the checker accepted, and the place to look for the cause is the rule that let a value of the wrong type in. That gives a way to test a checker that the conservativeness of the first chapter does not: run each program it accepts and confirm that the evaluator never raises one of those errors. A checker that rejects too much fails tests that expect a program to run; a checker that accepts too much fails this one.

The design space

Stating soundness one step at a time

Andrew Wright and Matthias Felleisen’s “A Syntactic Approach to Type Soundness” (1994) proved soundness without a value like wrong and without a denotational semantics. They gave the language a small-step semantics, in which a program rewrites one step at a time, and observed that “each intermediate state may be assigned the same type as the original program, i.e., reductions preserve type”, a property they called by its name from combinatory logic, subject reduction. A second observation completed it: “sound type systems do not assign a type to irreducible expressions that are the sources of type errors, such as 1 + true.” A well-typed program can then never step to a stuck expression. The method extended without much change to references, exceptions, and continuations, and they used it for the core of Standard ML. It became the usual way to prove a language sound. Textbooks now state the two halves as preservation, that a step keeps a well-typed expression’s type, and progress, that a well-typed expression is a value or can take a step.

The small-step statement separates what big-step cannot. A program that runs forever takes steps forever, and a stuck one stops at an expression that is neither a value nor able to step, so “never gets stuck” is a claim about the semantics alone. This chapter’s statement leans on the interpreter instead, on errors it reports, and its proof sketch follows the shape of the evaluator, one case per arm. Both say that types are kept as the program runs; they differ in what a run is.

Unsound by design

Some typed languages decline the guarantee. TypeScript’s design goals list among their non-goals: “Apply a sound or “provably correct” type system. Instead, strike a balance between correctness and productivity.“ Its checker accepts some programs that can go wrong, in order to type patterns common in existing JavaScript, and such a program then behaves as the JavaScript it compiles to. Dynamic and gradual typing takes up languages that mix typed and untyped code.

A language can also admit a known gap in its types and close it with a check at run time. In Java a String[] is a subtype of Object[], so an array of strings can be passed where an array of objects is expected, and the receiver can try to store an Integer in it. The Java Language Specification §10.5 handles it at the store: “an assignment to a component of the array is checked at run time”, and a wrong one throws an ArrayStoreException. Java programs stay safe, in the sense of Cardelli’s table, at the cost of a runtime error the types were meant to exclude. Dart, which shipped with optional, unsound types, made its type system sound in Dart 2.0 (2018); its documentation says that it “enforces that soundness using a combination of static checking (compile-time errors) and runtime checks.” Bertrand Meyer’s “Static Typing” (1995) discusses a gap in Eiffel: a subclass may narrow the type of a method’s argument, and a call through the parent class can then pass an argument the subclass’s method does not accept. He named such calls catcalls.

Unsound by accident

Soundness is a property of a set of rules, and the rules of a large language interact in ways their designers did not foresee. Adding reference cells to ML’s polymorphism gave a checker that accepted programs that go wrong, and several repairs were proposed before the one Standard ML adopted; Wright and Felleisen’s paper gives a counterexample and proves a repaired language sound. Nada Amin and Ross Tate’s “Java and Scala’s Type Systems are Unsound” (2016) states in its abstract: “We present short programs that demonstrate the unsoundness of Java and Scala’s current type systems.” Their programs combine generics with null to convert a value of any type to any other without a cast. The Java virtual machine checks types itself when the program runs, so the conversion is caught there.

For a language the size of Standard ML, a proof on paper is long enough that its own errors are a concern. Daniel Lee, Karl Crary, and Robert Harper’s “Towards a Mechanized Metatheory of Standard ML” (2007) checked a type-safety proof for the whole language by machine, in the Twelf proof assistant, by way of an internal language with the same expressive power.

Further reading

Proving soundness: Pierce’s Types and Programming Languages (MIT Press, 2002) proves progress and preservation for a language of booleans and numbers in chapter 8, for the simply typed λ-calculus in chapter 9, and adds references, with a store typing like $\Sigma$, in chapter 13. The Programming Language Foundations volume of Software Foundations carries out the same proofs in the Coq proof assistant, with every step checked by machine. Wright and Felleisen’s “A Syntactic Approach to Type Soundness” (1994) gives the method in full, with the polymorphic-reference counterexample and the proofs for references, exceptions, and continuations.

Semantic soundness: Milner’s “A Theory of Type Polymorphism in Programming” (1978), §3, defines the semantics with wrong, gives each type its set of values, and proves Theorem 1; the argument assumes some familiarity with domain theory.

When soundness fails: Amin and Tate’s paper (2016) builds its counterexamples up from small programs and explains which feature contributes what.

Concept checks