Skip to content

Instantly share code, notes, and snippets.

@kl0tl
Last active August 15, 2017 11:51
Show Gist options
  • Save kl0tl/c224c4a08917af0f0ec55eb25ba3243d to your computer and use it in GitHub Desktop.
Save kl0tl/c224c4a08917af0f0ec55eb25ba3243d to your computer and use it in GitHub Desktop.
Kan Extensions!
:set -i.
{-# LANGUAGE TypeOperators, MultiParamTypeClasses #-}
module Adjunctions where
class (Functor l, Functor r) => l ⊣ r where
unit :: d -> r (l d)
unit = leftAdjunct id
counit :: l (r c) -> c
counit = rightAdjunct id
leftAdjunct :: (l d -> c) -> d -> r c
leftAdjunct f = fmap f . unit
rightAdjunct :: (d -> r c) -> l d -> c
rightAdjunct f = counit . fmap f
{-# MINIMAL leftAdjunct, rightAdjunct | unit, counit |
leftAdjunct, counit | unit, rightAdjunct #-}
{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, DeriveFunctor #-}
module Codensity where
import Adjunctions
import Compose
import Identity
import MonoidalCategory2
import Nat
import Ran
newtype Codensity k a = Codensity (Ran k k a)
deriving Functor
runCodensity (Codensity (Ran akk)) = akk
codensityToRan (Codensity ran) = ran
instance Functor k => Applicative (Codensity k) where
pure = return
mab <*> ma = mab >>= (`fmap` ma)
instance Functor k => Monad (Codensity k) where
return a = Codensity (Ran (\ak -> ak a))
(Codensity (Ran akk)) >>= abkk = Codensity (Ran bkk)
where bkk bk = akk (\a -> (runCodensity . abkk $ a) bk)
class Abs_Ran k d where
abs_Ran :: Ran k (Compose f d) ~> Compose f (Ran k d)
instance (Functor k, Abs_Ran k Id) => (Ran k Id) ⊣ k where
unit = decompose . abs_Ran . (rotate_Ran ρ') . codensityToRan . return
counit = runIdentity . counit_Ran . Compose
module Comonad where
class Functor w => Comonad w where
extract :: w a -> a
extend :: w a -> (w a -> b) -> w b
{-# LANGUAGE MultiParamTypeClasses #-}
module Compose where
import Identity
import MonoidalCategory2
newtype Compose f g a = Compose { decompose :: (f (g a)) }
instance MonoidalCategory2 Compose Id where
λ = runIdentity . decompose
λ' = Compose . Id
ρ = fmap runIdentity . decompose
ρ' = Compose . fmap Id
α = Compose . fmap Compose . decompose . decompose
α' = Compose . Compose . fmap decompose . decompose
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}
module Coyoneda where
import Nat
data Coyoneda f a = forall x. Coyoneda (x -> a) (f x)
instance Functor (Coyoneda f) where
fmap ab (Coyoneda xa fx) = Coyoneda (ab . xa) fx
fromCoyoneda :: Functor f => Coyoneda f ~> f
fromCoyoneda (Coyoneda xa fx) = xa <$> fx
toCoyoneda :: f ~> Coyoneda f
toCoyoneda fa = Coyoneda id fa
{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, DeriveFunctor #-}
module Density where
import Adjunctions
import Comonad
import Compose
import Identity
import Lan
import MonoidalCategory2
import Nat
newtype Density k a = Density (Lan k k a)
deriving Functor
instance Functor k => Comonad (Density k) where
extract (Density (Lan ka k)) = ka k
extend (Density (Lan ka k)) kakb = Density (Lan kb k)
where kb k' = kakb (Density (Lan ka k'))
class Abs_Lan k d where
abs_Lan :: Compose f (Lan k d) ~> Lan k (Compose f d)
instance (Functor k, Abs_Lan k Id) => k ⊣ (Lan k Id) where
unit = decompose . unit_Lan . Id
counit = extract . Density . (rotate_Lan ρ) . abs_Lan . Compose
{-# LANGUAGE DeriveFunctor #-}
module Identity where
newtype Id a = Id { runIdentity :: a }
deriving Functor
{-# LANGUAGE ExistentialQuantification, TypeOperators, RankNTypes #-}
module Lan where
import Adjunctions
import Compose
import Coyoneda
import Identity
import Nat
data Lan k d a = forall i. Lan (k i -> a) (d i)
instance Functor (Lan k d) where
fmap ab (Lan ka d) = Lan (ab . ka) d
unit_Lan :: d ~> Compose (Lan k d) k
unit_Lan da = Compose (Lan id da)
rotate_Lan :: (d ~> d') -> Lan k d ~> Lan k d'
rotate_Lan nat (Lan ka d) = Lan ka (nat d)
lanToCoyoneda :: Lan Id d ~> Coyoneda d
lanToCoyoneda (Lan idia di) = Coyoneda (idia . Id) di
coyonedaToLan :: Coyoneda d ~> Lan Id d
coyonedaToLan (Coyoneda xa fx) = Lan (xa . runIdentity) fx
-- K ⊣ Lan_K Id
adjointToLan :: (l ⊣ r) => r ~> Lan l Id
adjointToLan = Lan counit . Id
lanToAdjoint :: (l ⊣ r) => Lan l Id ~> r
lanToAdjoint (Lan lia idi) = fmap lia . unit . runIdentity $ idi
{-# LANGUAGE TypeOperators, MultiParamTypeClasses #-}
module MonoidalCategory2 where
import Nat
class Functor i => MonoidalCategory2 tensor i where
λ :: Functor f => (i `tensor` f) ~> f
λ' :: Functor f => f ~> (i `tensor` f)
ρ :: Functor f => (f `tensor` i) ~> f
ρ' :: Functor f => f ~> (f `tensor` i)
α :: (Functor f, Functor g, Functor h) =>
((f `tensor` g) `tensor` h) ~> (f `tensor` (g `tensor` h))
α' :: (Functor f, Functor g, Functor h) =>
(f `tensor` (g `tensor` h)) ~> ((f `tensor` g) `tensor` h)
{-# LANGUAGE RankNTypes, TypeOperators #-}
module Nat where
type f ~> g = forall a. f a -> g a
{-# LANGUAGE RankNTypes, TypeOperators, DeriveFunctor #-}
module Ran where
import Adjunctions
import Compose
import Identity
import Nat
import Yoneda
newtype Ran k d a = Ran (forall i. (a -> k i) -> d i)
deriving Functor
counit_Ran :: Compose (Ran k d) k ~> d
counit_Ran (Compose (Ran f)) = f id
rotate_Ran :: (d ~> d') -> Ran k d ~> Ran k d'
rotate_Ran nat (Ran akd) = Ran (nat . akd)
ranToYoneda :: Functor d => Ran Id d ~> Yoneda d
ranToYoneda (Ran aididi) = Yoneda (<$> aididi Id)
yonedaToRan :: Functor d => Yoneda d ~> Ran Id d
yonedaToRan yo = Ran (\aidi -> runIdentity . aidi <$> fromYoneda yo)
-- Ran_K Id ⊣ K
adjointToRan :: (l ⊣ r) => l ~> Ran r Id
adjointToRan l = Ran (\ari -> Id . counit . fmap ari $ l)
ranToAdjoint :: (l ⊣ r) => Ran r Id ~> l
ranToAdjoint (Ran arid) = runIdentity $ arid unit
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveFunctor #-}
module Yoneda where
import Nat
newtype Yoneda f a = Yoneda { runYoneda :: forall x. (a -> x) -> f x }
deriving Functor
fromYoneda :: Yoneda f ~> f
fromYoneda = ($id) . runYoneda
toYoneda :: Functor f => f ~> Yoneda f
toYoneda fa = Yoneda (`fmap` fa)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment