Dependently Typed Code

TLDR: Declarative, dependently-typed programming can result in software that is more stable, less buggy, easier to maintain, and sometimes more efficient. Utopia bridges the gap between mathematics and computer programming, resulting in more code re-use and stronger degrees of abstraction and encapsulation.

Prerequisites: None, though experience with math and coding will definitely help

One of the first things that any computer programmer learns about are types. While most programming languages support very basic types, it turns out that if you go all the way down the rabbit hole then you end up with software that can’t crash, and is in general much less buggy, and oftentimes faster.

Let’s explore types together, getting into high-power types as fast as it makes sense to do for an audience of intelligent laypeople, and then we’ll discuss why the software industry hasn’t caught on to the power of types and how they might be used in Utopia.

Simple Types

All modern computers are symbol processing machines where all the symbols ultimately ground-out as bits encoded by transistors — simple electric devices that can be in one of two states, like a little switch controlled by electricity. A bit, then, is simply a type of thing that can be one of two ways. It is common to call the values that a bit can have “0” and “1.” Importantly these are not numbers per-se, but simply two arbitrary names for the values a bit could possibly have.

0 : Bit
1 : Bit

I’m going to use that colon notation to describe what type something is. By explicitly marking our values with types we can resolve the ambiguity of whether 0 and 1 are supposed to be bits or whether they’re normal numbers.

To create more complex symbols I need to combine bits together. The simplest method of combining values is to pair them up — to simply have one after the other. A pair of bits can be written like this:

0 , 0 : Bit ∧ Bit

And we might read that as “zero with zero is an instance of a bit and a bit” or just “zero zero is a pair of bits.” (The word “pair,” unfortunately is ambiguous about whether it’s on the level of types or the level of values. A “pair of bits” makes sense, as does “zero paired with zero,” despite these being pretty different. I’m using the comma symbol for value-level pairing and the ∧ symbol for the type-level.)

In computer science a pair of bits is sometimes called a “crumb,” so if we wanted to be fancy we could say “zero zero is a crumb.” There are similar definitions involving pairs, the most famous of which is the “byte.”

Crumb = Bit ∧ Bit
Nibble = Crumb ∧ Crumb
Byte = Nibble ∧ Nibble

0 , 1 , 0 , 0 , 0 , 0 , 0 , 1 : Byte

A byte is exactly eight bits, but we can also talk a list of bits that can be any (natural) number of bits, including zero bits. I’ll use the symbol “Ø” to indicate an empty list, and I’ll use the “◃” symbol to delimit longer lists. The lists in my notation will always end with Ø, for reasons that I’ll get into a little bit later.

Ø : Bit List
0 ◃ Ø : Bit List
1 ◃ Ø : Bit List
0 ◃ 1 ◃ 0 ◃ 0 ◃ 0 ◃ 0 ◃ 0 ◃ 1 ◃ Ø : Bit List

Lists are kinda interesting because while bits and bytes each take a fixed amount of transistors to represent, a list of bits can be arbitrarily long, and thus potentially too big to fit on our computers. We typically ignore this sort of thing when thinking about things abstractly like we’ve been doing. Modern machines can hold a lot of bits, and the logic can still be solid even if we happen to ask too much of our hardware.

Now, we can have lists of other things besides bits, of course. For instance, we can represent text-characters as a collection of bits using a code. The first major character code in computing was ASCII, which uses seven bits to represent each character. In ASCII the letter “A” is encoded as 1000001, “B” is 1000010, and so on.

ASCII-Char = Bit ∧ Bit ∧ Bit ∧ Bit ∧ Bit ∧ Bit ∧ Bit
...
"H" = 1 , 0 , 0 , 1 , 0 , 0 , 0
"I" = 1 , 0 , 0 , 1 , 0 , 0 , 1
...
"a" = 1 , 1 , 0 , 0 , 0 , 0 , 1
"b" = 1 , 1 , 0 , 0 , 0 , 1 , 0
"c" = 1 , 1 , 0 , 0 , 0 , 1 , 1
...

Ø : ASCII-Char List
"H" ◃ "i" ◃ Ø : ASCII-Char List
"H" ◃ "e" ◃ "l" ◃ "l" ◃ "o" ◃ Ø : ASCII-Char List

Notice that Ø can indicate either an empty list of bits or an empty list of characters. Again, specifying types allows for using familiar symbols unambiguously. Similarly, we can overload quote marks in this syntax to indicate either a single character or a list of characters. This would be similarly ambiguous if we didn’t have a notion of types.

"Hi" : ASCII-Char List
"Hello" : ASCII-Char List
"How are you?" : ASCII-Char List

Contextualized Types

