Afterword

The first chapter put four numbers on a table and told two stories about adding them. Mr. State held a running total. Mr. Fold pressed pairs together until one number remained. Both got 18. That split between stepping through state and folding over structure ran through every chapter that followed: for loops and Reduce(), Turing machines and lambda calculus. Church and Turing proved in 1936 that the two models compute exactly the same class of functions. Any question you can ask of one, you can ask of the other.

Types turned out to be a third way of looking at the same functions. In 1934 Haskell Curry noticed that the types of his combinators read like the axioms of propositional logic, and in 1969 William Howard wrote the match out in full (Types as propositions). A function of type A -> B is a proof that A implies B, a pair of type (A, B) is a proof that both hold, and a program that type-checks is a proof of the theorem its type states. A type checker that accepts the program has checked the proof.

That guarantee is what a mathematician went looking for after finding, in 1999, while lecturing at the Institute for Advanced Study, that a key lemma in a paper he had written six years earlier was wrong and nobody had caught it. The repair took until 2006. Vladimir Voevodsky came out of it wanting proofs a computer could check, and in the foundations he proposed for that, equality is a structure: two values are equal when a path connects them, the path is itself a type, and that type can have its own paths, equalities between equalities.

Paths that connect points, and paths between paths, are what topologists study when they ask which shapes can be deformed into one another. Voevodsky’s equalities obey the same rules, so the whole of homotopy theory maps onto type theory, and a path in a space becomes a term you can type-check and compute with. “Programs are like proofs” and “types are like spaces” kept turning out to be identities. Homotopy type theory is young, and where it leads is open.

The habit of asking what two fields share is older than that. In the early 1940s an algebraist and a topologist found that a calculation from each of their fields was the same calculation, and to say what “the same” meant they had to write down what the two settings had in common. The objects mattered less than the maps between them. The framework Samuel Eilenberg and Saunders Mac Lane published for it in 1945 is category theory. Colleagues called it “general abstract nonsense”, and Mac Lane went on using the name himself.

The structures appeared in this book before their names did. Mr. Fold’s + over four numbers, associative with 0 as its identity, is a monoid. map(x, sqrt) returns a list of the same length with the shape untouched, a functor. as.list(), which gives the same answer whether you map before or after it, is a natural transformation. The laws for all three are in Functors, monoids, and friends.

If you go looking you will find more of these connections, between R and Haskell, between type theory and topology, between the code you write on a Tuesday afternoon and mathematics worked out before there were computers to run it on.

The connections are still forming. R 4.1 gave the language a native pipe (|>) and a one-character lambda (\(x)). R 4.4 added the null-coalescing operator (%||%) that rlang had provided for years, and R 4.3 added two generics through which inherits() and the arithmetic operators consult other object systems, so that S7, a class system that ships as an ordinary package, can sit on top of base R (S7).

The tidyverse’s packages for language models are built the same way. In ellmer you hand the model an ordinary R function and it decides when to call it; mcptools does the same for a coding agent talking to your R session. A function is a value you can pass to a program you did not write (Passing functions to functions), and now the program on the other end can be a model. Church published the lambda calculus in 1936. Ninety years on, a function is still the unit that gets passed around.

Thank you for reading.