## Type-Level Induction in Haskell

The code from this post is available as a gist.

One of the most basic tools for use in type-level programming is the Peano definition of the natural numbers:

Using the new `TypeFamilyDependencies`

extension, these numbers can be used to describe the “size” of some type. I’m going to use the proportion symbol here:

Using this type family we can describe induction on the natural numbers:

```
class Finite n where
induction ∷ t ∝ Z → (∀ k. t ∝ k → t ∝ S k) → t ∝ n
instance Finite Z where
induction z _ = z
{-# inline induction #-}
instance Finite n ⇒ Finite (S n) where
induction z s = s (induction z s)
{-# inline induction #-}
```

The `induction`

function reads as the standard mathematical definition of induction: given a proof (value) of the zero case, and a proof that any proof is true for its successor, we can give you a proof of the case for any finite number.

An added bonus here is that the size of something can usually be resolved at compile-time, so any inductive function on it should also be resolved at compile time.

We can use it to provide the standard instances for basic length-indexed lists:

Some instances for those lists are easy:

However, for `Applicative`

, we need some way to recurse on the size of the list. This is where induction comes in.

This lets us write `pure`

in a pleasingly simple way:

But can we also write `<*>`

using induction? Yes! Because we’ve factored out the induction itself, we just need to describe the notion of a “sized” function:

Then we can write `<*>`

as so:

```
instance Finite n ⇒
Applicative (List n) where
pure x = induction Nil (x :-)
(<*>) =
induction
(\Nil Nil → Nil)
(\k (f :- fs) (x :- xs) → f x :- k fs xs)
```

What about the `Monad`

instance? For that, we need a little bit of plumbing: the type signature of `>>=`

is:

One of the parameters (the second `a`

) doesn’t have a size: we’ll need to work around that, with `Const`

:

Using this, we can write our `Monad`

instance:

```
head' ∷ List (S n) a → a
head' (x :- _) = x
tail' ∷ List (S n) a → List n a
tail' (_ :- xs) = xs
instance Finite n ⇒
Monad (List n) where
xs >>= (f ∷ a → List n b) =
induction
(\Nil _ → Nil)
(\k (y :- ys) fn → head' (fn (Const y)) :-
k ys (tail' . fn . Const . getConst))
xs
(f . getConst ∷ Const a n → List n b)
```

## Type Family Dependencies

Getting the above to work actually took a surprising amount of work: the crux is that the `∝`

type family needs to be injective, so the “successor” proof can typecheck. Unfortunately, this means that every type can only have one notion of “size”. What I’d prefer is to be able to pass in a function indicating exactly *how* to get the size out of a type, that could change depending on the situation. So we could recurse on the first argument of a function, for instance, or just its second, or just the result. This would need either type-level lambdas (which would be cool), or generalized type family dependencies.