Posted on May 5, 2018

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

``````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 :-)
(<*>) =
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:

``(>>=) ∷ 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:

``````head' ∷ List (S n) a → a
head' (x :- _) = x

tail' ∷ List (S n) a → List n a
tail' (_ :- xs) = xs

instance Finite n ⇒
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.