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

```
data ℕ
= Z
| S ℕ
```

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:

`type family (t ∷ k) ∝ (n ∷ ℕ) = (a ∷ Type) | a → t n k`

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

```
class Finite n where
Z → (∀ k. t ∝ k → t ∝ S k) → t ∝ n
induction ∷ t ∝
instance Finite Z where
= z
induction z _ {-# inline induction #-}
instance Finite n ⇒ Finite (S n) where
= s (induction z 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:

```
infixr 5 :-
data List n a where
Nil ∷ List Z a
:-) ∷ a → List n a → List (S n) a (
```

Some instances for those lists are easy:

```
instance Functor (List n) where
fmap _ Nil = Nil
fmap f (x :- xs) = f x :- fmap f xs
```

However, for `Applicative`

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

`type instance '(List,a) ∝ n = List n a`

This lets us write `pure`

in a
pleasingly simple way:

```
instance Finite n ⇒
Applicative (List n) where
pure x = induction Nil (x :-)
```

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:

```
data a ↦ b
type instance ((x ∷ a) ↦ (y ∷ b)) ∝ n = (x ∝ n) → (y ∝ n)
```

Then we can write `<*>`

as
so:

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

What about the `Monad`

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

is:

`>>=) ∷ m a → (a → m b) → m b (`

One of the parameters (the second `a`

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

:

`type instance (Const a ∷ ℕ → Type) ∝ n = Const a n`

Using this, we can write our `Monad`

instance:

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

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