If you’ve ever delt with a functional language on the maths-first end of things, you’re most likely aware of the wild concepts, mainly expressed through maths, that many adherents of them take for granted. While sort systems aren’t necessarily as flashy or useful, they form the fundamentals of a language’s way of handling types.

A Short Foreword #

Asking somebody about their salary, asking a physicist to define energy, and asking a functional programmer why all the mathematics involved is good and beneficial — these are questions you should most likely avoid asking.

Many people interested in functional languages, particularly languages on the theoretically preferential side I like to think of languages sitting on a spectrum. On one side, it’s languages that see the computer as hardware. On the other, languages that backport lambda calculus into x86 assembly. Each language then starts at some point on this spectrum and gets sucked closer to either which side. are motivated in large part by a passion for mathematics, be it directly useful or not. Disclaimer: I am one of those people, too.

However, this doesn’t (and it shouldn’t) automatically disqualify these languages from ever being useful. Or even more/less useful than others, though I’m not convinced ‘usefulness’ forms anything more than a preorder. As we’ll see, these mathematical abstractions help us abstract our code, too – and since we’re talking about types, give us more expressiveness, and a better understanding of type systems in general.

I’m writing this post to confine all the bits of explanations I’ve read over the ages into a single place. For example, kinds are fairly well explained in the domain of Haskell programming, however going beyond Haskell, or beyond kinds into sorts, usually yields unfavourable search results.

In fact, the most information (and most enlightening too) was a lecture given by Peyton-Jones at some point on generally exploring the type space of languages. I cannot find it now, but I’ll link to it when I find it. He is a very charismatic presenter, and watching any talk of his will leave you slightly more informed, as well as feeling like you could tackle all of the high-level maths head-first (which you can).

A lot of this post will, most likely, draw from that lecture and/or other talks he’s given, though not exclusively.

This post is primarily aimed at those getting into type theory, or interested in a systematisation of type systems, curious to learn more. A healthy dose of Haskell knowledge will help, though it isn’t strictly necessary, so long as you understand the type annotation and polymorphism syntax (i.e. fmap :: Functor f => (a -> b) -> f a -> f b). C++ templates are also mentioned, though they’re only there as an example.

Lastly, after discussing each type-kind-sort level individually, we’ll look at Agda, which lets us traverse infinitely high on this ladder with its Universes. After that, I’ll briefly mention Idris (in the context of dependently types languages), and Sage (in the context of pure type systems).

Ascending the Abstraction Pyramid #

The sort ladder is infinite. In fact, some languages let you use all infinite levels of it! Luckily for us, it’s a lower-bounded kind of infinity: we have somewhere to start from.

If you remember induction from high-school math — proving for a base case, a general case, and then the next-to-general case — sorts are structured like that, and that intuition will help you understand what ‘going up a level’ would entail.

Values #

All languages deal with values. It’s their primary specialty. What’s more, if they couldn’t manipulate values, then they wouldn’t be very useful. As a heads up, in lambda calculus, values are referred to as terms, which you might read in further literature.

Values are the things that expressions evaluate to: 3, "a string", new Dog(). Over them, we have functions that can take in some values and produce a new one:

function add(x, y) {
	return x + y;
}

Some languages let you use functions as values too:

auto add = [](int a, int b) -> int { return a + b; };

In languages such as Python, JavaScript, Lua, we only ever worry about values. We could effectively say that these languages are untyped: they don’t possess any types. On their Wikipedia page, though, you’ll see that they’re dynamically typed.

Dynamically typed means that values are assigned types at runtime, and that all types are kept consistent throughout the program’s lifetime. However, since we, as programmers, don’t have any insight into how the runtime system works, we can only ascertain that things break when we pass in values that don’t like the things we’re doing to them. But what if we pass in a value that’s of a ‘different type’ – whatever that means – that supports everything that we want to do with it?

This would be consistent with the language being untyped and such ocurrences as happenstance. However, duck and structural typing say that the type of a value actually only depends on what the value looks like: if it looks like a duck and quacks like a duck, it’s a good enough duck-like value.

The distinction here isn’t clear The fine distinctions are pretty well discussed in this StackOverflow post. since dynamic typing means we can weasel out of giving a definitive yes-or-no answer for an input program. We simply defer that checking to runtime, where things either happen gracefully or we crash.

Crashing is, among other things, why we might decide to classify our values. For one, it helps programmers make more assertions about their code. And it helps language designers and compiler developers know what to expect ahead of time: how much memory needs be allocated, what’s the optimal way to pass arguments to a procedure, etc.

Types #

Types are, in their simplest, ways to classify values. If we look at all possible values like LEGOs spread out across the floor, if we start to group the bricks together by some criterion – like colour – we’ll end up with a bunch of piles. Those piles are types.

The exact method of piling these values together can vary. We might bunch all numbers together: now we have a language that doesn’t differentiate between ints and floats. We might group values by the way they’re structured: we’ve just added support for simple C structs.

A type is, abstractly speaking, a collection of values. In fact, we can think of it as a set. This line of reasoning will help us a lot, though it isn’t strictly always true, especially not for all languages.

Since we know types are really sets, we can look into them:

We can ask questions such as $"string" \in \tt{Integer}$?

We can define functions as set functions:

Here we needed two input values for our function. Set functions simply map elements of one set (the domain) onto elements of another set (the codomain). This might make it sound like taking “multiple input values” is impossible. To ‘step around’ this issue we can use the Cartesian product of two sets, which gives us a new set that contains pairs of values from each set. That way we can pack multiple values into a single element.

What happens when we introduce subset relationships in our types? $2$ is at least in $\N$, but $\N \subset \Z \subset \R \subset \cnums$ means $2$ is also a complex number. I leave working out the implications of subsetting and value-sharing as an exercise to the reader (for further reading, ‘subset’ maps pretty well onto the ‘subtype’ relation).

An interesting thing to note is that, when we can’t inspect the elements of sets themselves, we can only differentiate sets by how they behave. And any two sets of the same length can be easily mapped to-and-fro just by matching each element of one set with another from the other set, and choosing the same pairs for the function going in reverse. That way walking $A \to B \to A$ gets us to where we started.

This mapping is called an isomorphism, and is why two-value enums and boolean values are really the same thing, just like how (int, char) are the same as (char, int), or maybe less obviously List<int> and Tree<int>. You can store values as either type, and seamlessly move back and forth between the two without losing any information.

This set thing has worked out great for us so far. However, we do run into some issues upon further inspection.

Function Types #

The least worrying issue, perhaps, is writing function value types. That is, let’s say we have some function:

char apply(char (*f)(int), int a) {
  return f(a);
}

How do we write it in our set function notation? A simple (but still correct) answer would maybe look like:

If functions are also values in our type system, then that means there is at least one type that holds all the function values. And since we know that types are sets, and there exists a type for functions, there must also exist a set that contains functions.

Functions are set mappings that exist between sets. But in our case, they’re regular elements of some sets, too! The type of a function is really the set of all implementations for that function signature.

In this case, set theory doesn’t give us adequate notation to fully encode the type of a function value. We can introduce a new operator to better express this:

When we say $Int \Rightarrow Int$ we mean the set of all functions mapping the left-hand side of the arrow onto the right-hand side. Really this isn’t much different from the usual arrow:

which looks like almost valid Haskell code!

Pointer Semantics #

Let’s imagine a language much akin to C. In fact, this language is a slightly stricter version of C. How is it stricter? Well, we know C is a weakly typed language, meaning it will allow you to do implicit casts practically wherever.

You can call functions taking floating-point numbers with integers, you can store character values into long variables, etc. Our C dialect does almost the same. It will let you do a lot of the same type conversions. However, it pays special care to pointer and non-pointer types.

If a function takes an int * parameter, you can pass it a void *, char *, struct Calendar *. But, you cannot pass a regular int, size_t, or any other type. The same is true vice-versa: you cannot initialise an int variable with an int * value.

Now, when we’re compiling the program, we have to look at every use of a variable and make sure that the types are valid. In particular, we have to make sure the programmer isn’t using pointer types where non-pointer types are wanted, and we want to print an error if he does.

A Short Showcase of Lambda Calculus #

Set theory notation becomes increasingly hard to use to demonstrate types and type semantics, at least without introducing a big corpus of category theory knowledge.

Instead, the much easier alternative is switching to lambda calculus, which I will do hereafter.

The formal definition of lambda calculus is given in just three rules:
Let $\Lambda$ be the set of all lambda expressions

1. If $x$ is a variable, then $x \in \Lambda$ follows
2. If $B \in \Lambda$ and $x$ is a variable, $(\lambda x. B)$ is also a lambda expression
3. If $F, A \in \Lambda$, then $(F A) \in \Lambda$ follows

This syntax can be used to express simple, untyped terms, as discussed in ii.1. Values. We can extend it to include types as follows:

If $\alpha$ is a type, $x$ is a variable and $B$ is a lambda expression: $\lambda x: \alpha. B$

In effect, this defines a function that takes some value $x$ that has type $\alpha$ and then evaluates the body $B$.

So for a function that adds two ints together, when we type the parameters as int, what we really mean is:

where nonpointer is any type that isn’t a pointer type, and $+_{\tt{int}}$ is addition over ints.

Now, wait a minute! What we’ve effectively now done is reduce our rich and vibrant type collection into just two types: pointer and nonpointer, which we know isn’t true. We still need types for memory allocation, access, struct member fields, etc.

The types pointer and nonpointer aren’t actually types, they’re different kinds of types. They’re two categories we can put our types in: either they’re pointers or they aren’t.

Generics #

Generic programming is great. It lets us write our code once, encapsulating the structure, and then lets us apply it over a span of different types. Undoubtedly, you’ve written code that uses them: List<Integer>.

In particular, C++ templates are my favourite kind of generics. They let you pass in a lot more than what Java would allow. They also let you write specialised definitions depending on one or all of the template parameters. They take in both types and values, allowing for some light dependent typing.

Let’s take a look at how a binary tree might be written in C++.

template<typename T>
class binary_tree {
	struct node {
		std::tuple<binary_tree<T>*, binary_tree<T>*> trees;
		T value;
	};

	node *_node;
};

This is a toy example and isn’t meant for production use. However, we can see that a tree is either a node with a value and two pointers to two other trees, or it’s the end of the tree.

Similarly, we can implement a rose tree – an n-ary tree:

template<typename T>
class rose_tree {
	struct node {
		std::vector<rose_tree<T>*> trees;
		T value;
	};

	node *_node;
};

Notice anything similar? In fact, the last two snippets are the same, save for the type of node::trees. When we have repeating code, we factorise it to get one copy and two instances. Let’s try it:

template<typename C, typename T>
class tree {
	struct node {
		C<tree<C, T>*> trees;
		T value;
	};
};

Except that this won’t work. The compiler complains that C isn’t a template, so we can’t apply it to tree<C, T>*. If you’re well versed enough in C++ templates, you’ll know that we have to pass what’s called a template template parameter. That is, a parameter to a template that is a template itself.

template<template<typename> typename C, typename T>
class tree {
	struct node {
		C<tree<C, T>*> trees;
		T value;
	};
};

There we go. Now, the definitions of the other trees are as follows:

template<typename T>
using double_pair = std::pair<T, T>;

template<typename T>
using binary_tree = tree<double_pair, T>;

template<typename T>
using rose_tree = tree<std::vector, T>;

Notice how in the implementation of the general tree, we had to explicitly differentiate the container type C and the item type T. We know they’re both types, except that one is also a template.

Very similarly, we can agree that std::vector is a type. However, you can’t The C++17 deduction guides only improve automatic type inference. You write std::vector, but it infers std::vector<int>. bind a variable to that type. std::vector<int> on the other hand is a more ‘complete’ type, that you can get values of.

Somehow, both of these types are types, but they’re fundamentally different in such a way that we cannot mix them.

OOP-style Polymorphism #

The very beginning lecture on polymorphism in object-oriented programming languages: we have a Mammal, a Human, and a Dog. Here’s a diagram for your viewing pleasure:

Where we expect a value of type Mammal, both Mammal, Human, and Dog will do. If you’ve done your homework and looked into subtyping, as mentioned in ii.2. Types, you could argue that this works because Dog and Human are subtypes of Mammal.

I’m not disputing this. However, we can say that for some type $\alpha$, we can get the set of types $<:_{\alpha}$ (pronounced sub-alpha) that are subtype to $\alpha$. So, when we ask for a Mammal, just like in the C dialect example, we actually mean a set of types.

Kinds #

