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