Null on trial

At the end of the last chapter, Python’s compiler translated "hello" * {}, a string multiplied by an empty dictionary, into bytecode without a single complaint, and the error surfaced only when the program ran. The check function in the Ognivo compiler made sure only that every name had a value; what kind of values they were, and what could be done with them, was nobody’s concern. Now hide the same line in a branch the program rarely takes.

The function is defined, two calls go through, and the third one crashes, at the moment the name “Hoare” comes into the program. In a production program, that might happen a day or a year after it was written. Yet the error can be seen in the text: no name makes it all right to multiply a string by a dictionary. Couldn’t a machine read the program and find such places in advance, without running it?

It could. But first, a word about an error that such checks let through for decades and that is probably still the most common one in the history of programming. It has an inventor, and he has pleaded guilty.

Case No. 53

This chapter is a trial. The defendant is null, the “null reference”: a value that means “there is nothing here.” In Python it goes by None, in C by NULL, in Go, Ruby and Swift by nil, and JavaScript has two of them, null and undefined. The prosecution will present crashed programs and a spacecraft lost at Mars; the defense will answer with convenience and speed. In between, expert witnesses will explain what a type is and how a machine finds types that nobody wrote down, and ordinary witnesses will take the stand: programming languages that have dealt with the defendant in different ways.

You sit on the jury. Once you have heard both sides, you will deliver a verdict, and then you will write a type checker yourself, a program that finds "hello" * {} before anything runs.

The prosecution: the inventor confesses

To see what broke, recall what a type promises. In Chapter 2 a value’s type told you what you could do with it: strings can be joined and sliced, numbers added. A reference of type “employee record” promises that an employee record lies at the other end, and you can ask it for a surname. A null reference breaks that promise. It is allowed into a variable of any reference type, but you can’t ask it for a surname, because there is nothing at the other end. In C the null pointer is address 0, and, as we saw in Chapter 38, the page containing that address is deliberately given to nobody: dereferencing it ends in a segmentation fault. Java throws a NullPointerException. And in Python, None turns up from places where nobody expects it.

Four different roads, and at the end of each one a None that neither the function’s name nor its call warns you about. The last line fails with an error that everyone who has written Python for more than a week has seen: 'NoneType' object has no attribute 'upper'. Worst of all, the program fails in one place, while the error was born in another. None can travel through a dozen functions before anyone asks it for an attribute, and the traceback will show where the program fell, not where the emptiness appeared.

SQL has a NULL too, but it is a different thing: a mark in a table cell saying “the value is unknown,” and SQL at least doesn’t hide it, since any comparison with it gives “unknown.” On trial here is a reference that passes itself off as anything at all.

Expert testimony: what is a type?

Before it judges, the court hears an expert. For the purposes of checking, it is convenient to define a type as a set of values together with the operations allowed on them. int is the integers and everything done with them: addition, comparison, remainder. str is the strings, joining them, searching them, multiplying them by an integer. A type error is an operation applied to a value outside its set: multiplying a string by a dictionary, asking None for .upper().

Python always catches such errors, but at the last moment. Every value in Python carries a tag with its type, and the BINARY_OP instruction looks at the tags of both operands before it multiplies. This is the dynamic checking of Chapter 49: reliable, but late. Static checking reasons about a program without running it: for every expression it works out a type from the text and compares it with what is expected. A program that does this is called a type checker, and the rules it reasons by are a type system.

Python has such a program: mypy. Jukka Lehtosalo, a Finnish PhD student at the University of Cambridge, started writing it in 2012. In 2014, with Guido van Rossum and Łukasz Langa, he wrote PEP 484, an agreement on how to write types right in the text of a program. A parameter’s type goes after a colon, the result’s type after an arrow: def greet(name: str) -> str. Such marks are called type annotations. Python itself doesn’t check them (the PEP says outright that “Python will remain a dynamically typed language”); mypy reads them. It is installed in the course sandbox, and a cell calls it through the module cs.typecheck: the function mypy(text) prints what it found. Line numbers count from the first line of code in the text you pass.

With annotations, mypy found the error in a second without calling greet once: you don’t multiply a string by a dictionary. Without annotations it kept quiet, and that is deliberate. mypy treats a function without a single annotation as territory it wasn’t invited into: every value there gets the type Any, “anything,” with which everything is allowed. That way types can be added to a big program gradually, function by function, and old code doesn’t drown in thousands of messages. This approach is called gradual typing. The --strict flag withdraws the concession: then mypy demands annotations on every function.

Presumed guilty

In one respect a court for programs runs on the opposite principle from a court for people. A court that tries a person presumes innocence: every doubt counts in favor of the accused. A type checker presumes the opposite. If it can’t prove that an operation is safe, it rejects the program, even a program that works. So that you can watch both courts at once, from here on we call mypy a different way. The line mypy_cell() at the top of a cell hands it the text of the cell itself, with the line numbers you see on the page, prints its verdict, and then the cell runs as usual.

The run shows that the program is correct: x is a number only when verbose is true, and only then is one added to it. But to see that, you have to follow the link between two branches, and mypy remembers a single fact about x: “a number or a string,” int | str. You can’t add one to that, nor return it as a string, so mypy reports two errors. It won’t guess.

Sometimes a checker has no choice but to reject the innocent: a perfect checker, one that could tell for any program whether a type error will happen in it, does not exist. That follows from a theorem we will prove in Chapter 56. What remains is to choose which way to err. A type system that never lets the guilty go is called sound; the price of soundness is turning away the innocent. There is some consolation: what the checker can’t follow is often hard for a person to follow too. Rewrite label so that each branch builds its own string, and mypy will agree, and the function will get simpler.

A witness for the prosecution: the spacecraft at Mars

null plays no part in the prosecution’s second episode, but the episode shows the same trait of types: they promise less than we think. It happened two years after the Pathfinder of Chapter 39 landed on Mars.

Seen through the eyes of a type system, the story looks like this. In the Lockheed Martin program and in the navigators’ program alike, the impulse is a floating-point number, a float. The types matched; there was nothing to check. A number standing for 4.45 newton-seconds and a number standing for one are indistinguishable to the type system: float knows that it holds a number, but not a number of what. Could units be made part of the type? Try the calculator below, where every number travels together with its unit.

The calculator catches two different kinds of error. The first is a dimension error: meters can’t be added to seconds in any units at all, and the calculator rejects such a line. The second kind is sneakier, and it is the one the orbiter made: the dimensions are right, an impulse is added to an impulse, but the units differ. If each number carries its unit, the calculator converts one into the other, and there is no error: 1 lbf*s + 1 N*s is about 5.45 newton-seconds. Trouble starts where the unit gets lost: one program prints a bare number to a file, another reads it and assigns its own unit. In the preset “orbiter: bare numbers” every dimension agrees, and the answer is off by a factor of 4.45.

Units in the type

There are three ways to make a machine keep track of units. The lightest one comes with mypy: NewType creates a new type out of an old one. To Python at run time, NewtonSeconds(10.0) is the same old number, but mypy treats NewtonSeconds and PoundSeconds as different types and won’t let you pass one where the other is expected.

mypy rejected the first call: pound-force seconds are not newton-seconds. At run time, though, the same call went through without a murmur, because Python doesn’t check annotations, and the navigators “applied” 12 newton-seconds instead of 53.4. The second call passed because the conversion is written out: multiply by 4.448, and only then call the result newton-seconds. Still, NewType knows no physics: it won’t stop you from calling a number newton-seconds when you forgot to multiply it. All it requires is that every conversion from one unit to another be written in the text, where a reader can see it.

The second way is to carry the unit along with the number at run time: an object holds a value and a dimension, and addition and multiplication check the dimension and work out the new one. That is how the calculator above works, and libraries such as pint; you will write such a class in the task “Units under control.” The error comes to light only while the program runs, at the first computation, but it always comes to light. The third way is to build units into the type system itself. The language F# does this: units of measure arrived in version 2.0, in 2010, designed by Andrew Kennedy. There 100.0<m> / 5.0<s> has the type float<m/s>, the compiler won’t let you add meters to seconds, and at run time not a trace of the units remains, so they cost nothing.

But all three ways share one limit, and the orbiter’s error sat right on it. The two programs lived in different organizations and exchanged a file. A type lives inside a program; a file holds digits, and between programs the only thing that can keep track of units is the interface specification, which people read. The orbiter had a specification, and the units in it were right. Two working rules come out of the story. Put the unit into the data itself: a field called impulse_newton_s is harder to misread than impulse. And test the seams: run real data through both programs together, as the Ariane 5 inquiry board advised in Chapter 11.

The defense

The prosecution has spoken. The defense asks the court to hear four arguments.

First: emptiness is needed. A key may be missing from a dictionary. A search may find nothing. A value may not be computed yet, a file not yet opened, a person may have no middle name. Every language needs a way to say “there is nothing here,” and None is the shortest. Take it away, and programmers will start inventing substitutes: −1 for an index, an empty string for a name, a zero date. A substitute is worse than the original, because −1 can be added to another index by mistake, and the program won’t even crash.

Second: it costs nothing. A null reference is a zero in a pointer and no more. It takes no extra memory, and the check p == NULL costs one comparison. Any wrapper of the “a value or nothing” kind needs room for a flag and time to check it. In C, in an operating system kernel or in a rocket’s firmware, where every cycle counts, such costs show.

Third: freedom. In Python without annotations, a program gets written in an evening, without explaining to the machine what is obvious anyway. The duck typing of Chapter 12 works with any object that can do what is needed. Annotations take time, and the checker, as we have seen, sometimes rejects correct programs. It is no accident that the authors of PEP 484 promised that annotations in Python would never become mandatory.

Fourth: types don’t catch everything. The Ariane 5 software in Chapter 11 was written in Ada, a language with strict static typing. Converting a 64-bit floating-point number into a 16-bit integer was legal as far as the types were concerned; it was the value itself that didn’t fit. Types let the orbiter’s error through too: float matched float. A wrong formula, two arguments of the same type swapped, a forgotten branch of logic: the type checker sees none of these. Tests are needed anyway.

The prosecution replies. To the first argument: emptiness is needed, but it doesn’t follow that everything may be empty. What Hoare regretted was emptiness creeping into every type; it is enough to tell “a string” apart from “a string or nothing,” and the checker will see to it that the second is never taken for the first. To the second: in Rust the type Option<&T>, “a reference or nothing,” is guaranteed by the language to take as much memory as a reference, and the “nothing” in it is stored as the same zero. The machine code is the same as in C; the only difference is that the compiler won’t let you forget the check. To the third: gradual typing has already left room for freedom, since annotations go in where and when they pay for themselves. The fourth argument the prosecution accepts: types don’t catch everything. But what they catch, they catch in every run, while a test catches it only in the runs you thought of.

The weighing of arguments comes at the end. The defense complained that types have to be written by hand, and to look into that, the court calls a second expert.

Expert testimony: types that nobody wrote

Take the function lambda x: x + 1. Nobody said that x is a number, but you can see it: one is being added to it. So the function takes an integer and returns an integer. The function lambda x: x, meanwhile, returns whatever it was given and doesn’t care what that is: its type is “from anything to the same thing.” A machine can reason the way you did a moment ago and find types that aren’t in the text.

The first to do this rigorously was the logician Roger Hindley: in 1969 he proved that for the expressions of combinatory logic the most general type, if there is one, can always be found by an algorithm. In 1978 Robin Milner, in Edinburgh, unaware of Hindley’s work, devised the same method for ML, the language in which he was writing a theorem-proving system; his version is called algorithm W. The same paper contains a phrase that everyone who works on types has been repeating ever since: “Well-typed programs cannot ‘go wrong.’” In 1982 Luis Damas proved that Milner’s algorithm always finds the most general type when one exists. The method is called Hindley–Milner type inference, and ML, OCaml, Haskell and F# are built on it; Rust and Swift use its relatives.

The idea fits into three steps. Give every unknown type a name, an unknown: t1, t2, … Every use gives an equation: if f is applied to x, then f is a function whose argument has the same type as x. Solve the system of equations by substituting what you have found into the rest; this is called unification, and John Alan Robinson invented it in 1965 for automated theorem proving. An unknown that stays unknown to the end means “any type”; such unknowns are printed as 'a, 'b. Below is type inference for one-line Python functions, the lambda of Chapter 10. The text is parsed by the ast module from Chapter 50, and the language is tiny: integers and booleans, addition, comparison, calls and the conditional expression.

Read the third example. f(x) gives the equation “f is a function from the type of x to something”; f(f(x)) gives another one: “the result of f will also do as its argument.” Unification boils them down to this: the argument and the result of f have the same type, and which type doesn’t matter. The answer is ('a -> 'a) -> 'a -> 'a: the function takes a function from anything to the same thing, then a value of that type, and returns another one like it. The text contains no types at all, yet inference produced an exact description that fits numbers and strings alike. The fourth example resisted inference: x serves as a condition, so it is a bool, while the branches return 1 in one case and x in the other, and nothing can be an integer and a boolean at once. The fifth requires the type of x to be a function that takes itself: the equation t8 = t8 -> t9 has no solution, any more than $x = x + 1$ does.

mypy is more modest. It infers the type of a local variable by itself: after xs = [1, 2] it knows that xs is a list[int]. But it takes a function’s type only from the annotations: a function without a return annotation returns Any as far as mypy is concerned. This is by design. In a language with inheritance, overloading and mutable objects, pure Hindley–Milner inference doesn’t work, and a function signature written out in full serves as documentation that the machine checks.

The witnesses: languages

The court calls its witnesses. Each language gets the same assignment: find a user by name and print the length of their email address. The user may not exist. The court asks each witness what it will say about such a program before it runs, and what will happen when it does.

The witnesses fell into three groups. In the first are C, Java, JavaScript and Python without annotations: emptiness is allowed anywhere, and you find out about it at run time. C crashes with a segfault, or worse, since dereferencing a null pointer is undefined behavior, and an optimizing compiler is entitled to assume it never happens. Java throws a NullPointerException, JavaScript a TypeError, Python an AttributeError.

In the second group are Kotlin, Swift, TypeScript in strict mode, C# since 2019, and Python with mypy. Emptiness is still there, but under supervision: a String can never be null, a String? can, and before you call a method you have to prove to the checker that the value is there. Kotlin’s documentation presents this part of the language as a way to reduce “the risk of null references, also known as The Billion-Dollar Mistake.” The third group is Haskell, OCaml and Rust, whose ordinary types have no empty value at all. “Maybe nothing” is a separate type, Maybe in Haskell, Option in Rust, and the value comes out of it only when both cases are handled.

Exhibit A: Optional

Python with mypy is in the second group. The type “a string or nothing” is written str | None; older code also has Optional[str], which means the same thing. Such types are called option types. To mypy, str and str | None are different types: the first is never None, and the second can’t be used as a string until it has been checked that a string is there.

mypy found one error, in shout, where the result of the search is told to shout straight away, and the run confirmed it with the familiar AttributeError. shout_safely has no error, even though name is declared as “a string or nothing.” The check if name is None: return cut off the empty case, and after it mypy knows that name is a str. This is called type narrowing: a check in the program becomes a proof for mypy. if name: narrows types too, and so do isinstance and match.

The playground below is for your own experiments: edit the cell, run it and check it with mypy. The most interesting cases are those where the two verdicts disagree: mypy finds an error and the run goes fine, or the other way around.

mypy has loopholes, and it is worth knowing them, so as not to trust it more than it promises. The type Any switches off checking for everything that passes through it. assert x is not None narrows a type, but it is a promise that is checked only at run time. typing.cast tells mypy to take your word for it. Big programs can’t do without them, but each such place is a signed note: “here I answer for it, not the checker.”

The prosecution proposes: algebraic types

The third group of witnesses does without null entirely. Instead of one type that emptiness sneaks into, it describes data as a choice among several variants. In Haskell the type “maybe nothing” is declared in one line, data Maybe a = Nothing | Just a: either nothing, or Just with a value inside. The vertical bar reads “or.”

Data types are put together with two operations. A record is “and”: a point on the screen is x and y. If x has 1920 possible values and y has 1080, there are $1920 \cdot 1080$ possible points, a product. A variant is “or”: a shape is a circle or a rectangle, and the number of possible shapes is the number of circles plus the number of rectangles, a sum. Types built from sums and products are called algebraic data types, and that arithmetic is where the name comes from. Maybe a is “type a plus one value”: one more possibility, no more. That one is the same emptiness, only written into the type, and it has no way into other types.

In Python a product is a class with the @dataclass decorator, which writes __init__, __repr__ and __eq__ for you from the list of fields. A sum is a union of types with |. Variants are taken apart with the match statement, which arrived in Python 3.10: it tries the value against patterns in turn and pulls out the fields at the same time. This is called pattern matching. The most valuable part is that mypy checks that the matching is exhaustive. If the last branch says assert_never(s), “control never gets here,” mypy makes sure every variant has been handled before it, and if one has been forgotten, mypy names it.

The triangle was added to the union but forgotten in area, and mypy pointed at assert_never: a Triangle can get there. At run time the rectangle’s area was computed, while the triangle reached assert_never and the program crashed with an AssertionError: the same error, only now in front of a user. In a program of a thousand files such a check is a lifesaver: add a new variant, and the checker lists every place that doesn’t handle it. Failures are described the same way. A function returns either a result or a description of an error (in Rust this type is called Result), and the caller can’t forget about failure, because to get at the result it has to handle both variants. The exceptions of Chapter 11 can’t do that: a function’s signature says nothing about them.

Expert testimony: types with a parameter

We have already written list[str] and dict[str, int]. A bare “list” is a template waiting for the type of its elements: list[int] and list[str] are different types, and mypy won’t let you put a string into a list of integers. Such types are called generic types. Since Python 3.12 a generic function of your own is declared like this, with the type parameter in square brackets after the name:

T is the same kind of unknown as 'a in Hindley–Milner: at every call mypy puts the type of the argument in its place. reveal_type asks mypy to say which type it inferred; this is a note, not an error, and the if TYPE_CHECKING block is read only by the checker, while Python skips it. For a list of numbers first returns “an integer or nothing,” for a list of strings “a string or nothing.” mypy rejected the line n + 1, even though at run time it printed 4, since the list [3, 1, 2] isn’t empty. But mypy judges all runs at once, and first([]) on the same line shows what could come back another time.

The highest court: proofs

Courts have levels of appeal, and so does the checking of programs. A test from Chapter 11 asks a program about a few inputs that a person chose and says nothing about the rest. A type checker speaks about all inputs at once, but about only one kind of error: no operation will get a value of the wrong type. The next level up is to prove that, on any input, the program does what its description says. Programs that a great deal depends on have already been checked this way.

In 2009 a group at NICTA, an Australian research center, completed a proof of correctness for seL4, an operating system kernel written in 8,700 lines of C and 600 lines of assembly. They proved that the kernel behaves as its formal description requires: it never crashes, never dereferences a null pointer and never hangs in an endless loop. The proof ran to about 200,000 lines for Isabelle/HOL, a proof assistant that checks every step. The kernel’s code cost about two person-years, the proof about twenty.

Since 2005 Xavier Leroy at INRIA, a French research institute, has been building CompCert, a C compiler for which it is proved, in the Coq system, that a compiled program behaves the same as its source. The compiler was put through a hard test. In 2011 a group at the University of Utah published the results of three years spent hunting for compiler bugs with Csmith, a program that generates random valid C programs. They found more than 325 bugs in GCC, LLVM and other compilers; every compiler they tested crashed at least once and at least once silently produced wrong code. In CompCert, bugs turned up only in the parts the proof didn’t cover. The “middle-end” bugs found in every other compiler were not in it, though about six CPU-years went into the search.

But the highest court also judges by a law that people wrote. A proof says that the program matches its description. It won’t find an error in the description itself, and the seL4 authors admit as much: “A cynic might say that an implementation proof only shows that the implementation has precisely the same bugs that the specification contains.” The difference is that the specification, written in the same notation, is a third the size of the code and simpler. What we get is a ladder. Tests are cheap and catch particular cases; types catch one kind of error in every run; a proof catches everything that contradicts the description, but for seL4 it cost ten times as much as the program itself.

The verdict

Both sides have rested, and the jury takes over. Below are all the arguments heard during the trial, six from each side. Decide for each one whether it convinces you, and the scales will show which way you lean. The verdict that comes out is your own position: the court doesn’t know the right answer, and the languages, as you have seen, decided differently.

History, meanwhile, is reaching a verdict of its own. Kotlin, Swift and Rust, which appeared in the 2010s, don’t let emptiness into ordinary types unsupervised. C# added references that can’t be null in 2019, and Dart moved the whole language over to them in 2021. Java added the Optional type in 2014, but null is still allowed in any reference, and billions of lines of old code can’t be rewritten. Python left the decision to you: annotations and mypy are optional.

Whatever your verdict, the trial leaves a few rules for tomorrow. Write annotations at least on the functions that other people use: the signature def find(...) -> User | None warns about emptiness better than any comment, and a machine checks it. Run mypy as regularly as your tests; in a big program it finds forgotten None checks before the users do. Describe variants as a union of types and take them apart with match and assert_never. Keep units in names and types. And remember the defense’s fourth argument: tests are needed anyway.

Tasks

Four tasks. In the first you get past mypy in strict mode; in the second and third you write tools that no program working with other people’s data can do without; and in the fourth you write the type checker promised at the start of the chapter.

What next

The verdict is in, but both sides agreed on one thing: types don’t catch everything. Here is a function that mypy has nothing against. Its types fit together, and its annotations are in place.

mypy is satisfied, and on these numbers the function answers: 97 gets to 1 in 118 steps. But will it stop for every integer n greater than zero? That is the Collatz conjecture from Chapter 0, and nobody knows the answer. A program that hangs can be worse than one that crashes: a crashed program gets restarted, a hung one gets waited for. Could we write a stronger check, a program that reads any program and says whether it will stop?

To answer that, we need a rigorous account of what a program is and what the machine that runs it is. Python, Iskra-8 and the Lisp interpreter of Chapter 51 are too complicated to reason about rigorously. We will start with the simplest machine. It has no variables, no stack and no tape, only a finite number of states and rules for moving between them. It can do a fair amount, for instance check whether a string looks like a date or an email address. But telling whether parentheses are properly balanced is beyond it. That machine, and the language in which it is given its orders, are the subject of the next chapter.