Skip to content

Instantly share code, notes, and snippets.

@kl0tl
Last active August 14, 2017 22:44
Show Gist options
  • Save kl0tl/87d9eecc7f7db585f10dce905f71f6e6 to your computer and use it in GitHub Desktop.
Save kl0tl/87d9eecc7f7db585f10dce905f71f6e6 to your computer and use it in GitHub Desktop.
Yoneda!
:set -i.
module Contravariant where
class Contravariant f where
contramap :: (b -> a) -> f a -> f b
{-# 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
{-# 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
{-# 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
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment