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
`int`

s and `float`

s. We might group values by the way they’re structured: we’ve
just added support for simple C `struct`

s.

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:

$\tt{unsigned \enspace int} = \{x\,|\,x \in \Z,\, x > 0\}$We can ask questions such as $"string" \in \tt{Integer}$?

We can define functions as set functions:

$\textstyle \begin{gather*} f:\tt{Number} \times \tt{Number} \to \tt{Number}\\ f(a, b) = a + b \end{gather*}$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:

$apply: IntToChar \times Int \to Char$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:

$apply: (Int \Rightarrow Char) \times Int \to Char$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:

$apply: (Int \to Char) \times Int \to Char$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

- If $x$ is a variable, then $x \in \Lambda$ follows
- If $B \in \Lambda$ and $x$ is a variable, $(\lambda x. B)$ is also a lambda expression
- 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 `int`

s 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 `int`

s.

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**. When we look at

*types*`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 `foldl`

s 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.