Yoneda!

.ghci

:set -i.

Contravariant.hs

module Contravariant where

class Contravariant f where
  contramap :: (b -> a) -> f a -> f b

ContravariantCoyoneda.hs

{-# LANGUAGE ExistentialQuantification #-}

module ContravariantCoyoneda where
import Contravariant

data Coyoneda f a = forall b. Coyoneda (a -> b) (f b)
instance Contravariant (Coyoneda f) where
  contramap f (Coyoneda g fb) = Coyoneda (g . f) fb

toCoyoneda :: f a -> Coyoneda f a
toCoyoneda fa = Coyoneda id fa

fromCoyoneda :: Contravariant f => Coyoneda f a -> f a
fromCoyoneda (Coyoneda f fb) = contramap f fb

ContravariantYoneda.hs

{-# LANGUAGE Rank2Types, TypeOperators #-}

module ContravariantYoneda where
import Contravariant

type f ~> g = forall a. f a -> g a
type Op a b = b -> a

-- Nat(Hom(-, a), F) ≣ F a
newtype Yoneda f a = Yoneda (Op a ~> f)
instance Contravariant (Yoneda f) where
  contramap f (Yoneda yo) = Yoneda $ \g -> yo $ f . g

toYoneda :: Contravariant f => f a -> Yoneda f a
toYoneda fa = Yoneda $ \f -> contramap f fa

fromYoneda :: (Contravariant f) => Yoneda f a -> f a
fromYoneda (Yoneda yo) = yo id

-- Nat(Hom(-, a), Hom(-, b)) ≣ Hom(a, b)
type Embedding a b = Op a ~> Op b

embed :: (a -> b) -> Embedding a b
embed = (.)

unembed :: Embedding a b -> (a -> b)
unembed nat = nat id

Coyoneda.hs

{-# LANGUAGE ExistentialQuantification #-}

module Coyoneda where

data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)
instance Functor (Coyoneda f) where
  fmap f (Coyoneda g fb) = Coyoneda (f . g) fb

toCoyoneda :: f a -> Coyoneda f a
toCoyoneda fa = Coyoneda id fa

fromCoyoneda :: Functor f => Coyoneda f a -> f a
fromCoyoneda (Coyoneda f fb) = fmap f fb

Yoneda.hs

{-# LANGUAGE Rank2Types, TypeOperators #-}

module Yoneda where

type f ~> g = forall a. f a -> g a
type Reader a b = a -> b

-- Nat(Hom(a, -), F) ≣ F a
newtype Yoneda f a = Yoneda (Reader a ~> f)
instance Functor (Yoneda f) where
  fmap f (Yoneda yo) = Yoneda $ \g -> yo $ g . f

toYoneda :: Functor f => f a -> Yoneda f a
toYoneda fa = Yoneda $ \f -> fmap f fa

fromYoneda :: Yoneda f a -> f a
fromYoneda (Yoneda yo) = yo id

-- Nat(Hom(a, -), Hom(b, -)) ≣ Hom(b, a)
type Embedding a b = Reader a ~> Reader b

embed :: (b -> a) -> Embedding a b
embed = flip (.)

unembed :: Embedding a b -> (b -> a)
unembed nat = nat id