Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Created Apr 17, 2020
Embed
What would you like to do?
The Cont adjunction
{-# LANGUAGE
TypeOperators, -- Type-level infix operators, here (<-:)
PolyKinds, -- Kind-polymorphic classes. (You can also instantiate all k and h to Type)
ScopedTypeVariables, -- Extend the scope of type variables to the body of a function
InstanceSigs, -- Type signatures on instance methods
MultiParamTypeClasses, -- Self-explanatory
FlexibleContexts, -- Allows constraints like (Adjunction (->) d f g) where the first argument is not a type variable
AllowAmbiguousTypes, -- unit and counit each don't mention one of the type class parameters
TypeApplications -- To use functions with ambiguous types
-- How unexpected is it that comments are allowed inside pragmas?
#-}
module Adjunction where
import Control.Category (Category, (>>>))
import qualified Control.Category as Category
import Data.Kind (Type)
-- This name is a pun for symmetry:
--
-- Haskell | Category theory
-- ----------------------------------------------
-- Functor | Endofunctor (on Hask)
-- Exofunctor | Functor
class Exofunctor c d f where
exomap :: c a b -> d (f a) (f b)
newtype (<-:) a b = Co { unCo :: b -> a }
instance Exofunctor (->) (<-:) ((<-:) r) where
exomap :: (a -> b) -> ((r <-: a) <-: (r <-: b))
exomap f = Co (\(Co g) -> Co (g . f))
instance Exofunctor (<-:) (->) ((<-:) r) where
exomap :: (a <-: b) -> ((r <-: a) -> (r <-: b))
exomap (Co f) (Co g) = Co (g . f)
-- An adjunction f -| g between categories c and d is a pair of functors
--
-- f from d to c
-- g from c to d
--
-- with 'unit' and 'counit' satisfying some laws.
class
(Exofunctor d c f, Exofunctor c d g) =>
Adjunction
(c :: k -> k -> Type)
(d :: h -> h -> Type)
(f :: h -> k)
(g :: k -> h) where
unit :: d a (g (f a))
counit :: c (f (g a)) a
instance Adjunction (<-:) (->) ((<-:) r) ((<-:) r) where
unit x = Co (\(Co k) -> k x)
counit = Co (unit @_ @_ @(<-:) @(->))
-- They're not an adjunction the other way around (Adjunction (->) (<-:))!
--
-- That's because we cannot define counit :: ((a -> r) -> r) -> a
-- The composition of adjoint functors is a monad or a comonad (depending on which way it goes)
newtype Compose f g a = Compose { unCompose :: f (g a) }
-- Monad = return + join
adjReturn :: forall c f g a. Adjunction c (->) f g => a -> Compose g f a
adjReturn = Compose . unit @_ @_ @c @(->)
-- ^^^^ important part (return = unit is the textbook version)
--
-- The rest with Compose is newtype fluff which doesn't appear in category
-- theory textbooks because it is a detail specific to this encoding in
-- Haskell.
adjJoin :: forall c f g a. Adjunction c (->) f g => Compose g f (Compose g f a) -> Compose g f a
adjJoin = Compose . exomap (counit @_ @_ @c @(->)) . (exomap . exomap @(->) @c) unCompose . unCompose
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ important part (join = exomap counit)
-- Comonad = extract + duplicate
adjExtract :: forall d f g a. Adjunction (->) d f g => Compose f g a -> a
adjExtract = counit @_ @_ @(->) @d . unCompose
adjDuplicate :: forall d f g a. Adjunction (->) d f g => Compose f g a -> Compose f g (Compose f g a)
adjDuplicate = Compose . (exomap . exomap @(->) @d) Compose . exomap (unit @_ @_ @(->) @d) . unCompose
-- The continuation monad as an adjunction:
type Cont r = Compose ((<-:) r) ((<-:) r)
runCont :: Cont r r -> r
runCont (Compose (Co f)) = f (Co id)
main :: IO ()
main = putStrLn (runCont $ adjJoin @(<-:) (adjReturn @(<-:) (adjReturn @(<-:) "Hello World!")))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment