# 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!