{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Kleisli
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- This is an attempt at the Kleisli category, and the construction
-- of an adjunction for each monad.
-----------------------------------------------------------------------------
module Data.Category.Kleisli where

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Monoidal
import qualified Data.Category.Adjunction as A


data Kleisli m a b where
  Kleisli :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b

kleisliId :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k a -> Kleisli m a a
kleisliId :: Monad m -> Obj k a -> Kleisli m a a
kleisliId Monad m
m Obj k a
a = Monad m -> Obj k a -> k a (m :% a) -> Kleisli m a a
forall m (k :: * -> * -> *) b a.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
Kleisli Monad m
m Obj k a
a (MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) m
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (Id k) m -> Obj k a -> k (Id k :% a) (m :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a)

-- | The category of Kleisli arrows.
instance Category (Kleisli m) where

  src :: Kleisli m a b -> Obj (Kleisli m) a
src (Kleisli Monad m
m Obj k b
_ k a (m :% b)
f) = Monad m -> Obj k a -> Obj (Kleisli m) a
forall m (k :: * -> * -> *) a.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj k a -> Kleisli m a a
kleisliId Monad m
m (k a (m :% b) -> Obj k a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a (m :% b)
f)
  tgt :: Kleisli m a b -> Obj (Kleisli m) b
tgt (Kleisli Monad m
m Obj k b
b k a (m :% b)
_) = Monad m -> Obj k b -> Obj (Kleisli m) b
forall m (k :: * -> * -> *) a.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj k a -> Kleisli m a a
kleisliId Monad m
m Obj k b
b

  (Kleisli Monad m
m Obj k c
c k b (m :% c)
f) . :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c
. (Kleisli Monad m
_ Obj k b
_ k a (m :% b)
g) = Monad m -> Obj k c -> k a (m :% c) -> Kleisli m a c
forall m (k :: * -> * -> *) b a.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
Kleisli Monad m
m Obj k c
c ((MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (EndoFunctorCompose k :% (m, m)) m
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (m :.: m) m -> Obj k c -> k ((m :.: m) :% c) (m :% c)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k c
c) k (m :% (m :% c)) (m :% c) -> k a (m :% (m :% c)) -> k a (m :% c)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Monad m -> m
forall f. Monad f -> f
monadFunctor Monad m
m m -> Dom m b (m :% c) -> Cod m (m :% b) (m :% (m :% c))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k b (m :% c)
Dom m b (m :% c)
f) k (m :% b) (m :% (m :% c)) -> k a (m :% b) -> k a (m :% (m :% c))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a (m :% b)
g)



newtype KleisliFree m = KleisliFree (Monad m)
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliFree m) where
  type Dom (KleisliFree m) = Dom m
  type Cod (KleisliFree m) = Kleisli m
  type KleisliFree m :% a = a
  KleisliFree Monad m
m % :: KleisliFree m
-> Dom (KleisliFree m) a b
-> Cod (KleisliFree m) (KleisliFree m :% a) (KleisliFree m :% b)
% Dom (KleisliFree m) a b
f = Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
forall m (k :: * -> * -> *) b a.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
Kleisli Monad m
m (k a b -> Obj k b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
Dom (KleisliFree m) a b
f) ((MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) m
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (Id k) m -> Obj k b -> k (Id k :% b) (m :% b)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! k a b -> Obj k b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
Dom (KleisliFree m) a b
f) k b (m :% b) -> k a b -> k a (m :% b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a b
Dom (KleisliFree m) a b
f)

data KleisliForget m = KleisliForget
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliForget m) where
  type Dom (KleisliForget m) = Kleisli m
  type Cod (KleisliForget m) = Dom m
  type KleisliForget m :% a = m :% a
  KleisliForget m
KleisliForget % :: KleisliForget m
-> Dom (KleisliForget m) a b
-> Cod
     (KleisliForget m) (KleisliForget m :% a) (KleisliForget m :% b)
% Kleisli m b f = (MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (EndoFunctorCompose k :% (m, m)) m
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (m :.: m) m -> k b b -> k ((m :.: m) :% b) (m :% b)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! k b b
b) k (m :% (m :% b)) (m :% b)
-> k (m :% a) (m :% (m :% b)) -> k (m :% a) (m :% b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Monad m -> m
forall f. Monad f -> f
monadFunctor Monad m
m m -> Dom m a (m :% b) -> Cod m (m :% a) (m :% (m :% b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k a (m :% b)
Dom m a (m :% b)
f)

kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
  => Monad m -> A.Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
kleisliAdj :: Monad m
-> Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
kleisliAdj Monad m
m = KleisliFree m
-> KleisliForget m
-> (forall a.
    Obj k a -> Component (Id k) (KleisliForget m :.: KleisliFree m) a)
-> (forall a b.
    Obj (Kleisli m) b
    -> k a (KleisliForget m :% b) -> Kleisli m (KleisliFree m :% a) b)
-> Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
A.mkAdjunctionUnit (Monad m -> KleisliFree m
forall m. Monad m -> KleisliFree m
KleisliFree Monad m
m) KleisliForget m
forall m. KleisliForget m
KleisliForget (MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) m
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (Id k) m -> Obj k a -> k (Id k :% a) (m :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!) (\(Kleisli _ x _) k a (KleisliForget m :% b)
f -> Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
forall m (k :: * -> * -> *) b a.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
Kleisli Monad m
m Obj k b
x k a (KleisliForget m :% b)
k a (m :% b)
f)