-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A Church-encoded Freer monad.
-}
module Control.Monad.Freer.Church where

import Control.Effect (type (~>))
import Control.Freer (Freer, interpretFreer, liftIns, retractFreer, transformFreer)
import Control.Monad.Cont (Cont, ContT (ContT), runCont)
import Control.Monad.Freer (MonadFreer, interpretFreerK)
import Control.Monad.Identity (Identity (Identity), runIdentity)
import Control.Monad.Trans.Free.Church (FT (FT), retract, transFT)

-- | A Church encoded Freer monad.
newtype FreerChurch f a = FreerChurch {forall (f :: * -> *) a. FreerChurch f a -> FT f Identity a
unFreerChurch :: FT f Identity a}
    deriving newtype
        ( forall a b. a -> FreerChurch f b -> FreerChurch f a
forall a b. (a -> b) -> FreerChurch f a -> FreerChurch f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) a b. a -> FreerChurch f b -> FreerChurch f a
forall (f :: * -> *) a b.
(a -> b) -> FreerChurch f a -> FreerChurch f b
<$ :: forall a b. a -> FreerChurch f b -> FreerChurch f a
$c<$ :: forall (f :: * -> *) a b. a -> FreerChurch f b -> FreerChurch f a
fmap :: forall a b. (a -> b) -> FreerChurch f a -> FreerChurch f b
$cfmap :: forall (f :: * -> *) a b.
(a -> b) -> FreerChurch f a -> FreerChurch f b
Functor
        , forall a. a -> FreerChurch f a
forall a b. FreerChurch f a -> FreerChurch f b -> FreerChurch f a
forall a b. FreerChurch f a -> FreerChurch f b -> FreerChurch f b
forall a b.
FreerChurch f (a -> b) -> FreerChurch f a -> FreerChurch f b
forall a b c.
(a -> b -> c)
-> FreerChurch f a -> FreerChurch f b -> FreerChurch f c
forall (f :: * -> *). Functor (FreerChurch f)
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (f :: * -> *) a. a -> FreerChurch f a
forall (f :: * -> *) a b.
FreerChurch f a -> FreerChurch f b -> FreerChurch f a
forall (f :: * -> *) a b.
FreerChurch f a -> FreerChurch f b -> FreerChurch f b
forall (f :: * -> *) a b.
FreerChurch f (a -> b) -> FreerChurch f a -> FreerChurch f b
forall (f :: * -> *) a b c.
(a -> b -> c)
-> FreerChurch f a -> FreerChurch f b -> FreerChurch f c
<* :: forall a b. FreerChurch f a -> FreerChurch f b -> FreerChurch f a
$c<* :: forall (f :: * -> *) a b.
FreerChurch f a -> FreerChurch f b -> FreerChurch f a
*> :: forall a b. FreerChurch f a -> FreerChurch f b -> FreerChurch f b
$c*> :: forall (f :: * -> *) a b.
FreerChurch f a -> FreerChurch f b -> FreerChurch f b
liftA2 :: forall a b c.
(a -> b -> c)
-> FreerChurch f a -> FreerChurch f b -> FreerChurch f c
$cliftA2 :: forall (f :: * -> *) a b c.
(a -> b -> c)
-> FreerChurch f a -> FreerChurch f b -> FreerChurch f c
<*> :: forall a b.
FreerChurch f (a -> b) -> FreerChurch f a -> FreerChurch f b
$c<*> :: forall (f :: * -> *) a b.
FreerChurch f (a -> b) -> FreerChurch f a -> FreerChurch f b
pure :: forall a. a -> FreerChurch f a
$cpure :: forall (f :: * -> *) a. a -> FreerChurch f a
Applicative
        , forall a. a -> FreerChurch f a
forall a b. FreerChurch f a -> FreerChurch f b -> FreerChurch f b
forall a b.
FreerChurch f a -> (a -> FreerChurch f b) -> FreerChurch f b
forall (f :: * -> *). Applicative (FreerChurch f)
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (f :: * -> *) a. a -> FreerChurch f a
forall (f :: * -> *) a b.
FreerChurch f a -> FreerChurch f b -> FreerChurch f b
forall (f :: * -> *) a b.
FreerChurch f a -> (a -> FreerChurch f b) -> FreerChurch f b
return :: forall a. a -> FreerChurch f a
$creturn :: forall (f :: * -> *) a. a -> FreerChurch f a
>> :: forall a b. FreerChurch f a -> FreerChurch f b -> FreerChurch f b
$c>> :: forall (f :: * -> *) a b.
FreerChurch f a -> FreerChurch f b -> FreerChurch f b
>>= :: forall a b.
FreerChurch f a -> (a -> FreerChurch f b) -> FreerChurch f b
$c>>= :: forall (f :: * -> *) a b.
FreerChurch f a -> (a -> FreerChurch f b) -> FreerChurch f b
Monad
        , FreerChurch f a -> FreerChurch f a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (f :: * -> *) a.
