Skip to content

N_P3Ch11a_KanExt

Jump to bottom
rpeszek edited this page Apr 20, 2018 · 7 revisions

Markdown of literate Haskell program. Program source: /src/CTNotes/P3Ch11a_KanExt.lhs

Notes about CTFP Part 3 Chapter 11. Kan Extensions

This note covers:

  • Haskell (simplified) derivations of Ran and Lan.
  • Similarities of Codensity, ContT, Yoneda.
  • Example of calculating adjunctions.
  • That beautiful argument about how Yoneda creates functors for free using Haskell code.

Book Ref: https://bartoszmilewski.com/2017/04/17/kan-extensions/

Refs:
http://comonad.com/reader/2011/free-monads-for-less/
http://comonad.com/reader/2011/free-monads-for-less-2/
http://comonad.com/reader/2011/free-monads-for-less-3/
http://comonad.com/reader/2008/kan-extensions/
http://comonad.com/reader/2008/kan-extensions-ii/
http://comonad.com/reader/2008/kan-extension-iii/

 {-# LANGUAGE Rank2Types
       , ExistentialQuantification
       , KindSignatures, PolyKinds
       , TypeOperators
       , MultiParamTypeClasses
       , FunctionalDependencies
       , FlexibleInstances
 #-}
 module CTNotes.P3Ch11a_KanExt where
 import Control.Monad
 import CTNotes.P3Ch09a_Talg

Ran, Haskell derivation

Haskell formula for Ran (right Kan extension):

 newtype Ran k d a = Ran (forall i. (a -> k i) -> d i)

Here is this how this formula is derived from the right Kan adjunction (Ran is right-adjunct of functor composition)

        
                 [I, C]          [A, C]
                          - ∘ K
                 F' ∘ K <--------  F'
                    |              |
  [I, C](F' ∘ K, D) |              |  [A, C](F', Ran_K D)
                   \ /            \ /
                    D  ---------> Ran_K D
                         Ran_K -

[I, C](F' ∘ K, D) ≅ [A, C](F', Ran_K D)

Pseudo-Haskell representation of the above diagram is

forall ix. f (k ix) -> d ix     ≅ forall ax. f ax -> Ran k d ax

take f = (a ->)

forall ix. (a -> k ix) -> d ix  ≅ forall ax. (a -> ax) -> Ran k d ax

and apply Yoneda lemma on RHS

forall ix. (a -> k ix) -> d ix  ≅ Ran k d a

So, Haskell Ran is basically Ran adjunction specialized to the hom functor with Yoneda lemma applied.

Q: For non-Hask categories (as in N_P1Ch03b_FiniteCats) it makes sense to consider (assuming homsetA implementing Control.Category, I is non-Hask, A is non-Hask, and C = Hask))

 newtype CRan (homsetA:: ka -> ka -> *) (k:: ki -> ka) (d::ki -> *) (a:: ka) = 
    CRan (forall i. (a `homsetA` (k i)) -> d i)

A: there are 2 problems, first: Yoneda lemma is no longer that simple (N_P2Ch05b_YonedaNonHask), second: we no longer have free theorems for naturality condition N_P1Ch10b_NTsNonHask. So the above derivation no longer holds.

Lan, Haskell derivation

Haskell formula for Lan.

 data Lan k d a = forall i. Lan (k i -> a) (d i)

