{-# 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 :: 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 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 (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit Monad m
m 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 :: forall a b. Kleisli m a b -> Obj (Kleisli m) a
src (Kleisli Monad m
m Obj k b
_ k a (m :% b)
f) = 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 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a (m :% b)
f)
  tgt :: forall a b. Kleisli m a b -> Obj (Kleisli m) b
tgt (Kleisli Monad m
m Obj k b
b k a (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) . :: forall b c a. Kleisli m b c -> Kleisli m a b -> Kleisli m a c
. (Kleisli Monad m
_ Obj k b
_ k a (m :% b)
g) = 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 ((forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply Monad m
m 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) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall f. Monad f -> f
monadFunctor Monad m
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k b (m :% c)
f) 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 % :: forall a b.
KleisliFree m
-> Dom (KleisliFree m) a b
-> Cod (KleisliFree m) (KleisliFree m :% a) (KleisliFree m :% b)
% Dom (KleisliFree m) a b
f = 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 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (KleisliFree m) a b
f) ((forall f a. MonoidObject f a -> Cod f (Unit f) a
unit Monad m
m forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (KleisliFree m) a b
f) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. 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 % :: forall a b.
KleisliForget m
-> Dom (KleisliForget m) a b
-> Cod
     (KleisliForget m) (KleisliForget m :% a) (KleisliForget m :% b)
% Kleisli Monad m
m Obj k b
b k a (m :% b)
f = (forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply Monad m
m 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 b
b) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall f. Monad f -> f
monadFunctor Monad m
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k 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 :: forall m (k :: * -> * -> *).
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m
-> Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
kleisliAdj Monad m
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 -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
A.mkAdjunctionInit (forall m. Monad m -> KleisliFree m
KleisliFree Monad m
m) forall m. KleisliForget m
KleisliForget (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit Monad m
m 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 Monad m
_ Obj k b
x k b (m :% b)
_) k a (KleisliForget m :% b)
f -> 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)
f)