A few years ago, Amos (AKA fasterthanlime) wrote a really great article entitled Aiming for correctness with types. It's a lengthy post, but at heart it was about how, by more faithfully modelling our world at the type level, we can avoid a great number of runtime bugs & errors (a topic near to my heart). He took as a running example the problem of building an authenticating proxy for a simple web service. In particular, he dug in to modelling HTTP headers, calling out the Rust hyper crate as a particularly expressive model; one in which "you can only build something that's meaningful".

This is also known as "correctness by construction": if you can build an instance of your type, if the constuctor returns successfully, then you know that that instance satisfies certain properties (I loathe the "create-then-init" idiom that was at one point, and is perhaps still, common among Java programmers). This is interesting when it comes to HTTP header names because, while they are commonly modelled (TODO: need refs) as strings, in fact the salient RFCs restrict them to a fairly small subset of ASCII. Furthermore, the RFCs state that they are case-insensitive: "Host", "host", and "HoSt" should all be considered as the same header.

hyper, quite sensibly, provides for creating instances of their HeaderName from strings or buffers of byte. An arbitrary Rust string, which is a UTF-8 encoding, cannot, by virtue of its type, be known to be a valid header name (to say nothing of an arbitrary array of byte). The constuctors therefor validate their input, either panicing or returning an error result if the input does not meet their preconditions. In this way, type HeaderName is indeed correct by construction: if you successfully construct an instance, you are guaranteed that it's valid. Well & good.

And yet. If, at compile time, I wish to construct a HeaderName from the string "Host", I know that that is legitimate– why do I need to accept a possible panic or unwrap an error code? Yes, hyper offers a pre-defined header for "Host", since it's standard, but replace that with "X-My-Custom-Thing". What if I could encode the preconditions into the type, and make the attempt to construct an invalid header name like "名" into a compile-time error?

Enter depdendent types. I introduced them in my posts on the lambda cube, albeit in a fairly abstract, formal way. In this post, I return to them, hopefully in a more practical, down-to-earth manner, and show how they can help us get closer to correctness with types.

In the next section, I'll discuss dependent types with a lot less type theory. Then I'll look at how to "reason" at the type level. Next, we'll look at modelling HTTP header names in Idris, a functional dependently-typed language I'm learning. Next we'll look at how I used dependent types in some live Idris code, and finally wrap-up.

Dependent types are not well-known in the programming community because languages in common use in industry don't offer them. I'll describe depdendent types in terms of what we already know. Consider the C++ function template:

template <typename T>
T f(T x);

f isn't a term that we can use in our program, not directly. We can only invoke f once we supply a template parameter, say int. f<int>() is now a function that we can invoke, take its address and so forth. We might regard the function template f as a function from types to terms, and in that way we can say that f<int>() is a "term that depends on a type".

Now consider the Rust Vec struct:

struct Vec<T>

Here again, T is a generic type parameter to Vec; I can't construct a Vec, only a Vec<usize> or a Vec<f64>, or whatever. We might regard the generic struct Vec as a function from type to type, and in that way we can say that Vec<usize> is a "type that depends on a type" (I have it a type, usize, and received a type in return Vec<usize>).

If we consider familiar expressions in our programs as "terms that depend on other terms", that leaves one final combination: types that depend on terms. These are dependent types. The simplest form is a function that takes values of some type and returns a type. For instance, we might write:

type f(bool x) {
  if (x) {
    return int;
  } else {
    return string;
  }
}

This isn't real C++, of course, since one can't program with "first-class types" in any industrial language of which I'm aware. But this is exactly the sort of thing which one can do in dependently-typed languages.

If we can compute at the type level, we can now do things like:

f(x) g(bool x) {
    if (x) {
        return 11;
    } else {
        return "Hello, world!";
    }
}

Here, the type-checker can "compute" the return value of g() from x, and "see" that this implementation type-checks.

In his talk Dependent Types for Practical Use, Andre Videla had a nice summary of our situation:

Another way to look at dependent types is as "indexed type families". In the example above, f() is indexed by the booleans; each specific boolean maps to a concrete type. We would say "int is the type at true, and string is the type at false." The classic example here is length-indexed lists. In Coq, such a thing is called a "vector", and is defined like so:

Inductive Vector A : nat -> Type := (* ... *)

