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.