So far we’ve kept values and types distinct. Let’s break that barrier and clarify that types are also a kind of value — we can give a type to our types! Let’s use “Type₀” to refer to the type of most types. Some examples should help…

Bit : Type₀
Byte : Type₀
Bit ∧ ASCII-Char : Type₀
Bit List : Type₀
ASCII-Char List : Type₀

This might be a little brain-breaking, but it’s actually pretty straightforward. When I say “Bits, bytes, pairs of bits and ASCII-characters, bit bists, and ASCII-character lists are all examples of types” I’m really just saying the same thing as the above block of code.

Why the subscript-0? Because Type₀ is itself a value, but in order to stay sane we can’t have a type whose type is itself. Thus we say Type₀ : Type₁, and Type₁ : Type₂, and so on. This isn’t important for our purposes and can be ignored; I simply mention it to explain why Type₀ has the subscript, for those inclined to dive deeper.

We’ve seen two examples of lists so far: lists of bits and lists of characters. But lists can be over anything. To express this, we can say that for all types there is a list of that type.

∀ X : Type₀.
  X List : Type₀

Let’s unpack this syntax. The “∀” can be read as “for all” or “for any,” and introduces an abstract value that we’re allowed to give an arbitrary name. It’s common for these arbitrary names to be a single letter, and in this case we use the letter “X.” Note that uppercase X is different from lowercase x; it’s common to use uppercase letters for types and lowercase letters for non-types.

The abstract value introduced by ∀ is restricted to a specific type, which in our case is Type₀. The period at the end of the first line, and the indentation of the following line indicates that our abstract value is only able to be used in that immediate context. If we tried to talk about X somewhere else we wouldn’t know what was being referenced.

Let’s practice with this syntax using a few more examples:

∀ x : Bit.
  x , 0 : Crumb

∀ X : Type₀. ∀ Y : Type₀.
  X ∧ Y : Type₀

∀ X : Type₀.
  Ø : X List

Abstraction is extremely powerful. It’s so powerful, in fact, that it’s only fully implemented in a handful of programming languages called dependently typed languages.

Functions

All programming languages use some abstraction, it’s just usually not powerful abstraction that talks about types.

For any number there is a number that’s twice as big. We can write this fact in our notation by abstracting over a natural number (denoted ℕ) and defining twice that number using addition.

∀ n : ℕ.
  n twice = n + n

And because we’re being abstract, what we’ve done here is essentially to define a function. Functions are relationships between a type of inputs and a type of outputs such that for any possible input there is a corresponding output. All abstract definitions correspond to functions, where the inputs are whatever abstract values are in the context, and the output is the defined value.

6 = 3 twice

When we think about twice as a function, and not simply a definition in an abstract context, we can give it a type that reveals the type of inputs and outputs. More generally (and abstractly), we can see that there is a type of functions between any two types, just like there is a type of pairs between any two types.

twice : ℕ → ℕ

∀ A : Type₀. ∀ B : Type₀.
  A → B : Type₀

Weirdly, this means that Ø is also a function, since it’s defined in a context with an abstract type. However, thanks to explicit types and other hints it’s so easy to guess at what the input to Ø needs to be for a given context that we simply elide it. Elided inputs like this are said to be inferred. Inference is extremely useful in not having clutter everywhere, and is one of the many things that types can help provide.

The ◃ symbol is a function, too. And unlike Ø, it has two inputs that (usually) can’t be inferred. We call ◃ an “operator” because it takes an inputs on its left and on its right, just like the + operator for numbers.

∀ X : Type₀. ∀ x : X. ∀ xs : X List.
  x ◃ xs : X List

∀ X : Type₀.
  ◃ : X ∧ X List → X List

Both of those expressions mean (approximately) the same thing. They say that if you provide a value in some type and a list of values in the same type, then you can prepend the loose value onto the list to get a new list of values in that type. That’s why we need to put Ø at the end of a list (unless we use special syntax like for lists of characters) in order to make the types work out.

0 ◃ 1 ◃ 0 ◃ Ø = 0 ◃ (1 ◃ (0 ◃ (Ø : Bit List)))

Equality Types

We’ve been using types more often than you might realize. At several points I’ve written an equality between values like so:

"H" ◃ "i" ◃ Ø = "Hi"

In dependent typed programming, the above equality is a type!

Here’s how equalities work in abstract:

∀ X : Type₀. ∀ Y : Type₀. ∀ x : X. ∀ y : Y.
  x = y : Type₀

∀ X : Type₀. ∀ x : X.
  x reflected : x = x

In English: for any two values we can talk about the type of equality between those values (regardless of whether they’re equal), and for any one value we can construct an instance of the equality type between it and itself. I call the trivial constructor for equality “reflected” partly for historical reasons (it’s often called “refl”), and because x is on both the left and right side of the equals operator, as though it were looking at itself in a mirror.