(Functor f, Eq1 f, Eq a) =>
FreerChurch f a -> FreerChurch f a -> Bool
/= :: FreerChurch f a -> FreerChurch f a -> Bool
$c/= :: forall (f :: * -> *) a.
(Functor f, Eq1 f, Eq a) =>
FreerChurch f a -> FreerChurch f a -> Bool
== :: FreerChurch f a -> FreerChurch f a -> Bool
$c== :: forall (f :: * -> *) a.
(Functor f, Eq1 f, Eq a) =>
FreerChurch f a -> FreerChurch f a -> Bool
Eq
        , FreerChurch f a -> FreerChurch f a -> Bool
FreerChurch f a -> FreerChurch f a -> Ordering
FreerChurch f a -> FreerChurch f a -> FreerChurch f a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {f :: * -> *} {a}.
(Functor f, Ord1 f, Ord a) =>
Eq (FreerChurch f a)
forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Bool
forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Ordering
forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> FreerChurch f a
min :: FreerChurch f a -> FreerChurch f a -> FreerChurch f a
$cmin :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> FreerChurch f a
max :: FreerChurch f a -> FreerChurch f a -> FreerChurch f a
$cmax :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> FreerChurch f a
>= :: FreerChurch f a -> FreerChurch f a -> Bool
$c>= :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Bool
> :: FreerChurch f a -> FreerChurch f a -> Bool
$c> :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Bool
<= :: FreerChurch f a -> FreerChurch f a -> Bool
$c<= :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Bool
< :: FreerChurch f a -> FreerChurch f a -> Bool
$c< :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Bool
compare :: FreerChurch f a -> FreerChurch f a -> Ordering
$ccompare :: forall (f :: * -> *) a.
(Functor f, Ord1 f, Ord a) =>
FreerChurch f a -> FreerChurch f a -> Ordering
Ord
        )
    deriving stock (forall a. FreerChurch f a -> Bool
forall m a. Monoid m => (a -> m) -> FreerChurch f a -> m
forall a b. (a -> b -> b) -> b -> FreerChurch f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> FreerChurch f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => FreerChurch f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => FreerChurch f a -> a
forall (f :: * -> *) m.
(Foldable f, Monoid m) =>
FreerChurch f m -> m
forall (f :: * -> *) a. Foldable f => FreerChurch f a -> Bool
forall (f :: * -> *) a. Foldable f => FreerChurch f a -> Int
forall (f :: * -> *) a. Foldable f => FreerChurch f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> FreerChurch f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> FreerChurch f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> FreerChurch f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> FreerChurch f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => FreerChurch f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => FreerChurch f a -> a
sum :: forall a. Num a => FreerChurch f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => FreerChurch f a -> a
minimum :: forall a. Ord a => FreerChurch f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => FreerChurch f a -> a
maximum :: forall a. Ord a => FreerChurch f a -> a
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => FreerChurch f a -> a
elem :: forall a. Eq a => a -> FreerChurch f a -> Bool
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> FreerChurch f a -> Bool
length :: forall a. FreerChurch f a -> Int
$clength :: forall (f :: * -> *) a. Foldable f => FreerChurch f a -> Int
null :: forall a. FreerChurch f a -> Bool
$cnull :: forall (f :: * -> *) a. Foldable f => FreerChurch f a -> Bool
toList :: forall a. FreerChurch f a -> [a]
$ctoList :: forall (f :: * -> *) a. Foldable f => FreerChurch f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> FreerChurch f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> FreerChurch f a -> a
foldr1 :: forall a. (a -> a -> a) -> FreerChurch f a -> a
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> FreerChurch f a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> FreerChurch f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> FreerChurch f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FreerChurch f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> FreerChurch f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FreerChurch f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> FreerChurch f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FreerChurch f a -> b
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> FreerChurch f a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> FreerChurch f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> FreerChurch f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FreerChurch f a -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> FreerChurch f a -> m
fold :: forall m. Monoid m => FreerChurch f m -> m
$cfold :: forall (f :: * -> *) m.
(Foldable f, Monoid m) =>
FreerChurch f m -> m
Foldable, forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall {f :: * -> *}. Traversable f => Functor (FreerChurch f)
forall {f :: * -> *}. Traversable f => Foldable (FreerChurch f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
FreerChurch f (m a) -> m (FreerChurch f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
FreerChurch f (f a) -> f (FreerChurch f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> FreerChurch f a -> m (FreerChurch f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> FreerChurch f a -> f (FreerChurch f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FreerChurch f a -> f (FreerChurch f b)
sequence :: forall (m :: * -> *) a.
Monad m =>
FreerChurch f (m a) -> m (FreerChurch f a)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
FreerChurch f (m a) -> m (FreerChurch f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FreerChurch f a -> m (FreerChurch f b)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> FreerChurch f a -> m (FreerChurch f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FreerChurch f (f a) -> f (FreerChurch f a)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
FreerChurch f (f a) -> f (FreerChurch f a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FreerChurch f a -> f (FreerChurch f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> FreerChurch f a -> f (FreerChurch f b)
Traversable)

liftInsChurch :: ins a -> FreerChurch ins a
liftInsChurch :: forall (ins :: * -> *) a. ins a -> FreerChurch ins a
liftInsChurch ins a
e = forall (f :: * -> *) a. FT f Identity a -> FreerChurch f a
FreerChurch forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (m :: * -> *) a.
(forall r.
 (a -> m r) -> (forall x. (x -> m r) -> f x -> m r) -> m r)
-> FT f m a
FT \a -> Identity r
k forall x. (x -> Identity r) -> ins x -> Identity r
f -> forall x. (x -> Identity r) -> ins x -> Identity r
f a -> Identity r
k ins a
e
{-# INLINE liftInsChurch #-}

interpretChurch :: Monad m => (ins ~> m) -> FreerChurch ins a -> m a
interpretChurch :: forall (m :: * -> *) (ins :: * -> *) a.
Monad m =>
(ins ~> m) -> FreerChurch ins a -> m a
interpretChurch ins ~> m
i = forall (f :: * -> *) a. Monad f => F f a -> f a
retract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) (m :: * -> *) b.
(forall a. f a -> g a) -> FT f m b -> FT g m b
transFT ins ~> m
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. FreerChurch f a -> FT f Identity a
unFreerChurch
{-# INLINE interpretChurch #-}

interpretChurchK :: (e ~> Cont r) -> FreerChurch e ~> Cont r
interpretChurchK :: forall (e :: * -> *) r. (e ~> Cont r) -> FreerChurch e ~> Cont r
interpretChurchK e ~> Cont r
i (FreerChurch (FT forall r.
(x -> Identity r)
-> (forall x. (x -> Identity r) -> e x -> Identity r) -> Identity r
f)) =
    forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> Identity r
k -> forall r.
(x -> Identity r)
-> (forall x. (x -> Identity r) -> e x -> Identity r) -> Identity r
f x -> Identity r
k \x -> Identity r
k' e x
e -> forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ forall r a. Cont r a -> (a -> r) -> r
runCont (e ~> Cont r
i e x
e) (forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Identity r
k')

instance Freer Monad FreerChurch where
    liftIns :: forall (ins :: * -> *) a. ins a -> FreerChurch ins a
liftIns = forall (ins :: * -> *) a. ins a -> FreerChurch ins a
liftInsChurch
    interpretFreer :: forall (m :: * -> *) (ins :: * -> *) a.
Monad m =>
(ins ~> m) -> FreerChurch ins a -> m a
interpretFreer = forall (m :: * -> *) (ins :: * -> *) a.
Monad m =>
(ins ~> m) -> FreerChurch ins a -> m a
interpretChurch
    retractFreer :: forall (m :: * -> *) a. Monad m => FreerChurch m a -> m a
retractFreer = forall (f :: * -> *) a. Monad f => F f a -> f a
retract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. FreerChurch f a -> FT f Identity a
unFreerChurch
    transformFreer :: forall (e :: * -> *) (e' :: * -> *) a.
(e ~> e') -> FreerChurch e a -> FreerChurch e' a
transformFreer e ~> e'
phi = forall (f :: * -> *) a. FT f Identity a -> FreerChurch f a
FreerChurch forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) (m :: * -> *) b.
(forall a. f a -> g a) -> FT f m b -> FT g m b
transFT e ~> e'
phi forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. FreerChurch f a -> FT f Identity a
unFreerChurch
    {-# INLINE liftIns #-}
    {-# INLINE interpretFreer #-}
    {-# INLINE retractFreer #-}
    {-# INLINE transformFreer #-}

instance MonadFreer Monad FreerChurch where
    interpretFreerK :: forall (e :: * -> *) r. (e ~> Cont r) -> FreerChurch e ~> Cont r
interpretFreerK = forall (e :: * -> *) r. (e ~> Cont r) -> FreerChurch e ~> Cont r
interpretChurchK
    {-# INLINE interpretFreerK #-}