Following a more general derivation in the book, to verify this formula, I need to show that this is indeed the left adjoint to functor composition

                 [A, C]          [I, C]
                         Lan_K -
                Lan_K D <--------  D
                    |              |
  [I, C](F ∘ K, D)  |              |  [A, C](F, Ran_K D)
                   \ /            \ /
                    F  ---------> F ∘ K
                         - ∘ K

 [A, Set](Lan_K D, F) ≅ [I, Set](D, F'∘ K)

or, in psedo-Haskell:

forall ax. Lan k d ax -> f ax  ≅  forall ix. d ix -> f (k ix)

forall ax. Lan k d ax -> f ax 
-- from definition 
≅ forall ax. forall i. Lan (k i -> ax) (d i) -> f ax 
-- currying LHS
≅ forall ax. forall i. (k i -> ax) -> (d i -> f ax)   
-- swapping universal quantification 
≅ forall i. forall ax. (k i -> ax) -> (d i -> f ax)     
-- Yoneda applied to inner forall (replaces ax with k i)
≅ forall i. d i -> f (k i)

Codensity, ContT, Yoneda

Are all related to Kan extensions!

Kan extensions have almost universal importance and applicability. Quoting Ch 15: "There is a saying that all concepts are Kan extensions and, indeed, you can use Kan extensions to derive limits, colimits, adjunctions, monads, the Yoneda lemma, and much more."

This part of the note follows the above commonad post to explore similarities between Codensity, and ContT, and Yoneda type constructors.

 newtype Codensity d a = Codensity {runCodensity :: forall i. (a -> d i) -> d i}

compare to

 newtype ContT k r m a = ContT {runContT :: (a -> m r) -> m r}

and to (see N_P2Ch05a_YonedaAndMap)

newtype Yoneda d a = Yoneda (forall i. (a -> i) -> d i)

Codensity is equivalent to Ran d d, Yoneda d is Ran id d.
Similarly to ContT Codensity d is always a Monad (for any type constructor d).

 instance Functor (Codensity k) where
   fmap f (Codensity m) = Codensity (\k -> m (k . f))
 instance Monad (Codensity f) where
  return x = Codensity (\k -> k x)
  m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))
 instance Applicative (Codensity f) where
   pure  = return
   (<*>) = ap
instance MonadTrans Codensity where
   lift m = Codensity (m >>=)

ContT and Codensity both yield a result in which all of the uses of the underlying monad's (>>=) are right associated. That makes Codensity useful in improving asymptotic complexity of Free monads.

A very interesting fact is that Codensity ((->) s) a is isomorphic to State s a

 class Monad m => MonadState s m | m -> s where
   get :: m s
   get = state (\s -> (s, s))
   put :: s -> m ()
   put s = state (\_ -> ((), s))
   state :: (s -> (a, s)) -> m a
   state f = do
          s <- get
          let ~(a, s') = f s
          put s'
          return a

 instance MonadState s (Codensity ((->) s)) where
    get = Codensity (\k s -> k s s)
    put s = Codensity (\k _ -> k () s)

Calculating Adjunctions

Adjunctions can be calculated with help of the following formula

-- Ran_K I_C ⊣ K ⊣ Lan_K I_C

Ran K Identity ⊣ K ⊣ Lan K Identity
Ran (forall i. (a -> k i) -> i)  ⊣ K ⊣ forall i. Lan (k i -> a) i

For Curry adjunction (-, a) ⊣ a -> - the book computes Lan ((,) a) Identity b and shows that it is isomorphic to a -> b.

Using the Ran against (->) a is even simpler

Ran ((->) a) Identity b
-- definition
= Ran (forall i. (b -> (a -> i)) -> i)
-- curry
≅ Ran (forall i. ((b, a) -> i) -> i)
≅ (b, a)

Yoneda and Functors for Free

A beautiful example of programming with categorical thinking from the book.
Non-functor data constructor D are functors from the corresponding discrete category, using book notation, call it, |Hask|

 A=Hask  
  / \     \
K  |       \  Ran_K D
   |        \/ 
I=|Hask| --> C=Hask
         D

K is the natural embedding of |Hask| into Hask.
Remember, we have

Ran_K D a ≅ ∫_i Set(A(a, K i), D i)

which translates (since A=Hask) to the same Ran definition:

newtype Ran k d a = Ran (forall i. (a -> k i) -> d i)

and since K is just type level Identity, this is equivalent to (using FreeF name from the book)

newtype FreeF d a = RanF (forall i. (a -> i) -> d i)

which is really (see the definition above)

newtype Yoneda d a = Yoneda (forall i. (a -> i) -> d i)

That explains why Yoneda creates monads for Free.

Similarly (see N_P2Ch05a_YonedaAndMap)

data CoYoneda f a = forall x. CoYoneda (x -> a) (f x)

is isomorphic to the type derived in the book using Lan_K D approach

data FreeF f a = forall i. FMap (i -> a) (f i)
Clone this wiki locally