Unlike all the types we’ve talked about before, equality types are the first to bring in the big guns. Many programming languages allow for types to depend on types (e.g. List) or for non-types to depend on non-types (e.g. twice), but very few allow for types to depend on non-types.

By letting types depend on non-type values, we connect the bridge between mathematical proof and computer programming. All (fully) dependently typed programming languages are theorem proving tools, and all theorem provers are dependently typed programming languages. An equality type is a proposition. An inhabitant of that type (i.e. a value whose type is the equality) is a proof of that proposition.

The rabbit hole keeps on going. Once we see that types can be propositions and inhabitants can be proofs, we can see that functions are implications, and function application is modus ponens. The full extent of this connection is well beyond the scope of this essay, but for the curious I think the book PROGRAM = PROOF is probably a good choice.

I want to highlight one powerful aspect of equality types, however, which is that they (along with abstraction and inference) can serve as a theoretical foundation for functions which return different outputs depending on their input.

∀ x : Bit.
  ∀ _ : x = 0.
    x toggled = 1
  ∀ _ : x = 1.
    x toggled = 0

toggled : Bit → Bit

The syntax above is hiding some magic (and in a real programming language we’d need things to be a little cleaner, such as using a “case” keyword). Essentially, we can think of “∀ _ : x = 0.” as equivalent to something like “if x is 0 then…” If we plug in “1 toggled” for the computer to evaluate, it will notice that it should try to prove 1 = 1 or 0 = 1. It can easily prove 1 = 1 by plugging in 1 reflected, which will mean that 1 toggled evaluates to 0.

Again, a real programming language would do things more efficiently than proof search there, and a real mathematical language would want to clarify between ∀ symbols that reduce to functions vs those that are implicit. But the point is that we can see that within the body of what is essentially an if-statement, we can explicitly reference and lean on the fact that our variable has a specific value.

No Runtime Errors

Why does any of this matter? Sure it’s cool for mathematicians who want to check the proofs of their theorems on a computer rather than relying entirely on their minds. But we started off this essay with the bold claim that software written using dependent typing can’t crash. What magic lets us be sure of that?

The trick is that if you set up your code like we’ve been doing, the computer can check that every possible pathway through the program is well-defined. This sort of checking is often very fast (but is unfortunately sometimes slow, or occasionally unending) and is done before anyone runs the program.

For example, let’s say that we’re defining division. In most programming languages if you try to divide by zero the software will crash. Programmers using these languages need to track using their meat-brains that any time two numbers are divided the denominator isn’t zero. In practice they often forget, which produces bugs and can be terrible for users.

Dependently typed programming, on the other hand, can demand a proof that the denominator isn’t zero wherever division occurs. With clever tricks like inference this proof can often be provided by the machine, simply saving the programmer from bad assumptions and otherwise staying out of the way.

At least, this is the ideal. In fact, dependent typed languages are so new and under-used that they often suck to use, and require things like equality proofs to be piped around by hand.

The bad (but increasingly much better) state of the tools for dependent-typed coding are a big part of what pushes newcomers away. Programmers often feel like they shouldn’t have to convince the machine of some property that they know is true, and don’t like being held up by errors about needing to prove things. (And then, when their hubris strikes them and causes crashes and bugs, they shrug and claim that coding is naturally hard and there’s no way around that.)

It’s worth noting that because proofs are checked before the code ever runs, equalities very rarely need to be handled when the program is actually running, and can be dropped. This means that at no point should a good language with dependent types force the user to provide proofs — it should simply warn whenever something isn’t provably safe.

Think of it like a light that comes on when you drive over the speed limit. It doesn’t prevent you from doing dangerous things if you think you’re not going to crash — it just lets you know that you’re being reckless and that safer options exist.

Types > Tests

Speaking of safety, one of the hot things in the world of programming is emphasis on Testing. I say uppercase-T because Testing isn’t just running your program and checking to make sure it works, but rather employing a suite of tools that automatically perform intricate tests on every piece of code. Why the obsession with Tests (sometimes to the extreme of Test Driven Development)? Because Tests are a good way to protect from bugs and ensure that the program you write has the properties that were desired.

Wait… properties that are desired… That sounds like a type!

Let’s consider the task of sorting a list of things:

sorted : X List → X List

A novice might assume that the only relevant property to the sorting function is whether the resulting list is in order.

isInOrder : X List → Bit

This mistake can happen either in traditional programming or in typed programming — nothing can save you from not knowing what you want. But an experienced coder will ask “is there a function that returns a list that’s in order that isn’t what I want?” And from this they might realize that the empty list is always in order, so a function that always returns the empty list will satisfy both the types and the tests.

