PS

(Co)Yoneda reduction for free

(Co)Yoneda reduction

Yoneda lemmaの(co)endによる表現:

  •  Fa \cong \displaystyle\int _ r \mathcal{Set}(\mathcal{C}(r, a), Fr)
  •  Fa \cong \displaystyle\int ^ b Fb \times \mathcal{C}(a, b)

を、(co)Yoneda redunctionという(と思う)。

(Co)Yoneda reduction for free

(Co)Ends for free - PSとより、

  •  Fa \cong \displaystyle\int _ r \big( (r \rightarrow a) \rightarrow Fr ) \cong \forall _ r \big( (r \rightarrow a) \rightarrow Fr )
  •  Fa \cong \displaystyle\int ^ b (Fb, a \rightarrow b) \cong \exists _ b (Fb, a \rightarrow b)

Functor.(Co)Yoneda

上をHaskellで実装したのが、kan-extenstions

module Data.Functor.Contravariant.Yoneda
newtype Yoneda f a = Yoneda { runYoneda :: forall r. (r -> a) -> f r }
module Data.Functor.Contravariant.Coyoneda
data Coyoneda f a where
  Coyoneda :: (a -> b) -> f b -> Coyoneda f a

だと思われる。

参考文献