Why Types? From Runtime Errors to Static Checking

Every program in Parts II through V has run with nothing between the parser and the evaluator. When an operation receives a value of the wrong kind, the evaluator finds out at that moment and stops with a RuntimeError. describe turns an account balance into a line of text. ++ joins two strings, and the prelude’s to_string converts a value to its text:

fn describe(n: Int) -> String =
    if n >= 0 { "balance " ++ to_string(n) }
    else { "overdrawn by " ++ (0 - n) };

fn main() {
    println(describe(120));
    println(describe(45));
    println(describe(-30));
}

The M4 evaluator prints two lines and then stops:

balance 120
balance 45
  × type error: expected String, found Int
   ╭─[describe.brg:3:12]
 2 │     if n >= 0 { "balance " ++ to_string(n) }
 3 │     else { "overdrawn by " ++ (0 - n) };
   ·            ─────────────┬────────────
   ·                         ╰── here
 4 │
   ╰────

(0 - n) is an Int where ++ needs a String. The mistake is in the else branch, which runs only for a negative balance, so a run that sees only positive balances never reaches it.

A second program has a mistake the evaluator does not report at all:

fn double(n: Int) -> Int = n ++ n;

fn main() {
    println(double("ab"));                              // abab
}

The grammar has required a type on every parameter of a top-level fn since Part I, and double says that n is an Int and that so is the result. Nothing reads those annotations. The evaluator binds n to the string "ab", ++ joins two strings, and the program prints abab.

The two programs raise these questions:

Can the mistake in describe be found without running the program? Nothing in the program says which balances it will be given, so a check made ahead of time cannot know which branch will run.
What would the annotations on double have to mean for double("ab") to be a mistake the language reports?
What does checking ahead of time cost? Which programs that would run without error does such a check turn away, and which runtime errors can it not prevent?

Types entered programming languages to tell a compiler how to store a value and which instructions to apply to it. Using them to find mistakes before a program runs came later.

From storage to checking

The IBM 704 did integer and floating-point arithmetic with different instructions, and its FORTRAN compiler had to know which one each + needed. The FORTRAN Programmer’s Reference Manual (1956) settled it by the spelling of a name: “Two types of variable are also permissible: fixed point (restricted to integral values) and floating point. Fixed point variables are distinguished by the fact that their first character is I, J, K, L, M, or N.” A variable’s type was a fact about how the machine should hold it, read off the first letter of its name.

The Revised Report on Algol 60 (1963) moved the type into a declaration and stated it as a restriction on values. §5.1.3: “Integer declared variables may only assume positive and negative integral values including zero. Boolean declared variables may only assume the values true and false.” Niklaus Wirth’s report on Pascal (1970) put the same idea in the terms this chapter uses: “The data type essentially defines the set of values which may be assumed by that variable.”

Other languages did without types. Dennis Ritchie’s “The Development of the C Language” (1993) describes the two that came before C: “Both languages are typeless, or rather have a single data type, the ‘word,’ or ‘cell,’ a fixed-length bit pattern. Memory in these languages consists of a linear array of such cells, and the meaning of the contents of a cell depends on the operation applied.” BCPL and B ran on word-addressed machines, where the cell was the machine’s word. The PDP-11 addressed individual bytes, which a language whose only value was the word had no way to name, and the floating-point hardware promised for it would need numbers larger than its 16-bit word. Ritchie gives the reasons C acquired types, and what was not among them: “For all these reasons, it seemed that a typing scheme was necessary to cope with characters and byte addressing, and to prepare for the coming floating-point hardware. Other issues, particularly type safety and interface checking, did not seem as important then as they became later.”

In 1973 Tony Hoare argued for the other use. His “Hints on Programming Language Design” (1973), §11, begins from the compiler’s need and arrives at the programmer’s:

The programmer declares the type of each variable, and the compiler can work out the type of each result; it therefore always knows what type of machine code instruction to generate. In cases where there is no meaningful operation (for example, the addition of an integer and a Boolean), the compiler can inform the programmer of his mistake, which is far better than having to chase its curious consequences after the program has run.

The same memo names the property a language has when the mistakes that cannot be caught in advance are still caught when the program runs. Such errors “must be cheaply detectable at run time; in no case can they be allowed to give rise to machine or implementation dependent effects, which are inexplicable in terms of the language itself. This is a criterion to which I give the name ‘security’.”

Robin Milner’s “A Theory of Type Polymorphism in Programming” (1978) gave the type discipline of the language ML. Its checker worked out the types of a program that declared none, and the paper proved what an accepted program was spared. Section 3.7 is titled “Well-Typed Expressions Do Not Go Wrong”, and §3.5 sets up its theorem “that well-typed expressions cannot “go wrong,”” where “wrong” is the result the paper’s semantics gives a meaningless operation, like Hoare’s integer plus Boolean. The guarantee is usually repeated as “well-typed programs cannot go wrong”.

