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.