Types: what they can and cannot prove

1. Slide 1

   A proof, quantified over every run

   The distinguishing feature of a type checker is not what it catches but how much it covers.

   function first(xs: string[]): string {
     return xs[0].toUpperCase();
   }

   The checker will accept this, and in accepting it makes a claim about every call that will ever be made: whatever xs turns out to be, it will be an array of strings. No test does that. A test tells you about the inputs it was given, and there are usually more inputs than that.

   The claim is also checked before the program runs, which changes the economics of finding a mistake. A type error is found in the editor, by the person who made it, seconds after making it. The same mistake found dynamically may be found by a customer, six weeks later, in a stack trace with none of that context. Both are the same bug and they cost very different amounts.

2. Slide 2

   What a type system actually rules out

   It is worth being concrete about the class of errors, because it is narrower than the reputation.

   A type system rules out applying an operation to a value of the wrong shape. Calling a method that is not there. Passing three arguments where two are expected. Adding a number to a function. In a language with sum types it also rules out forgetting a case, which is a genuinely different and more interesting guarantee, and it is the one that makes people who have used it reluctant to go back.

   Notice the example above. xs[0].toUpperCase() typechecks, and on an empty array it throws, because most type systems say that indexing an array of strings yields a string and decline to mention that the array might be too short. The checker proved exactly what it promised. It simply did not promise that.

3. Slide 3

   What it cannot rule out

   The list of things a mainstream type system says nothing about is longer than the list of things it catches.

   function days(a: Date, b: Date) {
     const gap = b.getTime() - a.getTime();
     return gap / 86400;
   }

   Every type is correct. The function is wrong by a factor of a thousand, because milliseconds are not seconds, and no type checker in ordinary use will say a word about it. Nor will one tell you that a list is sorted, that an index is in range, that a lock is held, that money and mass should not be added, that the two branches of a conditional do the same thing, or that the function does what its name says.

   Some of these are expressible in the more powerful systems — units of measure, refinement types, dependent types — and those systems exist and are used. What they cost is a much larger proof burden, borne by whoever writes the code, and that is a real trade rather than a free improvement.

4. Slide 4

   Soundness, and the languages that gave it up

   There is a technical property lurking under the word "safe", and the popular languages have taken conspicuously different positions on it.

   A sound type system never accepts a program that will commit a type error at runtime. It is a strong guarantee, and it forces the checker to reject some programs that would in fact have been fine, because it cannot prove that they are. Every sound system rejects correct programs; that is the deal.

   TypeScript is deliberately not sound, and says so in its own documentation. Array indexing, the any escape hatch and the way class fields are checked all admit programs that will fail. This was a design decision rather than an oversight: the goal was to describe JavaScript as it is actually written, and soundness would have meant rejecting a great deal of working code. Java's array covariance is a similar hole, patched with a runtime check. Whether an unsound checker is worth having is a fair question, and the honest answer is that it catches most of what it aims at and you must not treat its silence as a proof.

5. Slide 5

   Gradual typing, and what it is really for

   The last fifteen years quietly ended the argument in practice, by letting one program be both.

   TypeScript, Python's annotations, Ruby's signatures and PHP's types all let a codebase start untyped and acquire types where they pay. This is not a compromise between two camps so much as an acknowledgement that the value of a type varies enormously by location. At the boundary of a system — where data arrives from a network, a form, another team — a type is a description of a contract with someone who may not honour it, and worth a great deal. Deep inside a pure function that is called from three places, it is worth much less.

   The pattern that has emerged is to type the boundaries heavily, validate at them, and let the interior be as strict as the team finds comfortable. It is less ideologically satisfying than either original position and it is what almost everyone now does.

6. Slide 6

   Types and tests answer different questions

   The most common bad argument on both sides is that one of these replaces the other.

   A type says something weak about every possible execution. A test says something arbitrary about one. The two are not competing; they cover different axes, and a program with neither is in a worse position than a program with either. What is true is that they overlap at the margin: a language with sum types and exhaustive matching removes a category of test that a dynamic language must write by hand, and a thorough test suite catches shape errors eventually, at greater expense and later.

   The interesting question is not which to have but where the boundary sits for a given system, and it moves. A four-file script does not need either. A payments ledger maintained by thirty people over eight years needs both, and needs them mostly at the edges where the shapes are least under its control.

7. Slide 7

   The honest summary

   What the evidence supports is narrower than either camp's rhetoric, and it is still worth stating.

   Types find shape errors early and cheaply, and the earlier something is found the less it costs. They are documentation that cannot go stale, which is the only kind that stays true. They make large-scale change tractable, because a rename that the compiler follows is a different activity from a rename you must search for. Those are real, and they are why untyped codebases past a certain size tend to grow a type checker.

   What they do not do is make a program correct, and the temptation to believe otherwise is the one genuine hazard. The most dangerous line in any typed codebase is the one where a value crosses in from outside, wearing a type somebody asserted rather than checked. Everything downstream is then reasoning carefully from a premise that was never established, which is a more expensive kind of wrong than having no types at all.

← All lecturesAtrium