Type-level programming

Wipple’s type system is so powerful, you can write programs that are executed entirely by the type checker! It turns out that values can correspond to types, and functions can correspond to traits. Let’s look at a simple example of “type arithmetic”:

Z : type
S : N => type

Here, we define Z to represent zero and S to represent the “successor” to a number. For example, one is represented by S Z, two is represented by S (S Z), and so on. These types are effectively the same as an enumeration at the value level:

N : type {
    Z
    S N
}

You might notice that at the type level, Wipple doesn’t restrict what type you provide to S — you could provide Text or any other type. At the type level, Wipple is effectively dynamically-typed!

Now that we have our data, we can write a function to add together two numbers. This is defined using a trait:

Add : A B Sum => trait

Notice that we don’t have a value after the trait definition. This prevents the trait from being used in a value position; that is, it can only be referenced as a bound in a where clause. Similarly, we omit the value when we declare an instance:

A => instance (Add A Z A)

This is our base case — any “value” A plus zero is equal to A. Our second instance is a bit more complicated:

A B Sum where (Add A B Sum) => instance (Add A (S B) (S Sum))

This definition states that if you can add A and B together to get a Sum, then A plus the successor of B is equal to the successor of Sum — a + (b + 1) = (a + b) + 1. The recursion terminates when B is zero and the base case is reached. Essentially, you do the addition by repeatedly adding one to the input!

Now let’s use our Add “function” — remember that we’re working at the type level, so to perform a computation, we need to use a type annotation:

result :: Sum where (Add (S (S Z)) (S (S (S Z))) Sum) => Sum
result : ...

And now we can print result’s type by raising a type error:

_ : _ -> result

The error tells us that Sum is S (S (S (S (S Z)))), proving that 2 + 3 = 5!

error: could not determine the type of this expression
   ┌─ playground:11:5
   │
11 │ _ : _ -> result
   │     ^^^^^^^^^^^
   │     │
   │     try annotating the type with `::`
   │     this has type `a -> S (S (S (S (S Z))))` for some unknown type `a`

Let’s try another example — determining if a number is odd or even! We’ll start by defining our data:

Z : type
S : N => type

Odd : type
Even : type

And now we’ll make our function, which accepts a number N and returns a kind Kind (Odd or Even):

Odd-Even : N Kind => trait

Our base case is that Zero is Even:

instance (Odd-Even Z Even)

And now we implement the recursion! If n + 1 is odd, then n is even, and vice versa:

N where (Odd-Even N Even) => instance (Odd-Even (S N) Odd)
N where (Odd-Even N Odd) => instance (Odd-Even (S N) Even)

Let’s try it out!

zero :: A where (Odd-Even Z A) => A
zero : ...
_ : _ -> zero

one :: A where (Odd-Even (S Z) A) => A
one : ...
_ : _ -> one

two :: A where (Odd-Even (S (S Z)) A) => A
two : ...
_ : _ -> two

Sure enough, zero is even, one is odd, and two is even:

error: could not determine the type of this expression
   ┌─ playground:14:5
   │
14 │ _ : _ -> zero
   │     ^^^^^^^^^
   │     │
   │     try annotating the type with `::`
   │     this has type `a -> Even` for some unknown type `a`

error: could not determine the type of this expression
   ┌─ playground:18:5
   │
18 │ _ : _ -> one
   │     ^^^^^^^^
   │     │
   │     try annotating the type with `::`
   │     this has type `a -> Odd` for some unknown type `a`

error: could not determine the type of this expression
   ┌─ playground:22:5
   │
22 │ _ : _ -> two
   │     ^^^^^^^^
   │     │
   │     try annotating the type with `::`
   │     this has type `a -> Even` for some unknown type `a`

A practical example: first and rest

At the value level, you can use the first and rest functions to obtain the first item in a list or the items after it. These functions return Maybe values, since the input list could be empty. But at the type level, we can ensure that the list is non-empty! To start, let’s create a new list type along with a nil constructor:

Z : type
S : N => type

List : A Count => type -- no need to store an `A` because we don't care about
                       -- the list's value

nil :: A => List A Z
nil : ...

And now we can implement first like so:

first :: A Count => List A (S Count) -> A
first : ...

Notice that first requires that the list’s Count be the successor of a number; this is effectively saying that Count must be greater than zero. rest is similar:

rest :: A Count => List A (S Count) -> List A Count
rest : ...

Here, we make sure to reduce the Count by one in the returned list.

And lastly, let’s implement cons:

cons :: A Count => A -> List A Count -> List A (S Count)
cons : ...

Now let’s test our program!

my-list : cons 1 (cons 2 (cons 3 nil))
first my-list -- works!
first (rest my-list) -- works!
first (rest (rest (rest my-list))) -- fails!

The last line fails with a type error:

error: mismatched types
   ┌─ playground:22:7
   │
22 │ first (rest (rest (rest my-list))) -- fails!
   │       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `List Number (S a)` for some unknown type `a`, but found `List Number Z`

Awesome, now we have compile-time bounds checking!