Cofree traversable functor

Cotra.hs

{-# LANGUAGE GADTs #-}
import Data.Functor.HCofree
import Data.Vec.Lazy
import Data.Fin
import Data.Type.Nat

data Cotra f a where
  Cotra :: SNat n -> f (Fin n) -> Vec n a -> Cotra f a

to :: Functor f => Cotra f a -> HCofree Traversable f a
to (Cotra _ fn v) = HCofree (\vb -> fmap (vb !) fn) v

cotraUnit :: Traversable f => f a -> Cotra f a
cotraUnit = cotraUnit -- see paper

from :: HCofree Traversable f a -> Cotra f a
from hf = case cotraUnit hf of
  Cotra n hfn v -> Cotra n (counit hfn) v