This is the Big One: the weird name and concept you’ve never dealt with before. Well, except that you have. So far we’ve looked at values, and we’ve defined types as sets of values. We’ve also played with this definition of type by applying it to code and seeing if issues crop up.

In fact, we’ve seen our set-of-values type definition fall short a few times. We can’t really split between (non-)pointer types, and we have trouble handling template (template) parameters.

If you look back at how we started our intuition on types, we emptied our box of LEGO values all over the floor and started grouping them. By grouping similar values together into distinct piles, we got types. In other words, types are a way to classify values.

Kinds extend this concept by letting us classify types. When we look at std::vector and std::vector<int>, we recognise they’re not only different types, but different kinds of types, too: the former is missing template parameters.

Similarly, in our tree example, there is a profound difference between the container template parameter (template<typename> typename C – a mouthful), and the item type parameter (typename T).

And just as types are sets of values, kinds are sets of types. When we were talking about (non-)pointer types in the C dialect example, we were actually referring to kinds. Since we accept more than one type, instead of distilling our types into two, we can add an extra layer of categorisation. We can then pick whichever type from the category.

Quite a mouthful, but let’s look at it bit-by-bit. We first introduce the type variables $X$ and $Y$. Just how regular variables hold terms, type variables hold types.

We then say that the type variables $X, Y$ have the kind $\tt{nonpointer}$, meaning they can be any type from that kind (just how $x:N\!at$ lets $x$ be any natural number).

We then introduce the variables $x, y$ and type them as $X, Y$ respectively.

Applying kinds to classify types to fix our template issues might seem a bit daunting. Luckily for us, we can borrow some kinds from Haskell. Haskell defines two Actually, Haskell has more kinds, especially with the new additions of levity polymorphism and linear arrows. Also, I’ll be using the more ‘modern’ Type instead of the older * kind name, since that seems to be prevailing in newer literature. kinds, Type, and the binary operator (->). Perhaps seeing an example first might better help illustrate:

Int :: Type

List     :: Type -> Type
List Int :: Type

We can see that Int has kind Type, but List has kind Type -> Type! The similarity to the function arrow isn’t accidental. List is a type, yes, but it needs to be applied to a Type before it becomes a Type.

So, what’s the kind for our C++ tree? Well, we take in a template, which is Type -> Type, and we take in the item type, which is a regular Type. So, the kind of tree is:

tree :: (Type -> Type) -> Type -> Type

As we can see, tree still takes in two types, but one of those types actually takes in another type itself. We still get all the benefits from precise types, but we also get the expressiveness and accuracy in requiring a broad range of a certain kind of type — namely, one that takes in another type itself.

Let’s now explore a bit stranger type construction.

data IntContainer f = IntContainer (f Int)

We define a type that will take a container type, and put Int into it. So, the kind of f here is Type -> Type, meaning the kind of IntContainer :: (Type -> Type) -> Type.

Now we define a simple ‘type application’ datatype:

data ApplyT f a = ApplyT (f a)

Not much happens here: we take an f, an a and apply it to that f, getting a Type in return. So, what’s the kind of ApplyT? You could say

ApplyT :: (Type -> Type) -> Type -> Type

and that would work for a wide range of types. But what happens when we try to write ApplyT IntContainer List? Suddenly, everything breaks! The kinds don’t match up anymore. We have:

IntContainer :: (Type -> Type) -> Type
List :: Type -> Type
ApplyT :: (Type -> Type) -> Type -> Type

We’re trying to fit the IntContainer :: (Type -> Type) -> Type peg into a (Type -> Type) shaped hole.

What we really mean with ApplyT is, take an f, take an a that’s applicable to f, and return that type. We need to work for both (Type -> Type) and (Type -> Type -> Type) and so on and so forth. We can do this with a little trick called kind polymorphism.

Instead of rigidly defining the left hand side, we bind a kind variable and let it span over all kinds:

data ApplyT (f :: k -> Type) (a :: k) = ApplyT (f a)

This might seem a really strange and foreign concept, but a very close equivalent in C++ looks like this:

template<
  template<typename...> f,
  typename ...as>
using apply_t = f<as...>;

The difference is that the C++ version’s f can be Type -> Type, Type -> Type -> Type, et cetera, whereas the Haskell version f is one of Type -> Type, (Type -> Type) -> Type, et cetera. The same is true for the other type parameter(s). Can you see what the syntax for that would look like in C++?

