The problem is that nobody understands type theory

I’m currently taking over a data/ETL project for maintenance that has been plagued by production issues and unexpected data inconsistencies and we’re just firefighting and talking about NULL values in data all day and I’m growing a bit tired of it. We really need people otherwise patching this stuff up will take forever but I guess this blog is not the right place to complain.

And if any coworkers are reading this it’s fine you did a good job it’s a complex environment and I appreciate the effort. This is like every software project ever. Everywhere it’s the same bugs over and over again.

Maybe I’m just growing old and bitter and it’s time to open a little Italian bistro to sell focaccia and stuff and get out of IT.

But you know. Learn type theory.

Actually let me mansplain it for you.

Functions, mkay. Functions have a domain and a codomain. That is, there is a set of inputs that the function accepts, that’s the domain, and for each input there is an output in the codomain.

The function that rounds down? It takes real numbers (domain) and returns integers (codomain).

Or how about this one, it takes a currency string like “EUR” and gives you the symbol like ”€”. Do you agree the type should be:

const currencySymbol = (code: string): string => { ... }

Because you put a string in and you get a string out, right?

WRONG.

This won’t work. What happens when you call currencySymbol("banana")? There is no symbol for “banana”. But your domain allows all strings so it’s a valid program.

That leaves you with two options.

Not a Solution 0 - Designated error string

You could return "INVALID CODE" when the input is not a valid currency code.

But if you do that, I will literally bite your head off ok? (Unless you are a C programmer, you do whatever you want.)

Solution 1 - Extend the codomain

Instead, we can extend the codomain to include some null or error-like value, and we return this value when the input is invalid.

const currencySymbol = (code: string): string | null => {
  const symbols: Record<string, string> = {
    EUR: "€",
    USD: "$",
    GBP: "£",
  };
  return symbols[code] ?? null;
}

Now our function is defined for the entire domain of all strings. ^[1]

Solution 2 - Shrink the domain

The other approach: shrink the domain to only include valid inputs.

type CurrencyCode = "EUR" | "USD" | "GBP";

const currencySymbol = (code: CurrencyCode): string => {
  const symbols: Record<CurrencyCode, string> = {
    EUR: "€",
    USD: "$",
    GBP: "£",
  };
  return symbols[code];
}

Notice how the second approach doesn’t need any runtime checks because the type checker handles invalid inputs at compile time.

And the downstream code doesn’t need to handle null values either. Guess which solution I prefer!

Solution 2.5 - Assertions

Say you have a function that computes the n-th prime number, and your initial idea is this type:

const nthPrime = (n: number): number => { ... }

This won’t work for nthPrime(0) or nthPrime(1.5), because there is no zeroth prime number. But, shrinking the domain isn’t really possible here:

type PositiveInteger = 1 | 2 | 3 | ...; // you can't really spell this out
const nthPrime = (n: PositiveInteger): number => { ... }

I mean it’s possible conceptually but typescript isn’t powerful enough to give you a way to write down a definition for PositiveInteger. So what we usually do in programming is to add a precondition inside the function. ^[2]

const nthPrime = (n: number): number => {
  assert(n >= 1 && Number.isInteger(n), "n must be a positive integer");
  // compute the n-th prime here
  ...
}

And we pretend that assertions at the start of a function are like filters on the domain. Even though they kind of aren’t because the assertion is a runtime check rather than a type-level guarantee.

Now you might argue that Solution 2.5 is actually more of a Solution 1.5 because isn’t throwing an error the same thing as returning a null, to which I say: shut up I am trying to make a point.

The point

I’m kidding, that was already the point. I just want every programmer to know about this, even vibe coders who have never read a single line of code.

Say you have a main.py file that is 400 lines long and it’s a single function.

First question: why? But also what you can do is you take any say 20 consecutive lines from the middle of it and pretend to wrap a function definition around it. And then you think about what assertions you would need at the start of that function to ensure the inputs are valid.

If you do this for all possible slices of your program (largest first; there are 80200), then all possible input conditions for every part of your program would be covered by assertions, at the earliest possible point.

I know it’s not so easy

Restricting your domain, or even spelling out your domain, is hard for real world programs. A database connection can time out or fail for reasons beyond your control, and who encodes every possible failure mode of a database in types? Nobody, you can’t.

You can’t, and if you can’t even write down your domain, you can hardly write good assertions either.

And like even if you assert that the database connection is valid, 3 nanoseconds later when you actually do the query, it might fail anyway.

I get all that.

But before we get into the hard and messy parts, please patch y’alls codebases with the easy stuff first, it’s not like you’re doing that either. I’ve seen your codebases, all of them. None of you have patched the easy stuff. Especially not the java devs.

Once the AI writes all new software in Lean maybe then we can stop worrying about domain issues but for now that’s just what we’re stuck with.

---

^[1] This function is incorrect for really subtle reasons. Do you see why?

^[2] Another common pattern in typescript is “branded types”, used by many popular validation libraries like zod and io-ts. It boils down to the same thing though — runtime checks that enforce constraints that the type system can’t.