A judgment about types

The rules of Program Semantics relate an expression to the value it produces, $e ⇓ v$ . A check made before anything runs needs a relation between an expression and the kind of value it would produce. The typing judgment

$⊢ e : τ$

reads expression $e$ has type $τ$ . A type names a set of values: Int the integers, Bool the two booleans, String the strings. Appendix D writes the judgment $Γ ⊢ e : τ$ , where the typing context $Γ$ records the type of each variable in scope. The expressions of this chapter have no variables, so $Γ$ is left out here, as Program Semantics left out the environment. It arrives with variables in the next chapter.

Literals have the type of the values they denote:

$⊢ n : Int (T-Int) ⊢ b : Bool (T-Bool) ⊢ s : String (T-Str)$

As in the reference, $\oplus$ stands for an arithmetic operator and $≶$ for an ordering comparison:

$\frac{⊢ e _{1} : Int ⊢ e _{2} : Int}{⊢ e _{1} \oplus e _{2} : Int} (T-Arith) \frac{⊢ e _{1} : Int ⊢ e _{2} : Int}{⊢ e _{1} ≶ e _{2} : Bool} (T-Ord)$

$\frac{⊢ e _{1} : Bool ⊢ e _{2} : Bool}{⊢ e _{1} and e _{2} : Bool} (T-And) \frac{⊢ e _{1} : String ⊢ e _{2} : String}{⊢ e _{1} + + e _{2} : String} (T-Concat-Str)$

Each rule has the shape of the evaluation rule for the same form, with types where the values were. $E-Add$ evaluates both operands and requires them to be integers:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{1} , v _{2} \in Z}{e _{1} + e _{2} ⇓ v _{1} + v _{2}} (E-Add)$

$T-Arith$ requires both operands to have type Int and evaluates nothing. Where $E-Add$ concludes with a particular integer, $T-Arith$ concludes only that the sum will be an integer of some value. The interpreter follows the same division. The evaluator’s addition arm holds two Values and matches each against Value::Int while the program runs; the checker holds the Ty it derived for each operand and compares it with Int before anything runs.

Evaluation and typing have different numbers of rules for if. Evaluation has one rule for each value of the condition, and each mentions only the branch that runs:

$\frac{e _{1} ⇓ true e _{2} ⇓ v}{if e _{1} then e _{2} else e _{3} ⇓ v} (E-If-True) \frac{e _{1} ⇓ false e _{3} ⇓ v}{if e _{1} then e _{2} else e _{3} ⇓ v} (E-If-False)$

Typing has one rule. It does not evaluate the condition, so it cannot know which branch will run, and it requires both branches to have the type the whole if is given:

$\frac{⊢ e _{1} : Bool ⊢ e _{2} : τ ⊢ e _{3} : τ}{⊢ if e _{1} then e _{2} else e _{3} : τ} (T-If)$

(The rules write if e1 then e2 else e3 for Bridger’s braced if, as the reference does.)

A typing derivation stacks the rules as an evaluation derivation does. For if 1 < 2 { 3 } else { 4 + 5 }:

$\frac{\frac{⊢ 1 : Int ⊢ 2 : Int}{⊢ 1 < 2 : Bool} ( T-Ord ) ⊢ 3 : Int \frac{⊢ 4 : Int ⊢ 5 : Int}{⊢ 4 + 5 : Int} ( T-Arith )}{⊢ if 1 < 2 then 3 else 4 + 5 : Int} (T-If)$

The derivation types 4 + 5, a branch that never runs; evaluation reaches 3 by $E-If-True$ and stops.

A program that runs and has no type

fn main() {
    println(if true { 1 } else { 1 + false });          // 1
}

On the M4 evaluator this prints 1. $E-If-True$ evaluates the condition and the first branch, and 1 + false is never evaluated. It has no typing derivation. $T-If$ needs a type for every branch, the only rule that can type a + is $T-Arith$ , and its premise $⊢ false : Int$ is concluded by no rule.

An expression with no typing derivation is ill-typed. A checker built from these rules rejects it whether or not the ill-typed part would ever run. A program with a derivation is well-typed, and the well-typed programs are a strict subset of the programs that run without a type error: if true { 1 } else { 1 + false } is in the second set and not the first.

Why every checker rejects something

A more careful checker could accept that program by noticing that the condition is the literal true. No checker can accept exactly the programs that never stop on a type error. Take any function p with no type error in it, and the program

fn main() {
    p();
    println(1 + true);
}

The program stops on a type error exactly when p() returns. A checker that accepted precisely the programs that never stop on a type error would accept this one exactly when p() runs forever, and so it would decide, for every p, whether p halts. Building that checker would solve the halting problem: given a program, decide whether it eventually stops. Alan Turing showed in “On Computable Numbers” (1936) that no algorithm solves it for every program. H. G. Rice’s theorem (1953) extends the result from halting to every non-trivial question about the function a program computes.

