The Cont adjunction

Adjunction.hs

{-# 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!")))