Types as propositions

Here’s the move that changes how you write code. Stop thinking of a type signature as documentation. Start thinking of it as a claim you are making, which the compiler will refuse to typecheck unless you have provided a proof.

val parse_request : bytes -> (request, parse_error) result

This signature claims: “I can transform any byte buffer into either a well-formed request or a parse error, with no other outcomes.” If your implementation can panic, throw, return null, or block on I/O without that being in the type, the signature is lying and the compiler will catch it (mostly — effects are the loophole and we will address them).

Curry-Howard, taken as engineering practice

The Curry-Howard correspondence makes this precise: types correspond to propositions, programs correspond to proofs, evaluation corresponds to proof normalization. You don’t need to take this seriously as logic to take it seriously as engineering practice. The engineering practice is: write the type first, and let the compiler tell you what’s missing.

A short example. You want a function that takes a non-empty list and returns its head:

val head : nonempty_list a -> a

The type promises that you always return an a. If you write the function to handle the empty case by raising an exception, the type is lying. To not lie, you must encode the non-emptiness in the type — make a nonempty_list type whose values are always at least one element long:

type nonempty_list a = { hd : a; tl : list a }

let head (xs : nonempty_list a) : a = xs.hd

Now there’s no way to construct a nonempty_list that doesn’t have a head. The function cannot fail. The signature is honest. The compiler enforces it.

The discipline cascades. Anywhere you would have written xs.head_or_raise(), you now write xs.head, no exception path, no defensive check. The invariant that the list is non-empty has been moved from runtime to compile time, and that’s the single highest-leverage move available in software engineering. Every site that handles the list no longer needs to know what to do if it’s empty, because empty isn’t representable.

Why this matters for systems work

The shape of your control plane’s state machine is a type. The shape of a wire protocol is a type. The shape of “this resource has been acquired but not yet released” is a type — we’ll meet this one as linear typing in chapter 13. The shape of a packet whose checksum has been verified is a type, distinct from the shape of an unverified packet.

If you can encode an invariant in the type system, you do not have to test for it, document it, or hope code review catches it. You have moved it from runtime to compile time. The number of bugs that survive this move is dramatically smaller than the number that survived being “documented in the function comment.”

A concrete example from this book’s design conversation: continuations are linear. The type system tracks that a continuation can be invoked at most once. The kernel cannot accidentally invoke a continuation twice, because the second invocation is a type error. The class of bugs called “use-after-resume” is structurally absent from any kernel written in this language. Not “tested away,” not “carefully avoided by senior engineers” — structurally absent.

This is what “ontologically minimal” design looks like from the inside. You let the domain dictate the algebra. You encode the algebra in types. The program writes itself in the negative space.

The discipline of writing types first

The practice is: when you start a new function, write its type before its body. Stare at the type. Ask: is this honest? Does it admit all the success cases? Does it disallow all the failure cases I cared about? Does it accidentally permit something I’d want to forbid?

If the type isn’t honest, fix the type first. Maybe you need to refine the input type (only non-empty lists). Maybe you need to refine the output (return a result so callers must handle the error case). Maybe you need to add an effect annotation (this function performs I/O; say so).

Once the type is honest, the body is constrained. There are usually far fewer plausible implementations of an honest type than of a vague one. The honest type guides you.

Look at the difference:

(* Dishonest: what happens if x is negative? *)
val sqrt : float -> float

(* Honest: we admit it might fail *)
val sqrt : float -> float option

(* More honest still: refuse to take a negative input *)
val sqrt : nonneg_float -> nonneg_float

The third form is most honest, but requires you to construct nonneg_float values somewhere — which is fine, that work has to happen anyway, it just gets pushed to the boundary where the float enters the program.

The compiler as a colleague

Treating types as propositions reframes the compiler from “a thing that yells at me about syntax” to “a thing that’s checking my work.” Every type error is the compiler saying: you claimed X, but your code does not prove X. Either fix the code or fix the claim. This is a useful thing for a colleague to do.

You will, in practice, sometimes spend an hour fighting the type checker over a single function. This is not a sign that ML is hostile; it is a sign that you wrote a claim you can’t support, and the compiler is refusing to let you ship it. After enough rounds of this, you develop the instinct to write more honest claims at the start, and the fights get rarer.

This is the same loop as test-driven development, but cheaper — the “tests” are types, which are written more compactly than test cases, and the compiler runs them on every save.

What this chapter committed to

Types are claims; the compiler is the proof checker. Honest types push invariants from runtime to compile time, which is the single highest-leverage move available. The practice is: write the type first, ask if it’s honest, fix it until it is, then write the body.

The next chapter is about the design choice ML and OO have made in opposite directions, and how to tell which one your problem wants.