A checker that always finishes is wrong about some programs, then, and its designer chooses the direction of the error: accept some programs that will get stuck, or reject some that would not. Bridger’s checker makes the second choice, as ML’s does. A program it accepts does not stop on any of the errors its types describe, which Soundness, informally states precisely. if true { 1 } else { 1 + false } is the price.

What the types describe

The stuck cases listed in Values and Runtime Errors fall on two sides of that guarantee. A TypeError, applying a value that is not a function (NotAFunction), a call with the wrong number of arguments (ArityMismatch), a field the value does not have (NoSuchField), == on a function (NotComparable), and an UnboundVariable are each predicted by the type of an expression or by the names in scope, and a well-typed program cannot reach them.

Division by zero is not. $T-Arith$ asks only that the divisor be an Int, and 0 is an Int, so println(10 / (5 - 5)) is well-typed and stops with division by zero with or without the checker. Nor can types predict the bound on call depth, the bound on the size of a range, or a failed read from input, since each depends on a value or on the world outside the program. Bridger’s prelude moves one such failure inside the types. head returns an Option, so head([]) is the value None, and a program that wants the element must match on the result.

Bridger’s checker

From Milestone M5, Bridger adds the check as a pass between parsing and evaluation. If every declaration of the program type-checks, the evaluator runs the program; otherwise the program does not start. The provided run method of the interpreter is the whole pipeline:

pub fn run(&mut self, src: &str) -> Result<Value, RunError> {
    self.load_program(src)?;
    self.check()?;
    Ok(self.eval_program()?)
}

Built for M4, check has no passes to run and returns at once. Built for M5, it runs the type checker, and describe produces this, and nothing before it:

  × type mismatch: expected String, found Int
   ╭─[describe.brg:3:32]
 2 │     if n >= 0 { "balance " ++ to_string(n) }
 3 │     else { "overdrawn by " ++ (0 - n) };
   ·                                ──┬──
   ·                                  ╰── here
 4 │
   ╰────

The lines balance 120 and balance 45 are not printed, because main never runs. The checker typed the else branch without knowing that the balance would be negative, by $T-If$ . double is rejected the same way, at the first n of n ++ n: the annotation n: Int is now the type the checker gives n inside the body, and the call double("ab") would be rejected too, for passing a String where the annotation says Int.

The checker reports a mismatch in terms the evaluator already used. Side by side, the variant the evaluator raises when an operation receives the wrong kind of value and the one the checker reports when an expression’s type is not the type its position needs:

// interp/error.rs: raised while the program runs
RuntimeError::TypeError { expected: Ty, found: Ty, span: Span }

// types/error.rs: reported before it runs
TyError::Mismatch { expected: Ty, found: Ty, span: Span }

The fields are the same. The evaluator’s found is read off a value it has in hand; the checker’s is derived by the rules from the program text.

The evaluator is unchanged. Values still carry their variant, and every arm that matches a Value::Int still has a branch that raises a TypeError for anything else. For a program the checker has accepted, those branches never run. The checker passes the evaluator no types; it answers yes or no and the evaluator runs the same program it would have run at M4, with the types discarded.

Bridger asks for types where a function meets its callers: each parameter of a top-level fn, and its result. A let and a lambda’s parameters may omit theirs, and the checker infers them by solving for the unknown types from how the values are used, which is part of what the next chapter builds. Writing the checker is Milestone M5. Its method check_expr is to the typing rules what eval_expr is to the evaluation rules: a recursive walk over the same Expr, one arm per rule, whose recursive calls on subexpressions are the premises of the rule. A typing derivation is the tree of those calls.

The design space

When types are checked

Luca Cardelli’s survey “Type Systems” separates two questions: whether a language has a type system that checks programs before they run, and whether it is safe. Safety is about what happens at an error. “It is useful to distinguish between two kinds of execution errors: the ones that cause the computation to stop immediately, and the ones that go unnoticed (for a while) and later cause arbitrary behavior. The former are called trapped errors, whereas the latter are untrapped errors.” A safe language is one in which no program fragment causes an untrapped error, the property Hoare called security. The two questions give four positions, and Cardelli places a language in each:

	Typed	Untyped
Safe	ML, Java	LISP
Unsafe	C	Assembler

The interpreter of Parts II through V sits in the untyped, safe cell: no check precedes the run, and every type-shaped mistake stops the program with an error at the operation that failed. From M5 Bridger is typed and safe. A language can also check types statically and still let a program get past them. In C, a cast or a union lets a program read the bytes of one type as another, and nothing checks the result at run time; the C standard calls what follows undefined behaviour, so the program’s output is not determined by the language at all.

Writing types down