Extending Kinds into Sorts #

Remember when I said that Haskell only has two kinds? Well, it has a few more. In particular, type constraints are represented with the Constraint kind. For example, Num :: Type -> Constraint, from which Num a :: Constraint follows.

In fact, the GHC ConstraintKinds extension, lets you write types of kind Constraint, with some limitations, but a lot more freely than without it. You can then, for example, define a type of kind Constraint that would be an alias for (Ord a, Eq a).

So, now that we have Constraint and Type as kinds, and (->) as a kind operator, what do we exactly mean when we use kind polymorphism and say forall k. (k -> Type) -> k -> Type? What exactly can k be?

We’ve seen this bounded polymorphism problem before with our pointer, non-pointer implicit casts! The problem there was retaining the classification of values by type (i.e. int, char), but putting bounds on what types we can cast from. To solve it, we created two new kinds of types: pointer and non-pointer types.

Applying the same logic here, we can define a new sort of kind, which is the set of all possible applications of Type and (->) called Concrete, representing ‘concrete’ kinds: those which eventually correspond to values, instead of typechecker rules. Then, we can accurately specify

data ApplyT forall (k :: Concrete) (f :: k -> Type) (a :: k). = ApplyT (f a)

…if you could specify and use sorts in Haskell. Sadly for us, Haskell stops here. However, the insight we’ve gained by walking up so far is pretty significant, especially if you’re starting out with a rudimentary knowledge of types.

Infinite Sorts of Universes: A Regular Day in Agda #

Agda is a dependently typed functional language. In my math spectrum classification of programming languages, Agda sits neatly with a high math-to-computer ratio. Its high barrier of entry and academic nature destined it for failure within the mainstream (at least so far), so it’s often reduced to a proof assistant (which it can be).

Dependent types mean that the barrier between terms (values) and types is removed, allowing function to take in and return types, as well as types being specified by values (more on that later). Its syntax is similar to that of Haskell. For example, below is a small program defining a data type and a function.

data Greeting : Set where
  hello : Greeting

greet : Greeting
greet = hello

Note how we had to specify that the type Greeting belonged in Set. Since we know that values form sets (called types), a collection of all values is really the collection of all sets. Also note how I am referring to all types as forming a collection. This is because you cannot form a set of all sets.

To avoid this paradox, as well as stay consistent with the original type theory, Agda introduces an infinite amount of sorts, also called universes. Namely, the base sort is the above-mentioned Set. But what is the sort of Set? Well, it’s Set1, and Set1 : Set2, and so on and so forth.

Being a dependently typed language, Agda lets us write data types and functions that operate on types: all types, not just small types in Set.

Borrowing from the Agda manual, we’ll look at an example where larger-than-Set might be useful.

Let’s define a product type.

data Product (A B : Set) : Set where
  _×_  : A → B → Product A B

This lets us use pair values such as 4 × 3, "string" × (12.4 × '1').

Now, let’s define a list type.

data List (A : Set) : Set where
  Nil  : List A
  _::_ : A → List A → List A

And now we have list values like "string" :: 12.4 :: '1' :: Nil.

So, let’s try to take a list of types (such as [Int, Char, Bool]) and form a product of them (that being (Int, Char, Bool)).

Prod : List Set → Set
Prod (A :: As) = A × (Prod As)
Prod Nil       = T

If we tried to compile this, we would get an error. Indeed, if we look at how List is defined, we say that its type parameter A is a Set, but now we’re trying to make A a ‘large’ set – that is – a collection of small sets.

The solution is to simply move List up a universe and let it contain large sets:

data List₁ (A : Set₁) : Set₁ where
  Nil  : List₁ A
  _::_ : A → List₁ A → List₁ A

If we substitute List for List₁ in our example, we would get a functioning program.

Dealing with universe levels like this is tedious. We’ve just had to create a new list type, meaning we lose all our list functions (that have the same implementation), for each universe we want to use.

The way to abstract our code, like always, is to add polymorphism. Meet universe polymorphism. Agda gives us a universe level type Level and the general, level-polymorphic sort Universe (ℓ : Level). With it, our list definition becomes

