{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Control.Category.FreeEffect
  ( EffectCategory (..)
  , EffCat (..)
  , liftEffect
  , foldNatEffCat
  , runEffCat
  , liftKleisli
  ) where

import Prelude hiding (id, (.))

import Control.Arrow (Kleisli (..))
import Control.Category (Category (..))
import Data.Functor.Identity (Identity (..))
import Data.Kind (Type)

import Control.Algebra.Free2 (FreeAlgebra2 (..))
import Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..))


-- | Categories which can lift monadic actions, i.e effectful categories.
--
class Category c => EffectCategory c m | c -> m where
  effect :: m (c a b) -> c a b

instance Monad m => EffectCategory (Kleisli m) m where
  effect :: forall a b. m (Kleisli m a b) -> Kleisli m a b
effect m (Kleisli m a b)
m = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (\a
a -> m (Kleisli m a b)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Kleisli a -> m b
f) -> a -> m b
f a
a)

instance EffectCategory (->) Identity where
  effect :: forall a b. Identity (a -> b) -> a -> b
effect = forall a. Identity a -> a
runIdentity

-- | Category transformer, which adds @'EffectCategory'@ instance to the
-- underlying base category.
--
data EffCat :: (Type -> Type) -> (k -> k -> Type) -> k -> k -> Type where
  Base   :: c a b -> EffCat m c a b
  Effect :: m (EffCat m c a b) -> EffCat m c a b

instance (Functor m, Category c) => Category (EffCat m c) where
  id :: forall (a :: k). EffCat m c a a
id = forall {k} (c :: k -> k -> *) (a :: k) (b :: k) (m :: * -> *).
c a b -> EffCat m c a b
Base forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  Base c b c
f    . :: forall (b :: k) (c :: k) (a :: k).
EffCat m c b c -> EffCat m c a b -> EffCat m c a c
. Base c a b
g    = forall {k} (c :: k -> k -> *) (a :: k) (b :: k) (m :: * -> *).
c a b -> EffCat m c a b
Base   forall a b. (a -> b) -> a -> b
$ c b c
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c a b
g
  EffCat m c b c
