The Yuan Has Its Angelica: The Mathematical Beauty of Type Systems

For most people, the most exciting things about Rust are the concept of ownership, the power of zero-cost abstraction, and the elegance with which a few well-chosen constraints dissolve the twin problems of memory safety and thread safety — I recall a statistic showing that these two categories account for a solid half of all bugs in the Linux kernel. In other words, learn Rust and you can lie back and wipe out 50% of the nastiest bugs, the ones that make even kernel developers turn pale at the mere mention.

But to me, the real delight of Rust is that it injects into so low-level a language so high-level a type system — one that has absorbed a great deal of the essence of Haskell. If you’ve spent time with Haskell, F#, or Scala, you can probably imagine my excitement. The world we live in rarely lets us have both — Haskell excels at type systems but robs the programmer of control over how data is laid out in memory; C excels at precise control over data in memory but has no decent type system to speak of. Rust manages to have almost both. My own Haskell journey eventually went from beginner to quitter, but like Zhang Wuji on Ice Fire Island, dimly puzzling over the martial arts manual, those concepts — monad, monoid, semigroup, sum type, product type — were seared into my mind, sealed away and waiting for a pretext to see the light of day again. That pretext was Rust.

This article borrows Rust to talk about my half-formed understanding of type systems. It isn’t really about Rust; anyone with experience in another programming language should be able to follow along.

primitive type

Primitive types. Virtually every programming language has them — integer, string, bool, array, list/vector, and so on. They are like the elements of the periodic table: few in number, yet together they compose our whole colorful world.

There is nothing much to say about primitive types, but before we dive into what follows, we need to ask ourselves one question: what is a type?

For u8, it is an integer between [0, 255] — a set, expressible as { x | x ∈ [0, 255]}. For String, it is the set of all strings, {x | x ∈ ["", "a", ..., "War and Peace", ...]}.

So the mathematical meaning of a type is a set.

product type

Product types exist in nearly every programming language we know — in some they are called records (Delphi, Erlang), in others structs (Elixir, Rust, Go) or objects (JavaScript). In day-to-day software development, the data type we can’t live without is the product type; just as molecules combine atoms of different elements, product types vastly enrich the space of possible types and thus serve us well in DDD (Domain-Driven Design).

Let’s look at the mathematical meaning of the product type. A product type, as the name suggests, is the product of different types. But what exactly is the product of types? Suppose the domain of x is the set int and the domain of y is the set string; then x * y expands to (…, -2, -1, 0, 1, 2, …) * (“”, “a”, “ab”, “hello world”, …). That is, for any value in int, there is any value in string paired with it. Look familiar? This is the Cartesian product. As shown:

In Rust, for example, we can model a user like this:

struct User {
  username: String,
  nickname: String,
  email: String,
  email_verified: bool,
}

The set of possible values of the User type is precisely the Cartesian product of all the types inside it.

sum type

The Cartesian product certainly helps us build all kinds of composite types, but it cannot describe a scenario like this: we want to add a payment type to User, and it can be one of credit card, cash, WeChat, or ABT. Naturally, we could describe it like this:

enum Payment {
  Creditcard,
  Cash,
  Wechat,
  Abt,
}

But such a type is incomplete — if the user picks a credit card, we need the card number, expiration date, cardholder, and so on; if they pick ABT, we need the wallet address and its public key. What to do? We need a type along these lines:

Creditcard(CreditcardType) | Cash(f64) | ... | Abt(WalletType)

In set theory this is called a disjoint union, written A + B. As shown:

In data types, the disjoint union is often called a tagged union (C++) or a sum type (Haskell, Rust). Contrary to the product type, most programming languages have no sum type. Let’s see how Rust uses a sum type to solve the problem above:

struct CreditcardInfo {
  number: String,
  expiration: chrono::NaiveDate,
  holder: String,
}

struct WalletType {
  address: String,
  pk: [u8; 32]
}

enum CreditcardType {
  Creditcard(CreditcardInfo),
  Cash(f64),
  Wechat(AccountInfo),
  Abt(WalletType)
}

The beauty of the sum type is that it fixes the latent imprecision of primitive and composite types in a type system. Take a function like this:

fn div(x: f64, y: f64) -> f64 { x / y }

From the type signature, it looks fine, but at the implementation level we quickly discover that x / y carries a constraint: y must not be 0. Either we design a new data type, non_zero_f64, that excludes zero (very difficult in most languages), making the function’s type signature complete from the input side; or we make the return value a special type that may be an f64 or may be empty.

Since most languages don’t support sum types, there are only two ways to handle this situation:

• The function’s return value may be an f64, or it may be null. If a language doesn’t support exceptions, you have to check the input and return null when it’s 0.
• The function’s return value is still an f64, but dividing by zero throws an exception. For languages that support exceptions, besides the previous approach, we can also throw.

The first approach erodes type completeness, because the type signature is no longer authoritative — callers can’t be sure they’ll get an f64 back, so they too must add condition checks, passing this leakage of type information down layer after layer. The second approach also damages type completeness, because callers must know about and choose whether to handle those “surprises.” Since the surprise isn’t part of the return type, extra logic is unavoidable.

The problem with div above is merely the tip of the iceberg. Apart from learning to write code or writing PoCs, we never get to write code for the happy ending alone — after all, we don’t live in a fairy tale. Errors and surprises accompany virtually every interaction — with IO, with libraries (other people’s code), with system calls. In his famous Railway Oriented Programming, Scott Wlaschin picks out one such situation after another in search of a remedy, and the sum type is the best choice of all.

In Rust, we have Option, which is rather like the Maybe Monad:

enum Option<T> {
  Some(T),
  None
}

For the function above, we can use Option<f64> to complete its type signature:

fn div(x: f64, y: f64) -> Option<f64>;

When y is zero, return None; otherwise return Some(x / y). On the surface it looks no different from the first approach above, but a formally complete type makes many things possible. This function can be piped and composed, and callers needn’t worry about type leakage — all the information is already in the type signature; the compiler can perform more appropriate and stricter checks, and can optimize accordingly — and more importantly, around this type we can abstract away the pile of if/else and try/catch result-checking that would otherwise keep reappearing in user code, turning it into a set of behaviors on the Option type, which makes user code clean.

By the same reasoning, in Rust, exceptions are abandoned and replaced by Result, also a sum type:

enum Result<T, E> {
  Ok(T),
  Err(E),
}

Interactions with IO and with other people’s code can all be handled through Result. Around Result there is likewise a standard set of behaviors and macros for handling its contents.

There is endless debate over whether a programming language needs exceptions and whether exceptions are medicine or poison: Java/Python are the establishment, C++/Haskell are the fence-sitters, Rust/Go are the opposition, and Erlang/Elixir are the anarchists. I won’t go into it here. You ask whom I side with? I love the classic line Yoda says to Luke: do or do not, there’s no try. That line also encapsulates the philosophy of Erlang: let it crash.

generics type

Generics — the type everyone loves and hates. It simplifies code and raises the level of abstraction, but the price the programmer pays is a steeply rising learning curve. Setting aside whether generics are good or bad, let’s first look at their mathematical meaning. Take the Option type again:

enum Option<T> {
  Some(T),
  None
}

T stands for any type, and Option<T> is the result of mapping T into this enum. So from another angle, we can regard a generic as a special kind of function acting on types: it takes one or more types and returns a new type. We know that when the compiler deals with concrete data, it expands the generic — for instance, Option<u8> expands to:

enum Option {
  Some(u8),
  None
}

This expansion can extend indefinitely, yet the expansions don’t intersect with one another, just like a sum type:

enum Options {
  U8(enum { Some(u8), None }),
  U16(enum { Some(u16), None }),
  String(enum { Some(String), None }),
  ...
  VectorU8(enum { Some(Vec<u8>), None }),
  VectorU16(enum { Some(Vec<u16>), None }),
  ...
}

This result is quite interesting. We know the mathematical meaning of a sum type is the sum of types; if we denote a primitive type as X, then here we have n X’s. Vector<T> can be a kind of Option<T>, so Vector<T> can expand into nX; there are also n types like Vector<T>, so the Options expanded thus far can be written as nX + n * nX. By the same token, HashMap<T, E> is n * nX, and n options expanded from types like HashMap<T, E> give n * n * nX, and so on, from which we can conclude that generics represent on the order of

n + n^2 + n^3 + n^4 + ....

data types. This is a geometric series, whose sum is n(1 - n^n) / (1 - n).

enum Result<T, E> {
  Ok(T),
  Err(E),
}