{-# 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 :: m (Kleisli m a b) -> Kleisli m a b
effect m (Kleisli m a b)
m = (a -> m b) -> Kleisli m a b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (\a
a -> m (Kleisli m a b)
m m (Kleisli m a b) -> (Kleisli m a b -> m b) -> m b
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 :: Identity (a -> b) -> a -> b
effect = Identity (a -> b) -> a -> b
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 :: EffCat m c a a
id = c a a -> EffCat m c a a
forall k (c :: k -> k -> *) (a :: k) (b :: k) (m :: * -> *).
c a b -> EffCat m c a b
Base c a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  Base c b c
f    . :: EffCat m c b c -> EffCat m c a b -> EffCat m c a c
. Base c a b
g    = c a c -> EffCat m c a c
forall k (c :: k -> k -> *) (a :: k) (b :: k) (m :: * -> *).
c a b -> EffCat m c a b
Base   (c a c -> EffCat m c a c) -> c a c -> EffCat m c a c
forall a b. (a -> b) -> a -> b
$ c b c
f c b c -> c a b -> c a c
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 = m (EffCat m c a c) -> EffCat m c a c
forall k (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
m (EffCat m c a b) -> EffCat m c a b
Effect (m (EffCat m c a c) -> EffCat m c a c)
-> m (EffCat m c a c) -> EffCat m c a c
forall a b. (a -> b) -> a -> b
$ (EffCat m c b c
f EffCat m c b c -> EffCat m c a b -> EffCat m c a c
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 -> EffCat m c a c)
-> m (EffCat m c a b) -> m (EffCat m c 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         = m (EffCat m c a c) -> EffCat m c a c
forall k (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
m (EffCat m c a b) -> EffCat m c a b
Effect (m (EffCat m c a c) -> EffCat m c a c)
-> m (EffCat m c a c) -> EffCat m c a c
forall a b. (a -> b) -> a -> b
$ (EffCat m c b c -> EffCat m c a b -> EffCat m c a c
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) (EffCat m c b c -> EffCat m c a c)
-> m (EffCat m c b c) -> m (EffCat m c a c)
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 :: m (EffCat m c a b) -> EffCat m c a b
effect = m (EffCat m c a b) -> EffCat m c a b
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 :: f a b -> EffCat m f a b
liftFree2    = f a b -> EffCat m f a b
forall k (c :: k -> k -> *) (a :: k) (b :: k) (m :: * -> *).
c a b -> EffCat m c a b
Base
  foldNatFree2 :: (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)    = f a b -> d a b
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) = m (d a b) -> d a b
forall k (c :: k -> k -> *) (m :: * -> *) (a :: k) (b :: k).
EffectCategory c m =>
m (c a b) -> c a b
effect (m (d a b) -> d a b) -> m (d a b) -> d a b
forall a b. (a -> b) -> a -> b
$ (forall (x :: k) (y :: k). f x y -> d x y)
-> EffCat m f a b -> d 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 (EffCat m f a b -> d a b) -> m (EffCat m f a b) -> m (d a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (EffCat m f a b)
mcab

  codom2 :: Proof (AlgebraType (EffCat m) (EffCat m f)) (EffCat m f)
codom2  = Proof (AlgebraType (EffCat m) (EffCat m f)) (EffCat m f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: Proof (AlgebraType0 (EffCat m) f) (EffCat m f)
forget2 = Proof (AlgebraType0 (EffCat m) f) (EffCat m f)
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 :: tr a b -> EffCat m (cat tr) a b
liftEffect = cat tr a b -> EffCat m (cat tr) a b
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 (cat tr a b -> EffCat m (cat tr) a b)
-> (tr a b -> cat tr a b) -> tr a b -> EffCat m (cat tr) a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. tr a b -> cat tr a b
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 (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 (x :: k) (y :: k). cat tr x y -> c x y)
-> EffCat m (cat tr) a b -> c 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). tr x y -> c x y) -> cat tr x y -> c x y
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 :: EffCat m c a b -> m (c a b)
runEffCat (Base c a b
f) = c a b -> m (c a b)
forall (m :: * -> *) a. Monad m => a -> m a
return c a b
f
runEffCat (Effect m (EffCat m c a b)
mf) = EffCat m c a b -> m (c a b)
forall k (m :: * -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Monad m =>
EffCat m c a b -> m (c a b)
runEffCat (EffCat m c a b -> m (c a b)) -> m (EffCat m c a b) -> m (c a b)
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 :: (a -> b) -> Kleisli m a b
liftKleisli a -> b
f = (a -> m b) -> Kleisli m a b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (b -> m b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> m b) -> (a -> b) -> a -> m b
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)