data List {n : Level} (A : Set n) : Set n where
  []   : List A
  _::_ : A → List A → List A

All list functions are now transitively level-polymorphic as well, and we can use the same foldls we’re used to, in whichever universe we’re in.

This self-referential and infinite structure leads to some interesting contradictions and inconsistencies which are carefully avoided. I could talk about them here, but it’s probably best if you checked out the Agda manual on it yourself.

A Passing Mention of Dependent Types #

As I’ve mentioned before, a dependently typed language (or type system, rather) doesn’t differentiate between values and types. In other words, more closely to the term’s etymology – types can depend on terms too.

More formally, let $A : \cal{U}$ be a type in a universe $\,\cal{U}$. Then, let $B$ be a type family $B : A \to \cal{U}$ that maps every term $a : A$ to a type $B(a) : \cal{U}$. The type $\prod_{x:A}B(x)$ denotes a function that takes terms $a : A$, but returns type $B(a)$, depending on $a$.

This might be hard to follow, so let’s restep it slowly. We’re given some type, $A$ – out of a collection (universe) of types $\cal{U}$. Next, we’re given a mapping from a value in $A$ (which is a regular value), to a value in $\,\cal{U}$ (which is a type – sibling to $A$).

We know how to map values to types ($B(a)$), and given the values ($A$), the input ($a:A$), and the types ($\,\cal{U}$), we can construct the type of a function taking in a value in $A$, but returning a value in $B(a) : \cal{U}$, denoted with $\prod_{x:A}B(x)$ – called a dependent product type, or just a pi-type.

More practically, this lets us do fun compile time things, like constructing the search result type of a regular expression, preventing double-frees, ensuring program totality, or having known-length vectors (using type-level arithmetic).

Here is an implementation of a known-length vector datatype in Idris.

data Nat = Zero | Succ Nat

(+) : Nat -> Nat -> Nat
Zero     + a = a
(Succ l) + r = Succ (l + r)

data Vect : Nat -> Type -> Type where
    Nil  : Vect Zero a
    (::) : a -> Vect l a -> Vect (Succ l) a

append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys

We should now have the prowess to inspect this code more closely. Nat is defined as a regular data type, and so is (+) a regular function. However, since Idris is dependently typed, the distinction between type and term does not exist, and we can use the two interchangeably.

Next, the definition of Vect is of particular interest. Here, we specify its kind, too. We see that Nat is, in effect, promoted to a kind. Idris, compared to Agda, trades mathematical precision in syntax for ease of use and understanding. Whereas in Agda we would have had to specify the universes (and had the comfort of an infinite amount thereof), in Idris we write what’s closer to what we want.

Just two lines below and we use the data (value) constructor Succ l in a type, and in the type signature of append, we call (+) – further strengthening the dependent type paradigm.

Arbitrary code within types means that type checking dependently typed languages is not generally decideable, and not every valid program will be able to type check.

Purely For Pleasure: Pure Type Systems #

Pure type systems are, perhaps, the final and ultimate abstraction of the concepts discussed in this post. They combine the infinite sorts we saw in Agda, while allowing arbitrary dependencies between any of the universes.

Just how Idris collapsed types and terms into interchangeable concepts (but not kinds), pure type systems collapse all universes.

Of note, the Sage language implements a pure type system with gradual typing. It statically checks what it can, and generates type checking code to be executed run-time for what it can’t

I haven’t yet played with it, or read much about it, so anyone that’s read something about it, or even tried it, I encourage to write to me about their experience using the contact methods in the footer.

Where To, Now? #

Goodbyes are, it is known, the hardest to say: you are forced to condense a rich history into a few final words before moving on. Luckily, type theory is a gift that keeps on giving.

This was only a basic introduction to the concept of sorts, with mentions of set theory (precursor to category theory, the category of sets, in particular), lambda calculus and dependent types.

If you’re so inclined, you can take on further reading to improve your mathematical understanding of the field of programming languages – or you can appreciate the new insight you’ve (hopefully) gained from reading this.

In either case, I’m interested to hear your thoughts, opinions, suggestions, spotted typos, inconsistencies and others. While I cannot speak with enough confidence as Knuth to give out money (even imaginary fiat!) for your efforts, I can give you a hearty thanks. You can find methods of contacting me in the footer, below.