## Doing more with length-typed vectors

The post *Fixing lists* defined a (commonly used) type of vectors, whose lengths are determined statically, by type. In `Vec n a`

, the length is `n`

, and the elements have type `a`

, where `n`

is a type-encoded unary number, built up from zero and successor (`Z`

and `S`

).

`infixr 5 :<`

data Vec ∷ * → * → * where

ZVec ∷ Vec Z a

(:<) ∷ a → Vec n a → Vec (S n) a

It was fairly easy to define `foldr`

for a `Foldable`

instance, `fmap`

for `Functor`

, and `(⊛)`

for `Applicative`

. Completing the `Applicative`

instance is tricky, however. Unlike `foldr`

, `fmap`

, and `(⊛)`

, `pure`

doesn't have a vector structure to crawl over. It must create just the right structure anyway. I left this challenge as a question to amuse readers. In this post, I give a few solutions, including my current favorite.

You can find the code for this post and the two previous ones in a code repository.

### An Applicative instance

As a review, here is our `Functor`

instance:

`instance Functor (Vec n) where`

fmap _ ZVec = ZVec

fmap f (a :< u) = f a :< fmap f u

And part of an `Applicative`

instance:

`instance Applicative (Vec n) where`

pure a = ??

ZVec ⊛ ZVec = ZVec

(f :< fs) ⊛ (x :< xs) = f x :< (fs ⊛ xs)

For `pure`

, recall the troublesome goal signature:

` pure ∷ a → Vec n a`

There's at least one very good reason this type is problematic. The type `n`

is *completely* unrestricted. There is nothing to require `n`

to be a natural number type, rather than `Bool`

, `String`

, `String → Bool`

, etc.

In contrast to this difficulty with `pure`

, consider what if `n ≡ String`

in the type of `fmap`

:

`fmap ∷ (a → b) → Vec n a → Vec n b`

The definition of `Vec`

guarantees that that there are no values of type `Vec String a`

. So it's vacuously easy to cover that case (with an empty function). Similarly for `(⊛)`

.

If we were to somehow define `pure`

with the type given above, then `pure ()`

would have type `Vec String ()`

(among many other types). However, there are no values of that type. Hence, `pure`

cannot be defined without restricting `n`

.

Since the essential difficulty here is the unrestricted nature of `n`

, let's look at restricting it. We'll want to include exactly the types that can arise in constructing `Vec`

values, namely `Z`

, `S Z`

, `S (S Z)`

, `S (S (S Z))`

, etc.

As a first try, define a class with two instances:

`class IsNat n`

instance IsNat Z

instance IsNat n ⇒ IsNat (S n)

Then change the `Applicative`

instance to require `IsNat n`

:

`instance IsNat n ⇒ Applicative (Vec n) where`

⋯

The definition of `(⊛)`

given above still type-checks. Well, not quite. Really, the recursive call to `(⊛)`

fails to type-check, because the `IsNat`

constraint cannot be proved. One solution is to add that constraint to the vector type:

`data Vec ∷ * → * → * where`

ZVec ∷ Vec Z a

(:<) ∷ IsNat n ⇒ a → Vec n a → Vec (S n) a

Another is to break the definition `(⊛)`

out into a separate recursion that omits the `IsNat`

constraint:

`instance IsNat n ⇒ Applicative (Vec n) where`

pure = ???

(⊛) = applyV

applyV ∷ Vec n (a → b) → Vec n a → Vec n b

ZVec `applyV` ZVec = ZVec

(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)

Now, how can we define `pure`

? We still don't have enough structure. To get that structure, add a method to `IsNat`

. That method could simply be the definition of `pure`

that we need.

`class IsNat n where pureN ∷ a → Vec n a`

instance IsNat Z where pureN a = ZVec

instance IsNat n ⇒ IsNat (S n) where pureN a = a :< pureN a

To get this second instance to type-check, we'll have to add the constraint `IsNat n`

to the `(:<)`

constructor in `Vec`

. Then define `pure = pureN`

for `Vec`

.

I prefer a variation on this solution. Instead of `pureN`

, use a method that can only make vectors of `()`

:

`class IsNat n where units ∷ Vec n ()`

instance IsNat Z where units = ZVec

instance IsNat n ⇒ IsNat (S n) where units = () :< units

Then define

` pure a = fmap (const a) units`

Neat trick, huh? I got it from *Applicative Programming with Effects* (section 7).

### Value-typed natural numbers

There's still another way to define `IsNat`

, and it's the one I actually use.

Define a type of natural number with matching value & type:

`data Nat ∷ * → * where`

Zero ∷ Nat Z

Succ ∷ IsNat n ⇒ Nat n → Nat (S n)

Interpret a `Nat`

as an `Integer`

`natToZ ∷ Nat n → Integer`

natToZ Zero = 0

natToZ (Succ n) = (succ ∘ natToZ) n

I wrote the second clause strangely to emphasize the following lovely property, which corresponds to a simple commutative diagram:

`natToZ ∘ Succ = succ ∘ natToZ`

This `natToZ`

function is handy for showing natural numbers:

`instance Show (Nat n) where show = show ∘ natToZ`

A fun & strange thing about `Nat n`

is that it can have at most one inhabitant for any type `n`

. We can synthesize that inhabitant via an alternative definition of the `IsNat`

class defined (twice) above:

`class IsNat n where nat ∷ Nat n`

instance IsNat Z where nat = Zero

instance IsNat n ⇒ IsNat (S n) where nat = Succ nat

Using this latest version of `IsNat`

, we can easily define `units`

(and hence `pure`

on `Vec n`

for `IsNat n`

):

`units ∷ IsNat n ⇒ Vec n ()`

units = unitsN nat

unitsN ∷ Nat n → Vec n ()

unitsN Zero = ZVec

unitsN (Succ n) = () :< unitsN n

I prefer this latest `IsNat`

definition over the previous two, because it relies only on `Nat`

, which is simpler and more broadly useful than `Vec`

. Examples abound, including improving an recent post, as we'll see now.

### Revisiting type-bounded numbers

The post *Type-bounded numbers* defined a type `BNat n`

of natural numbers less than `n`

, which can be used, for instance, as numerical digits in base `n`

.

`data BNat ∷ * → * where`

BZero ∷ BNat (S n)

BSucc ∷ BNat n → BNat (S n)

One useful operation is conversion from integer to `BNat n`

. This operation had the awkward task of coming up with `BNat`

structure. The solution given was to introduce a type class, with instances for `Z`

and `S`

:

`class HasBNat n where toBNat ∷ Integer → Maybe (BNat n)`

instance HasBNat Z where toBNat _ = Nothing

instance HasBNat n ⇒ HasBNat (S n) where

toBNat m | m < 1 = Just BZero

| otherwise = fmap BSucc (toBNat (pred m))

We can instead eliminate the `HasBNat`

class and reuse the `IsNat`

class, as in the last technique above for defining `units`

or `pure`

.

`toBNat ∷ ∀ n. IsNat n ⇒ Integer → Maybe (BNat n)`

toBNat = loop n where

n = nat ∷ Nat n

loop ∷ Nat n' → Integer → Maybe (BNat n')

loop Zero _ = Nothing

loop (Succ _) 0 = Just BZero

loop (Succ n') m = fmap BSucc (loop n' (pred m))

### A Monad instance

First the easy parts: standard definitions in terms of `pure`

and `join`

:

`instance IsNat n ⇒ Monad (Vec n) where`

return = pure

v >>= f = join (fmap f v)

The `join`

function on `Vec n`

is just like `join`

for functions and for streams. (Rightly so, considering the principle of type class morphisms.) It uses diagonalization, and one way to think of vector `join`

is that it extracts the diagonal of a square matrix.

`join ∷ Vec n (Vec n a) → Vec n a`

join ZVec = ZVec

join (v :< vs) = headV v :< join (fmap tailV vs)

The `headV`

and `tailV`

functions are like `head`

and `tail`

but understand lengths:

`headV ∷ Vec (S n) a → a`

headV (a :< _) = a

`tailV ∷ Vec (S n) a → Vec n a`

tailV (_ :< as) = as

Unlike their list counterparts, `headV`

and `tailV`

are *safe*, in that the precondition of non-emptiness is verified statically.

## conal:

Maxime Henrion suggested an alternative to my

`Applicative`

instance above:I hadnâ€™t considered splitting the one instance into two. I like the simplicity of this solution, though I suspect the constraint

`Applicative (Vec n)`

would be cumbersome in practice. A small drawback of this version is that it requires the GHC language extensions`FlexibleInstances`

and`FlexibleContexts`

.Continuing on to

`Monad`

:In this case, I'm using the general

30 January 2011, 5:25 pm`join`

function on monads. The`Monad`

instances would be more elegant and perhaps more efficient if`join`

were a method on`Monad`

as has been proposed.## Mikael Bung:

Some time ago I tried to find a solution that didn’t require an extra restriction on the context. As far as I can tell the IsNat solution is the best (in the sense that you only need to carry around one context) you can do currently but Maximes solution together with http://hackage.haskell.org/trac/ghc/wiki/KindSystem looks like it would allow the compiler to convince itself that the Applicative instance exists for all possible Vec n.

31 January 2011, 5:16 am## Darius Jahandarie:

Or, whenever this gets finished…

Or something like that

31 January 2011, 9:35 am## Conal Elliott » Blog Archive » Reverse-engineering length-typed vectors:

[…] About « Doing more with length-typed vectors […]

31 January 2011, 9:53 am## Bas van Dijk:

Nice post Conal!

We should realy invent a name for this pattern where we have a “type level datatype” (like Z and S n), an isomorphic value level GADT (like Nat) and a class that provides an overloaded constructor for this GADT (like IsNat).

I used this same pattern in 3 places already:

I’m even thinking about using some CPP hackery to abstract the pattern.

31 January 2011, 11:41 am## Conal Elliott » Blog Archive » A trie for length-typed vectors:

[…] Doing more with length-typed vectors […]

31 January 2011, 10:27 pm## Eyal Lotem:

Everyone might already know this, but

`(<$) = fmap . const`

, so the above:`pure a = fmap (const a) units`

Can be written:

`pure a = a <$ units`

or:

6 February 2011, 1:15 pm`pure = (<$ units)`

## conal:

Thanks, Eyal. I had forgotten about

6 February 2011, 8:40 pm`(<$)`

.