f         . Effect m (EffCat m c a b)
mg = forall {k} (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
m (EffCat m c a b) -> EffCat m c a b
Effect forall a b. (a -> b) -> a -> b
$ (EffCat m c b c
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (EffCat m c a b)
mg
  Effect m (EffCat m c b c)
mf . EffCat m c a b
g         = forall {k} (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
m (EffCat m c a b) -> EffCat m c a b
Effect forall a b. (a -> b) -> a -> b
$ (forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. EffCat m c a b
g) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (EffCat m c b c)
mf

instance (Functor m, Category c) => EffectCategory (EffCat m c) m where
  effect :: forall (a :: k) (b :: k). m (EffCat m c a b) -> EffCat m c a b
effect = forall {k} (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
m (EffCat m c a b) -> EffCat m c a b
Effect

type instance AlgebraType0 (EffCat m) c = (Monad m, Category c)
type instance AlgebraType  (EffCat m) c  = EffectCategory c m
instance Monad m => FreeAlgebra2 (EffCat m) where
  liftFree2 :: forall (f :: k -> k -> *) (a :: k) (b :: k).
AlgebraType0 (EffCat m) f =>
f a b -> EffCat m f a b
liftFree2    = forall {k} (c :: k -> k -> *) (a :: k) (b :: k) (m :: * -> *).
c a b -> EffCat m c a b
Base
  foldNatFree2 :: forall (d :: k -> k -> *) (f :: k -> k -> *) (a :: k) (b :: k).
(AlgebraType (EffCat m) d, AlgebraType0 (EffCat m) f) =>
(forall (x :: k) (y :: k). f x y -> d x y)
-> EffCat m f a b -> d a b
foldNatFree2 forall (x :: k) (y :: k). f x y -> d x y
nat (Base f a b
cab)    = forall (x :: k) (y :: k). f x y -> d x y
nat f a b
cab
  foldNatFree2 forall (x :: k) (y :: k). f x y -> d x y
nat (Effect m (EffCat m f a b)
mcab) = forall {k} (c :: k -> k -> *) (m :: * -> *) (a :: k) (b :: k).
EffectCategory c m =>
m (c a b) -> c a b
effect forall a b. (a -> b) -> a -> b
$ forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall (x :: k) (y :: k). f x y -> d x y
nat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (EffCat m f a b)
mcab

  codom2 :: forall (f :: k -> k -> *).
AlgebraType0 (EffCat m) f =>
Proof (AlgebraType (EffCat m) (EffCat m f)) (EffCat m f)
codom2  = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: forall (f :: k -> k -> *).
AlgebraType (EffCat m) f =>
Proof (AlgebraType0 (EffCat m) f) (EffCat m f)
forget2 = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof

-- | Wrap a transition into @'EffCat' cat@ for any free category 'cat' (e.g.
-- 'Cat').
--
liftEffect :: ( Monad m
              , FreeAlgebra2 cat
              , AlgebraType0 cat tr
              , Category    (cat tr)
              )
           => tr a b -> EffCat m (cat tr) a b
liftEffect :: forall {k} (m :: * -> *) (cat :: (k -> k -> *) -> k -> k -> *)
       (tr :: k -> k -> *) (a :: k) (b :: k).
(Monad m, FreeAlgebra2 cat, AlgebraType0 cat tr,
 Category (cat tr)) =>
tr a b -> EffCat m (cat tr) a b
liftEffect = forall k (m :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *)
       (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType0 m f) =>
f a b -> m f a b
liftFree2 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k (m :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *)
       (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType0 m f) =>
f a b -> m f a b
liftFree2

-- | Fold @'FreeLifting'@ category based on a free category @'cat' tr@ (e.g.
-- @'C' tr@) using a functor @tr x y -> c x y@.
--
foldNatEffCat
  :: ( Monad m
     , FreeAlgebra2 cat
     , AlgebraType  cat c
     , AlgebraType0 cat tr
     , Category    (cat tr)
     , EffectCategory c m
     )
  => (forall x y. tr x y -> c x y)
  -> EffCat m (cat tr) a b
  -> c a b
foldNatEffCat :: forall {k} (m :: * -> *) (cat :: (k -> k -> *) -> k -> k -> *)
       (c :: k -> k -> *) (tr :: k -> k -> *) (a :: k) (b :: k).
(Monad m, FreeAlgebra2 cat, AlgebraType cat c, AlgebraType0 cat tr,
 Category (cat tr), EffectCategory c m) =>
(forall (x :: k) (y :: k). tr x y -> c x y)
-> EffCat m (cat tr) a b -> c a b
foldNatEffCat forall (x :: k) (y :: k). tr x y -> c x y
nat = forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 (forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall (x :: k) (y :: k). tr x y -> c x y
nat)

-- | Join all effects in a free effectful category 'EffCat'.
--
runEffCat
  :: Monad m
  => EffCat m c a b
  -> m (c a b)
runEffCat :: forall {k} (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Monad m =>
EffCat m c a b -> m (c a b)
runEffCat (Base c a b
f) = forall (m :: * -> *) a. Monad m => a -> m a
return c a b
f
runEffCat (Effect m (EffCat m c a b)
mf) = forall {k} (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Monad m =>
EffCat m c a b -> m (c a b)
runEffCat forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (EffCat m c a b)
mf

-- | Functor from @(->)@ category to @'Kleisli' m@.  If @m@ is 'Identity' then
-- it will respect 'effect' i.e.
-- @'liftKleisli' ('effect' ar) = 'effect' ('liftKleisli' \<$\> ar)@.
--
liftKleisli :: Applicative m => (a -> b) -> Kleisli m a b
liftKleisli :: forall (m :: * -> *) a b.
Applicative m =>
(a -> b) -> Kleisli m a b
liftKleisli a -> b
f = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)