Languages differ in how many types the programmer writes. Pascal and C ask for a type on every variable and every parameter. ML asks for almost none: Milner’s checker infers the type of every expression from how it is used. Bridger asks for them at function boundaries and infers the rest, so a signature documents what a caller may pass, and the types inside a body are worked out from it; Function types and polymorphism describes how far that inference goes.

A language can also record annotations and leave them unchecked. Python’s type hints, introduced by PEP 484 (2014), are kept with the program, but “no type checking happens at runtime. Instead, the proposal assumes the existence of a separate off-line type checker which users can run over their source code voluntarily.” Python’s annotations play the role double’s did before M5: the program runs as written whatever they say, and a separate tool such as mypy reports the mismatches it finds without stopping the program from running. TypeScript checks its annotations when it compiles and then removes them, producing JavaScript whose values carry no static types at all. Dynamic and gradual typing takes up languages that mix checked and unchecked code in one program.

What a type can say

A type system rules out the errors its types can express, and richer types express more. Rust’s compiler rejects a use of a variable after its value has been moved elsewhere, which rules out, before the program runs, reading memory that another part of the program now owns. Some languages let a type say that an integer is nonzero, or that a list is not empty. Division then requires a divisor whose type says it is nonzero, and the programmer writes the reasoning into the program for the checker to verify. Each extension moves another class of runtime error to the checker, and each asks more of the programmer who has to satisfy it.

Bridger’s checker grows within the book. Part VIII extends it to reject a match that does not cover every value of its scrutinee’s type, which moves NonExhaustiveMatch from the evaluator’s errors to the checker’s.

Concept checks

Evaluation has two rules for if and typing has one. What would a typing rule have to know about the condition to split into two, and why does the checker not have it?

To split as $E-If-True$ and $E-If-False$ do, a typing rule would need the value of the condition, so that it could type only the branch that runs. The checker derives types from the program text before anything runs, and the condition’s value in general depends on inputs, calls, and the store, which exist only at run time. With one rule, the typing of an if holds whichever way the condition turns out, which is what lets the checker say something about every run at once. Requiring both branches to have type $τ$ is the cost.

Which of these stop the M4 evaluator, and which of those does the M5 checker reject before the program runs: 1 + true, 10 / 0, 5(3), (1, 2).5, if 1 < 2 { "a" } else { 0 }?

All but the if stop the M4 evaluator: 1 + true with a TypeError, 10 / 0 with a division by zero, 5(3) because 5 is not a function, and (1, 2).5 because a pair has no component 5. The if prints a, since its else branch never runs. The checker rejects every one of them except 10 / 0, whose operands are both Int; it rejects the if because $T-If$ needs both branches at one type, and "a" and 0 have none in common. So the checker rejects one program the evaluator would have run to completion and lets through one the evaluator stops.

On describe, the evaluator's error underlines the whole "overdrawn by " ++ (0 - n) and the checker's underlines only (0 - n). Why does each point where it does?

The evaluator reports the operation that could not proceed. It evaluated both operands, then the ++ arm found a string and an integer and had no rule to apply, so the error carries the span of the ++ expression. The checker reports the premise that failed. $T-Concat-Str$ needs $⊢ e_{2} : String$ , and the right operand has type Int, so the checker blames that operand. The evaluator sees values when an operation is attempted; the checker sees which subexpression fails to have the type its position needs.

A programmer argues that a checker rejecting if true { 1 } else { 1 + false } is simply wrong and should be fixed to accept it. Could it be? What happens if the fix is pushed as far as it will go?

That particular program could be accepted: a checker could notice the literal true and type only the first branch. Each such refinement makes the checker accept more programs that would run, but none reaches all of them. A checker that accepted exactly the programs that never stop on a type error would decide whether an arbitrary function halts, by the p(); println(1 + true) construction, and no algorithm does that. Every checker that always finishes therefore rejects some program that would have run, or accepts some program that will get stuck. The refinements also make the rules harder to state and to predict: a programmer reading the rule $T-If$ can tell what it will accept, which is harder to say of a checker that tries to evaluate parts of the program.

Python records annotations and its interpreter does not check them; Bridger from M5 refuses to run a program whose annotations are contradicted. What does each choice give the programmer, and what does it take away?

Python’s choice lets every program run, so a program can be tried, partly written or partly wrong, and checked by a separate tool when the programmer chooses. Its annotations can drift from the code without anything stopping the program, and the errors the tool would have reported reach the user at run time instead, as double’s mistake did on the M4 evaluator. Bridger’s choice guarantees that every program that runs agrees with its annotations and cannot stop on a type error, so an annotation is something a reader can rely on. In exchange, a program has to type-check everywhere before any part of it runs, including branches that would never run, like the else in if true { 1 } else { 1 + false }.

A Practical Introduction to Programming Language Design