Lists are not representable, but vectors are.

RepresentableVec.hs

{-# LANGUAGE GADTs, KindSignatures, TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, StandaloneDeriving #-}

import Control.Applicative
import Control.Arrow
import Data.Key
import Data.Distributive
import Data.Functor.Bind
import Data.Functor.Representable
import Data.Functor.Adjunction

import Control.Monad.State.Class
import Control.Monad.Trans.Adjoint
import Control.Comonad
import qualified Control.Comonad.Trans.Adjoint as Co


data Z
data S n

data Fin :: * -> * where
  Fz ::          Fin (S n)
  Fs :: Fin n -> Fin (S n)

data Vec :: * -> * -> * where
  Nil  ::                 Vec  Z    a
  Cons :: a -> Vec n a -> Vec (S n) a

type instance Key (Vec n) = Fin n

instance Indexable (Vec Z) where
  index Nil i = i `seq` error "We never get this far"
instance Indexable (Vec n) => Indexable (Vec (S n)) where
  index (Cons a _ )  Fz    = a
  index (Cons _ as) (Fs i) = index as i

instance                          Lookup        (Vec  Z   ) where lookup = lookupDefault
instance Indexable     (Vec n) => Lookup        (Vec (S n)) where lookup = lookupDefault

instance Representable (Vec Z) where
  tabulate _ = Nil
instance Representable (Vec n) => Representable (Vec (S n)) where
  tabulate f = Cons (f Fz) (tabulate (f . Fs))

instance                          Functor       (Vec  Z   ) where fmap = fmapRep
instance Representable (Vec n) => Functor       (Vec (S n)) where fmap = fmapRep
instance                          Keyed         (Vec  Z   ) where mapWithKey = mapWithKeyRep
instance Representable (Vec n) => Keyed         (Vec (S n)) where mapWithKey = mapWithKeyRep
instance                          Distributive  (Vec  Z   ) where distribute = distributeRep
instance Representable (Vec n) => Distributive  (Vec (S n)) where distribute = distributeRep
instance                          Apply         (Vec  Z   ) where (<.>) = apRep
instance Representable (Vec n) => Apply         (Vec (S n)) where (<.>) = apRep
instance                          Applicative   (Vec  Z   ) where { pure = pureRep; (<*>) = apRep }
instance Representable (Vec n) => Applicative   (Vec (S n)) where { pure = pureRep; (<*>) = apRep }



data Numbered n a = Numbered (Fin n) a

instance Representable (Vec n) => Functor (Numbered n) where fmap = fmapAdjunction

instance Representable (Vec n) => Adjunction (Numbered n) (Vec n) where
  leftAdjunct f a = tabulate (\i -> f (Numbered i a))
  rightAdjunct f (Numbered i a) = index (f a) i

fmapAdjunction :: Adjunction f u => (a -> b) -> f a -> f b
fmapAdjunction f = rightAdjunct (unit . f)

split :: Adjunction f u => f a -> (a, f ())
split = rightAdjunct (flip leftAdjunct () . (,))


instance (Adjunction f g, Monad m) => MonadState (f ()) (AdjointT f g m) where
  get = AdjointT $ leftAdjunct (\s -> return (fmap (const s) s)) ()
  put = AdjointT . pure . return

-- instance (Adjunction f g, Comonad w) => ComonadStore (f ()) (Co.AdjointT f g w) where
pos :: Adjunction f g => Co.AdjointT f g w a -> f ()
pos = snd . split . Co.runAdjointT

peeks :: (Adjunction f g, Comonad w) => (f () -> f ()) -> Co.AdjointT f g w a -> a
peeks f = uncurry indexAdjunction . (extract *** f) . split . Co.runAdjointT



instance Show (Fin Z) where
  show i = i `seq` error "We never get this far"
instance Show (Fin n) => Show (Fin (S n)) where
  show Fz = "Fz"
  show (Fs i) = "(Fs " ++ show i ++ ")"
instance Show (Vec Z a) where
  show Nil = "Nil"
instance (Show a, Show (Vec n a)) => Show (Vec (S n) a) where
  show (Cons a as) = "(Cons " ++ show a ++ " " ++ show as ++ ")"
deriving instance (Show a, Show (Fin n)) => Show (Numbered n a)