We say that Vector is parameterized by the generic type parameter A (i.e. you can have a Vector of int, or a Vector of string, or whatever) and indexed by \(\mathbb{N}\). The distinction between parameterization & indexing is that parameters remain fixed throughout the types definition whereas indicies can change (I don't want to dive into Coq syntax, yet, but the definition of a Vector of length n involves a Vector of length n-1). In Coq that distinction is reflected in whether the "argument" appears on the left or the right of the colon, but that's not true of other dependently-typed languages.

For the sake of completeness, I wrote about dependent types in a post on the type system λ-P. There, they were described as "Π-types" that generalized the arrow types with which we're already familiar in terms of representing functions. A function from bool to int would be said to have type \(bool\rightarrow int\). We generalize this by allowing the value on the left-hand side of the arrow to affect the value on the right (as in f(), above).

In that post, I used the example of \(\mathbb{V}_n\), the set of (double-precision) lists of length \(n\). In the λ calculus, a term reprsenting this indexed type family would be \(\lambda n.\mathbb{V}_n\): given an \(n\in \mathbb{N}\), you get back the type \(\mathbb{V}_n\). This is just like f(x), above: given a \(b\in bool\), you get back the type f(x).

We might imagin a function that, given \(n\in \mathbb{N}\) returns the zero vector for the type \(\mathbb{V}_n\), call it zero(n). Then type of zero(n) would be \(\Pi n:\mathbb{N}.\mathbb{V}_n\). This is analagous to g(), above: g() would have, in λ-P, type \(\Pi b:bool.f(b)\).

The relationship between \(\mathbb{V}_n\) and zero(n) is shown here:

where ∗ is the type of all types, and \(\square\) represents the universe above \(\ast\).

Dependent types allow us to write more expressive types. Examples include:

• length-indexed lists that allow us to write a SAXPY operation where passing vectors of different lists is a compile-time error
• writing a "printf" clone where the type & number of subsequent arguments is computed at compile-time based on the format string, turning a failure to supply the correct number & type of replacement parameters into a compile-time error (my first segv was exactly such an error in using printf)
• writing type-safe heterogeneous lists
• writing functions that take as an argument a value describing a table schema, whose return type is calculated from that schema

However, one of their most significant uses comes from something to which I alluded in that earlier post: the Curry-Howard correspondence. Very briefly, this refers to the fact that to every type system their corresponds a logic in which propositions in the latter correspond to types in the former. Inhabitants of a given type are proof terms for their corresponding proposition. My impression is that many of the logics are not terribly interesting, but once you've got dependent types, you can pretty-much encode all of first-order predicate logic which is very interesting indeed.

Before I start, let me introduce Idris, the dependently-typed functional language I'll be using throughout this post. There are few ways in which to define types in Idris, but the workhorse is the "data" declaration:

data Foo : arguments... -> Type where
  ctor1 : arguments -> Foo... 
  ctor2 : arguments -> Foo...
  ...

Here, Foo is the name of our type (or, generally, our type family). Everything after the colon is the "type constructor"; this is just the parameters & indicies of the type family. ctor1, ctor2 and so on are referred to as "data constructors"; these tell us how to construct instances inhabiting assorted types in our family.

A trivial example:

data Bool' : Type where
  False' : Bool'
  True' : Bool'

I've named my type Bool' to avoid conflicting with Bool, it is a simple type (i.e. no parameters, no indicies) and it has two data constuctors, again neither of which takes any parameters. We could re-define the natural numbers like so:

data Nat' : Type where
  zed : Nat'
  succ' : Nat' -> Nat'

As an aside, languages like Coq, Agda, Idris & so on all tend to define the natural numbers in this way (this is the Peano representation). I believe that this is due to this representation's convenience when it comes to recursion and it's Curry-Howard correspondent, induction. Regardless, what we have here is a simple type named Nat'. It has two data constuctors. The first takes no parameters, and in that way may be regarded as a constant. We are declaring that zed is a Nat'. The other way to get ahold of a Nat' is to apply succ to one you already have. In this way, the natural numbers 0, 1, 2 and so on are represented by zed, succ zed, succ (succ zed), and so forth.

Now consider this type family, indexed by Nat':

data Even : Nat' -> Type where
  ZedIsEven : Nat' zed
  Plus2IsEven : Even n -> Even (succ (succ n))

Let's think about this: this is a type family, indexed by \(\mathbb{N}\). In other words, to every \(n\in \mathbb{N}\), there corresponds a type Even n. How can we construct elements of these types? Well, we have two data constuctors. The first, ZedIsEven is a constant: ZedIsEven and it inhabits the type Even zed.

Next, if have an inhabitant \(x\) of the type Even n laying around, then Plus2IsEven \(x\) is an inhabitant of Even (succ (succ n)) (or, of Even n+2). So we see that we have:

and so on. In other words, we've constructed a type family, indexed by \(\mathbb{N}\) whose members are inhabited only at the evens. There's just no way to construct an element of type Even 1, or Even 3, and so on.

Hopping over to the logical view of this type, Even n corresponds to the proposition "\(n\) is even", and in this way Even may be regarded as a predicate over the naturals.

What can we do with such a thing? Well, we can do a few things. To begin with, we we can, dare I say it, leave proofs in our code instead of tests. Let us suppose we have a function; a very simple function, call it h() (since we've already used f() & g()):

h : Nat -> Nat
h x = x*2

And suppose we'd like to verify that our function always returns an even number. We could of course write tests in which we applied h() to various input & verify that the results are even, but that would only verify that h() returns an even for those particular inputs. Let's try to do a bit better.

Let's assert that for every natural x, we can find an inhabitant of the type Even (h x):

h_is_even : {x : Nat} -> Even (h x)

The type of h_is_even is that of a function: given a natural number, we are promising to produce an element of type Even (h x). The curly braces around x just mark x as an implict argument. Regarding h_is_even as a function, let's match, as usual, on the structure of its parameter. Being a Nat, x can have only two forms: either Z or S k for some other Nat k:

h_is_even : {x : Nat} -> Even (h x)
h_is_even {x = Z} = ZIsEven
h_is_even {x = (S k)} = ?h_is_even_rhs

The case in which x is zero is easy: we just return ZedIsEven. The "successor" case is more interesting. I mean, we know how it should go: we'll just be applying Plus2IsEven to… well, to whatever the image of k under h_is_even is. If we were working on the logic side of things, we'd be working inductively: the base case would be zero, which we've solved. Now we need the inductive step, which looks like: given a proof that h k is even, we need to produce a proof that h (k+1) is even.

The computational equivalent of induction is recursion. If we know the result for h k, then the result for x is Plus2IsEven applied to that thing:

h_is_even : {x : Nat} -> Even (h x)
h_is_even {x = Z} = ZIsEven
h_is_even {x = (S k)} = Plus2IsEven (h_is_even {x=k})

While this is appealing, the truth is it's not really something Idris focuses on. TODO quote Edwin.

A second application is picking-out a subset of an already-defined type. Let's suppose we want to write a function to halve its input:

half : Nat -> Nat
half Z = Z
half (S (S k)) = 1 + half k
half (S k) = half k

Fine… and yet: it's unsatisfying to truncate odd numbers. Wouldn't it be nicer if we could only define half() over the evens? With propositions, we can:

half2 : (n : Nat) -> Even n -> Nat
half2 Z ZIsEven = Z
half2 (S (S k)) (Plus2IsEven x) = 1 + half2 k x

half2() takes a second parameter, an element of Even n. Looked at another way, this argument could be viewed as a proof that n is even. And indeed, the type-checker sees this: it doesn't demand that we handle the case half2 S k.

Alright, but now our callers are forced to provide said proof term whenever they want to invoke our function, like so:

half2 : (n : Nat) -> Even n -> Nat
half2 Z ZIsEven = Z
half2 (S (S k)) (Plus2IsEven x) = 1 + half2 k x

namespace test
  x : Nat
  x = half2 4 (Plus2IsEven (Plus2IsEven ZIsEven))

To avoid this, we can leverage Idris' support for implicit arguments. By making the proof term implicit, Idris will search for a proof:

half3 : (n : Nat) -> {auto prf : IsEven n} -> Nat
half3 Z {prf = ZIsEven} = Z
half3 (S (S k)) {prf = (Plus2IsEven x)} = 1 + half3 k

namespace test
  x : Nat
  x = half3 8

  failing
    y : Nat
    y = half3 7 -- 👈 fails with "Can't find a value of type Even 7"

10/13/24 19:23