The correct solution also needs to return a list with the same elements as the original — essentially being a permutation of the input.

hasSameElementsAs : X List ∧ X List → Bit

The test, written in a common language will look something like:

function testSorted() {
  for _ in [0..100] {
    i = generateListOfX()
    o = i.sorted()
    assert(o.isInOrder())
    assert(i.hasSameElementsAs(o))
  }
}

The type-based approach will instead put properties of the function into the same context (or alternatively attach the properties to the output of the function).

∀ X : Type₀. ∀ xs : X List.
  xs sorted : X List
  xs sorted isInOrder = 1
  xs sorted hasSameElementsAs xs = 1

Not only is the type-based approach cleaner and less likely to itself be buggy (especially with some syntax sugar/colors and editor tooling), but it’s able to check correctness for every possible input! The sorting function might, for some strange reason, have a bug when the first element of the list is equal to the last element; when verifying code integrity through testing one must hope that the generator of X Lists reliably hits that case.

Autogenerated Code

But the benefits of powerful types don’t stop there. Thanks to strong machine-checked properties and structures, it’s possible for many functions to be automatically written by the computer. On the low end of this are functions that have an “obvious” implementation like map:

∀ X : Type₀. ∀ Y : Type₀. ∀ xs : X List. ∀ f : X → Y.
  xs map f : Y List

Requiring a bit more effort are one-off functions that are uniquely pinned down by their types/properties. For instance, instead of writing toggled in the way we did earlier, we could simply demand that it satisfy a property and autogenerate it.

∀ x : Bit.
  x toggled : Bit
  x toggled ≠ x

On the extreme end would be having an AI pair-programmer pay attention to everything from the names of functions to the surrounding code in the overall program, and suggest code that matches the specified types and properties, even if it can’t guarantee that it’s unique or ultimately correct.

As AI develops I think software development will move away from human programmers doing most of the algorithmic heavy-lifting, instead having their expertise be in communicating desires to the machine and checking the results.

Speed and Efficiency

The most complained about, highest-friction aspect of dependent typed programming, in my experience, is that engineers who are used to the old way find it hard to think about. They’re used to describing programs as a series of changes to be made to concrete data, not juggling proofs about abstract entities. Particularly unnerving to certain high-power programmers is not being able to model how languages that look like the notation we’ve been using ground out in actual instructions for the computer.

For these people, I suggest reading the gory (but cool) details for how a language like Haskell turns abstract declarations into low-level instructions. But for most programmers, I think it’s more useful to generally trust that sensible things are happening under the hood to produce efficient code from high-level symbols and words. This is, after all, a similar situation to how any high-level programming language works, whether it’s Javascript or C#.

There are a few gotchas, however, which give rise to the second most likely thing an anti-dependent-type programmer is likely to complain about: “randomly” bad performance, especially around memory usage and infinite loops. When I screw up writing Javascript my browser freezes and I have to close that tab; when I screw up using Haskell my computer locks up so bad that I often have to power it down the hard way. It was this issue that kept me away from these kinds of languages for years.

While it goes too far into the weeds to be worth getting into here, I’ll simply say that I believe the answer is more static analysis and types. I wouldn’t fault you at this point from thinking that I’m in an abusive relationship with my type-checker, but hear me out.

When done well, heavily typed code can run as fast or faster than high-performance code in other languages, and it can even work without gobbling up memory. The task is then to do it well, hopefully without breaking our brains trying to understand what’s going on.

Thankfully, things like state monads and substructural types can capture the relevant properties and bring them front-and-center. We can even use models of the machines we’re compiling on to develop low-level code and then prove that it’s a version of the high-level function that we define in the natural, easy-to-read way. Imagine having a machine-checked type/property that guarantees that your function has the amortized complexity that you think it does.

Utopian Dependently Typed Code

In my vision of Utopia, the standard way that humans program computers is by defining and proving things in dependently typed, interactive coding environments. This feels much closer to mathematics to most people, and there’s no hard line in Utopia between programmers and mathematicians.

While different projects have different needs and build things in different ways, the heavy emphasis on abstraction means that much more code in Utopia can be re-used between projects. This, combined with crisp sandboxing, smaller, more modular programs, and other good features, means that it’s faster to build new applications by remixing and leveraging existing tools than reinventing everything from scratch.

Most people don’t bother to model the details of how code turns into instructions. Compilers and even artificial intelligences work to build out efficient machine-code that matches the properties desired by the developers. Real-time tools like namespace searching, inference, type/value inspection, and code generation make writing software a delightful experience.

Photo by Joshua Woroniecki