Type systems are theorem mini-languages

This is related to what’s called the Curry-Howard correspondence, and is a neat concept that I recently discovered and felt like sharing. The correspondence more strongly claims that a function is equivalent to a logical proof of its return type given the types of its arguments.

In other words, when you compile a function, you’re making a claim of the function’s type correctness and embedding a proof of this claim. Any static checks a compiler does consist of extracting this claim and verifying your proof. Since whole programs can be understood as compositions of many functions, it follows that an entire program is such a claim. Naturally, the conclusion is that, among the functionalities type systems provide, they can always serve as formal verification tools.

This is obvious to anybody who has worked with strong static typing. A number of popular languages have taken to including very expressive type systems to allow programmers to have the compiler verify the correctness of their program at compile time.

As a simple example, take the following Haskell type declaration:

cons :: a -> [a] -> [a]

In English, “cons takes a value of type a and a list of elements with type a and produces a list of elements with type a.” The function cons must be written so that all possible invocations fit this declaration, thereby proving that cons behaves as claimed.

Let’s imagine a programming language with a heterogeneous list whose type can express things about the elements contained inside of it:

# The list may contain elements of either type a or type b.
List(a, b)
# The list may contain an element of type a.
List(a, ..)
# The list contains no element of type b.
List(¬b, ..)

We could now write a heterogeneous version of cons as follows:

hcons :: a -> List(b, ..) -> List(a, b, ..)

We could keep going! Let’s consider some other functions that operate on instances of our imagined type:

# Returns true if there exists an element in the list for
# which the predicate is true.
hexists :: (a -> Boolean) -> List(a, ..) -> Boolean
# Removes all elements of the given type.
hremove :: for some a, List(a, ..) -> List(¬a, ..)
# Maps elements of a type using the given function.
hmap :: (a -> b) -> List(a, ..) -> List(b, ..)
# Converts a heterogeneous list to a homogeneous list
tohom :: List(a) -> [a]

And yet, for as powerful as this seems, it’s clear that there are functions whose type cannot be expressed using this syntax. For example, we cannot express the type of an hhead function that returns the first element in a list. We could extend the type syntax to allow hhead’s type to be written (and therefore have the compiler prove that the definition of hhead fits it), but this new syntax would inevitably have its own shortcomings.

Taken to its extreme, we can imagine an entirely new type system where a function’s type is a formal description (indeed, a theorem) of its return type, given some assumption about its input types.

for pred: a → Boolean, hl: HetList(ts: [..]), 
if ts contains a,
then hexists :: pred → hl → Boolean
for fn: a → b, hl: HetList(ts: [..]),
hmap :: fn → hl → HetList([m(t) | t ∈ ts])
where m(a) = b, m(t) = t
for hl: HetList([t]),
tohom :: hl → HomList(t)

We can even express types that the previous system didn’t let us.

for hl: HetList([t, ..]),
hhead :: hl → t
for hl1: HetList(ts1: [..]), hl2: HetList(ts2: [..]),
hconcat :: hl1 → hl2 → HetList(ts1 ++ ts2)

for hl1: HetList(ts1: [..]), hl2: HetList(ts2: [..]),
hzip :: hl1 → hl2 → HetList(zip(ts1, ts2))

It’s clear that the most general type system is one that allows the programmer to express types this way. The relatively limited type systems that many existing languages give us are more or less restricted versions of such a system. In this system, the programmer writes a type as a theorem, and the body of a function as a proof, and the compiler verifies the proof. As it turns out, more familiar type systems, while different, serve the same purpose! The key difference is that the language authors have chosen a type system that has a good balance between being useful and being easy to prove. In this sense, type systems are mini-languages for expressing theorems.

I’m not sure how this is useful, I don’t know where I’m going with this, and I preemtively apologize for relating it to the Curry-Howard correspondence, but I felt this was an interesting share! Approach your type systems at a new angle!