{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Effect.Internal where

import Control.Monad
import Data.Kind

-- * The freer monad

data Freer f a where
  Pure :: a -> Freer f a
  Impure :: f a -> (a -> Freer f b) -> Freer f b

instance Functor (Freer f) where
  fmap :: forall a b. (a -> b) -> Freer f a -> Freer f b
fmap a -> b
g (Pure a
x) = b -> Freer f b
forall a (f :: * -> *). a -> Freer f a
Pure (b -> Freer f b) -> b -> Freer f b
forall a b. (a -> b) -> a -> b
$ a -> b
g a
x
  fmap a -> b
g (Impure f a
x a -> Freer f a
cont) = f a -> (a -> Freer f b) -> Freer f b
forall (f :: * -> *) ty b. f ty -> (ty -> Freer f b) -> Freer f b
Impure f a
x ((a -> b) -> Freer f a -> Freer f b
forall a b. (a -> b) -> Freer f a -> Freer f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
g (Freer f a -> Freer f b) -> (a -> Freer f a) -> a -> Freer f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Freer f a
cont)

instance Applicative (Freer f) where
  pure :: forall a. a -> Freer f a
pure = a -> Freer f a
forall a (f :: * -> *). a -> Freer f a
Pure
  <*> :: forall a b. Freer f (a -> b) -> Freer f a -> Freer f b
(<*>) = Freer f (a -> b) -> Freer f a -> Freer f b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad (Freer f) where
  (Pure a
x) >>= :: forall a b. Freer f a -> (a -> Freer f b) -> Freer f b
>>= a -> Freer f b
g = a -> Freer f b
g a
x
  (Impure f a
x a -> Freer f a
cont) >>= a -> Freer f b
g = f a -> (a -> Freer f b) -> Freer f b
forall (f :: * -> *) ty b. f ty -> (ty -> Freer f b) -> Freer f b
Impure f a
x (a -> Freer f a
cont (a -> Freer f a) -> (a -> Freer f b) -> a -> Freer f b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> Freer f b
g)

-- * Fixpoint functors

-- $doc
-- This is a generalisation/analogy with constructions like
--
-- > data Fix = f (Fix f)
--
-- Here, @f@ is of kind @Type -> Type@. The first insight is that this works
-- for arbitrary kinds @k@, i.e. for any @f :: k -> k@. The second step is
-- noting that for @k = Type -> Type@, we can also build something that
-- alternates between to @f@s. This is that type:

newtype Fixpoint (f :: (Type -> Type) -> Type -> Type) (g :: (Type -> Type) -> Type -> Type) :: Type -> Type where
  Fixpoint :: {forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint :: f (Fixpoint g f) a} -> Fixpoint f g a

instance (forall h. Functor (f h)) => Functor (Fixpoint f g) where
  fmap :: forall a b. (a -> b) -> Fixpoint f g a -> Fixpoint f g b
fmap a -> b
f (Fixpoint f (Fixpoint g f) a
x) = f (Fixpoint g f) b -> Fixpoint f g b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
f (Fixpoint g f) a -> Fixpoint f g a
Fixpoint (f (Fixpoint g f) b -> Fixpoint f g b)
-> f (Fixpoint g f) b -> Fixpoint f g b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f (Fixpoint g f) a -> f (Fixpoint g f) b
forall a b. (a -> b) -> f (Fixpoint g f) a -> f (Fixpoint g f) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f (Fixpoint g f) a
x

instance (forall h. Applicative (f h)) => Applicative (Fixpoint f g) where
  pure :: forall a. a -> Fixpoint f g a
pure = f (Fixpoint g f) a -> Fixpoint f g a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
f (Fixpoint g f) a -> Fixpoint f g a
Fixpoint (f (Fixpoint g f) a -> Fixpoint f g a)
-> (a -> f (Fixpoint g f) a) -> a -> Fixpoint f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f (Fixpoint g f) a
forall a. a -> f (Fixpoint g f) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Fixpoint f (Fixpoint g f) (a -> b)
f <*> :: forall a b.
Fixpoint f g (a -> b) -> Fixpoint f g a -> Fixpoint f g b
<*> Fixpoint f (Fixpoint g f) a
x = f (Fixpoint g f) b -> Fixpoint f g b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
f (Fixpoint g f) a -> Fixpoint f g a
Fixpoint (f (Fixpoint g f) b -> Fixpoint f g b)
-> f (Fixpoint g f) b -> Fixpoint f g b
forall a b. (a -> b) -> a -> b
$ f (Fixpoint g f) (a -> b)
f f (Fixpoint g f) (a -> b)
-> f (Fixpoint g f) a -> f (Fixpoint g f) b
forall a b.
f (Fixpoint g f) (a -> b)
-> f (Fixpoint g f) a -> f (Fixpoint g f) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Fixpoint g f) a
x

instance (forall h. Monad (f h)) => Monad (Fixpoint f g) where
  Fixpoint f (Fixpoint g f) a
a >>= :: forall a b.
Fixpoint f g a -> (a -> Fixpoint f g b) -> Fixpoint f g b
>>= a -> Fixpoint f g b
f = f (Fixpoint g f) b -> Fixpoint f g b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
f (Fixpoint g f) a -> Fixpoint f g a
Fixpoint (f (Fixpoint g f) b -> Fixpoint f g b)
-> f (Fixpoint g f) b -> Fixpoint f g b
forall a b. (a -> b) -> a -> b
$ f (Fixpoint g f) a
a f (Fixpoint g f) a
-> (a -> f (Fixpoint g f) b) -> f (Fixpoint g f) b
forall a b.
f (Fixpoint g f) a
-> (a -> f (Fixpoint g f) b) -> f (Fixpoint g f) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fixpoint f g b -> f (Fixpoint g f) b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint (Fixpoint f g b -> f (Fixpoint g f) b)
-> (a -> Fixpoint f g b) -> a -> f (Fixpoint g f) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fixpoint f g b
f

-- * Interpreting fixpoint functors layer by layer

-- | The idea of this class: If you have @InterpretOneLayer f g m@ and
-- @InterpretOneLayer g f m@, it's pretty easy to obtain a function
--
-- >  interpretFixpoint ::
-- >    (InterpretOneLayer f g m, InterpretOneLayer g f m) =>
-- >    Fixpoint f g a ->
-- >    m a
-- >  fromFixpoint = interpretOneLayer fromFixpoint . unFixpoint
--
-- which calls the two 'interpretOneLayer' functions mutually recursively.
class InterpretOneLayer f g m where
  interpretOneLayer :: (forall b. Fixpoint g f b -> m b) -> f (Fixpoint g f) a -> m a

instance (Monad m) => InterpretOneLayer Freer h m where
  interpretOneLayer :: forall a.
(forall b. Fixpoint h Freer b -> m b)
-> Freer (Fixpoint h Freer) a -> m a
interpretOneLayer forall b. Fixpoint h Freer b -> m b
_ (Pure a
a) = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  interpretOneLayer forall b. Fixpoint h Freer b -> m b
interpretNextLayer (Impure Fixpoint h Freer a
op a -> Freer (Fixpoint h Freer) a
cont) = do
    a
a <- Fixpoint h Freer a -> m a
forall b. Fixpoint h Freer b -> m b
interpretNextLayer Fixpoint h Freer a
op
    (forall b. Fixpoint h Freer b -> m b)
-> Freer (Fixpoint h Freer) a -> m a
forall a.
(forall b. Fixpoint h Freer b -> m b)
-> Freer (Fixpoint h Freer) a -> m a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
InterpretOneLayer f g m =>
(forall b. Fixpoint g f b -> m b) -> f (Fixpoint g f) a -> m a
interpretOneLayer Fixpoint h Freer b -> m b
forall b. Fixpoint h Freer b -> m b
interpretNextLayer (a -> Freer (Fixpoint h Freer) a
cont a
a)

-- * Interpreting fixpoint functors layer by layer, statefully

-- $doc
-- We could be even more generic and re-use the machinery from the last
-- section, if we're willing to stack another 'StateT' monad transformer. I
-- chose this presentation because it makes 'interpretOneLayerState' easier to
-- understand and use later on.

class InterpretOneLayerState x f g m where
  interpretOneLayerState ::
    (forall b. x -> Fixpoint g f b -> m (b, x)) ->
    x ->
    f (Fixpoint g f) a ->
    m (a, x)

instance (Monad m) => InterpretOneLayerState x Freer h m where
  interpretOneLayerState :: forall a.
(forall b. x -> Fixpoint h Freer b -> m (b, x))
-> x -> Freer (Fixpoint h Freer) a -> m (a, x)
interpretOneLayerState forall b. x -> Fixpoint h Freer b -> m (b, x)
_ x
x (Pure a
a) = (a, x) -> m (a, x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, x
x)
  interpretOneLayerState forall b. x -> Fixpoint h Freer b -> m (b, x)
interpretNextLayer x
x (Impure Fixpoint h Freer a
op a -> Freer (Fixpoint h Freer) a
cont) = do
    (a
a, x
x') <- x -> Fixpoint h Freer a -> m (a, x)
forall b. x -> Fixpoint h Freer b -> m (b, x)
interpretNextLayer x
x Fixpoint h Freer a
op
    (forall b. x -> Fixpoint h Freer b -> m (b, x))
-> x -> Freer (Fixpoint h Freer) a -> m (a, x)
forall a.
(forall b. x -> Fixpoint h Freer b -> m (b, x))
-> x -> Freer (Fixpoint h Freer) a -> m (a, x)
forall x (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
InterpretOneLayerState x f g m =>
(forall b. x -> Fixpoint g f b -> m (b, x))
-> x -> f (Fixpoint g f) a -> m (a, x)
interpretOneLayerState x -> Fixpoint h Freer b -> m (b, x)
forall b. x -> Fixpoint h Freer b -> m (b, x)
interpretNextLayer x
x' (a -> Freer (Fixpoint h Freer) a
cont a
a)

-- * Effect types

-- | The kind of effects.
type Effect = (Type -> Type) -> Type -> Type

-- | A list of 'Effect's, treated as a single 'Effect'.
data JoinedEffects (ops :: [Effect]) :: Effect where
  JoinedEffectsHere :: op m a -> JoinedEffects (op ': ops) m a
  JoinedEffectsThere :: JoinedEffects ops m a -> JoinedEffects (op ': ops) m a

-- | Is a given type of effects an element of a list of effect types?
--
-- In writing "reification" instances, a useful idiom is something like
--
-- > instance EffectInject (MonadWriterEffect w) ops => MonadWriter (AST ops)
--
-- which will define "writer-like syntax" for all lists of effects that
-- contain 'WriterEffect w'. This idiom is also the reason for the functional
-- dependency in the class: @ops@ must contain enough information to determine
-- @op@.
--
-- Users of the library should't write instances of this type, as they're
-- generated automatically. Also, "reification" instances like the one above
-- aren't written by hand, usually. Macros like 'makeEffect' do this.
class EffectInject (op :: Effect) (ops :: [Effect]) | ops -> op where
  effectInject :: op m a -> JoinedEffects ops m a

instance {-# OVERLAPPING #-} EffectInject op (op ': ops) where
  effectInject :: forall (m :: * -> *) a. op m a -> JoinedEffects (op : ops) m a
effectInject = op m a -> JoinedEffects (op : ops) m a
forall (ty :: (* -> *) -> * -> *) (m :: * -> *) a
       (tys :: [(* -> *) -> * -> *]).
ty m a -> JoinedEffects (ty : tys) m a
JoinedEffectsHere

instance (EffectInject x ops) => EffectInject x (y ': ops) where
  effectInject :: forall (m :: * -> *) a. x m a -> JoinedEffects (y : ops) m a
effectInject = JoinedEffects ops m a -> JoinedEffects (y : ops) m a
forall (ty :: [(* -> *) -> * -> *]) (m :: * -> *) a
       (tys :: (* -> *) -> * -> *).
JoinedEffects ty m a -> JoinedEffects (tys : ty) m a
JoinedEffectsThere (JoinedEffects ops m a -> JoinedEffects (y : ops) m a)
-> (x m a -> JoinedEffects ops m a)
-> x m a
-> JoinedEffects (y : ops) m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x m a -> JoinedEffects ops m a
forall (m :: * -> *) a. x m a -> JoinedEffects ops m a
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *])
       (m :: * -> *) a.
EffectInject op ops =>
op m a -> JoinedEffects ops m a
effectInject

-- * Abstract syntax trees for a list of effect types

-- | An abstract syntax tree which may use 'Effect's of types 'ops'
type AST ops = Fixpoint Freer (JoinedEffects ops)

-- | Low-level convenience function to build the "singleton" 'AST'
-- corresponding to one effect.
astInject :: (EffectInject op ops) => op (AST ops) a -> AST ops a
astInject :: forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *]) a.
EffectInject op ops =>
op (AST ops) a -> AST ops a
astInject op (AST ops) a
op = Freer (Fixpoint (JoinedEffects ops) Freer) a
-> Fixpoint Freer (JoinedEffects ops) a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
f (Fixpoint g f) a -> Fixpoint f g a
Fixpoint (Freer (Fixpoint (JoinedEffects ops) Freer) a
 -> Fixpoint Freer (JoinedEffects ops) a)
-> Freer (Fixpoint (JoinedEffects ops) Freer) a
-> Fixpoint Freer (JoinedEffects ops) a
forall a b. (a -> b) -> a -> b
$ Fixpoint (JoinedEffects ops) Freer a
-> (a -> Freer (Fixpoint (JoinedEffects ops) Freer) a)
-> Freer (Fixpoint (JoinedEffects ops) Freer) a
forall (f :: * -> *) ty b. f ty -> (ty -> Freer f b) -> Freer f b
Impure (JoinedEffects ops (AST ops) a
-> Fixpoint (JoinedEffects ops) Freer a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
f (Fixpoint g f) a -> Fixpoint f g a
Fixpoint (JoinedEffects ops (AST ops) a
 -> Fixpoint (JoinedEffects ops) Freer a)
-> (op (AST ops) a -> JoinedEffects ops (AST ops) a)
-> op (AST ops) a
-> Fixpoint (JoinedEffects ops) Freer a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. op (AST ops) a -> JoinedEffects ops (AST ops) a
forall (m :: * -> *) a. op m a -> JoinedEffects ops m a
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *])
       (m :: * -> *) a.
EffectInject op ops =>
op m a -> JoinedEffects ops m a
effectInject (op (AST ops) a -> Fixpoint (JoinedEffects ops) Freer a)
-> op (AST ops) a -> Fixpoint (JoinedEffects ops) Freer a
forall a b. (a -> b) -> a -> b
$ op (AST ops) a
op) a -> Freer (Fixpoint (JoinedEffects ops) Freer) a
forall a (f :: * -> *). a -> Freer f a
Pure

-- * Interpreting 'AST's

-- | Write an instance of this class to define the "standard" interpretation of
-- an effect type into a suitable domain.
--
-- If you want to use the function 'interpretAST', this class has to be
-- implemented for all effect types you're using in your 'AST'. In the normal
-- case, you won't do this by hand, but generate the instance (and others)
-- using a macro like 'makeEffect'.
--
-- Compared to logics like "Logic.Ltl", this is a low-level class; in the
-- standard applications of these logics, you'll never have to directly
-- interact with this class.
class InterpretEffect m op where
  -- | Given a function that describes how to interpret 'AST's and an effect,
  -- return the interpretation of the effect.
  interpretEffect :: (forall b. AST ops b -> m b) -> op (AST ops) a -> m a

-- | A list of constraints, reified as a datatype. Matching on the constructors
-- will bring the constraints in scope.
--
-- This trick is used in the functions 'interpretAST' and
-- 'interpretASTStateful': while deconstructing the 'JoinedEffects' to obtain
-- the individual effects to be interpreted through their 'InterpretEffect' (or
-- 'InterpretEffectStateful') instances, the instances are brought into scope
-- by deconstructing a matching 'ConstraintList'.
data ConstraintList :: (a -> Constraint) -> [a] -> Type where
  ConstraintNil :: ConstraintList c '[]
  ConstraintCons :: (c ty) => ConstraintList c tys -> ConstraintList c (ty ': tys)

-- | The constraint that all effects @ops@ are interpretable (in the sense of
-- 'InterpretEffect') into @m@.
--
-- You should never have to manually write an instance of this class, it should
-- always be inferred.
class InterpretEffects m ops where
  interpretEffects :: ConstraintList (InterpretEffect m) ops

instance InterpretEffects m '[] where
  interpretEffects :: ConstraintList (InterpretEffect m) '[]
interpretEffects = ConstraintList (InterpretEffect m) '[]
forall {a} (c :: a -> Constraint). ConstraintList c '[]
ConstraintNil

instance (InterpretEffect m op, InterpretEffects m ops) => InterpretEffects m (op ': ops) where
  interpretEffects :: ConstraintList (InterpretEffect m) (op : ops)
interpretEffects = ConstraintList (InterpretEffect m) ops
-> ConstraintList (InterpretEffect m) (op : ops)
forall {a} (c :: a -> Constraint) (ty :: a) (tys :: [a]).
c ty =>
ConstraintList c tys -> ConstraintList c (ty : tys)
ConstraintCons ConstraintList (InterpretEffect m) ops
forall (m :: * -> *) (ops :: [(* -> *) -> * -> *]).
InterpretEffects m ops =>
ConstraintList (InterpretEffect m) ops
interpretEffects

-- | If all effect types in @ops@ have an @InterpretEffect m@ instance, this
-- function will interpret the 'AST' into 'm'.
interpretAST :: (Monad m, InterpretEffects m ops) => AST ops a -> m a
interpretAST :: forall (m :: * -> *) (ops :: [(* -> *) -> * -> *]) a.
(Monad m, InterpretEffects m ops) =>
AST ops a -> m a
interpretAST = ConstraintList (InterpretEffect m) ops -> AST ops a -> m a
forall (m :: * -> *) (ops :: [(* -> *) -> * -> *]) a.
Monad m =>
ConstraintList (InterpretEffect m) ops -> AST ops a -> m a
interpAST ConstraintList (InterpretEffect m) ops
constraintList
  where
    constraintList :: ConstraintList (InterpretEffect m) ops
constraintList = ConstraintList (InterpretEffect m) ops
forall (m :: * -> *) (ops :: [(* -> *) -> * -> *]).
InterpretEffects m ops =>
ConstraintList (InterpretEffect m) ops
interpretEffects

    interpAST :: (Monad m) => ConstraintList (InterpretEffect m) ops -> AST ops a -> m a
    interpAST :: forall (m :: * -> *) (ops :: [(* -> *) -> * -> *]) a.
Monad m =>
ConstraintList (InterpretEffect m) ops -> AST ops a -> m a
interpAST ConstraintList (InterpretEffect m) ops
cs =
      (forall b. Fixpoint (JoinedEffects ops) Freer b -> m b)
-> Freer (Fixpoint (JoinedEffects ops) Freer) a -> m a
forall a.
(forall b. Fixpoint (JoinedEffects ops) Freer b -> m b)
-> Freer (Fixpoint (JoinedEffects ops) Freer) a -> m a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
InterpretOneLayer f g m =>
(forall b. Fixpoint g f b -> m b) -> f (Fixpoint g f) a -> m a
interpretOneLayer
        (ConstraintList (InterpretEffect m) ops
-> (forall b. AST ops b -> m b)
-> JoinedEffects ops (AST ops) b
-> m b
forall (m :: * -> *) (ops :: [(* -> *) -> * -> *])
       (allOps :: [(* -> *) -> * -> *]) a.
Monad m =>
ConstraintList (InterpretEffect m) ops
-> (forall b. AST allOps b -> m b)
-> JoinedEffects ops (AST allOps) a
-> m a
interpJoinedEffs ConstraintList (InterpretEffect m) ops
cs (ConstraintList (InterpretEffect m) ops -> AST ops b -> m b
forall (m :: * -> *) (ops :: [(* -> *) -> * -> *]) a.
Monad m =>
ConstraintList (InterpretEffect m) ops -> AST ops a -> m a
interpAST ConstraintList (InterpretEffect m) ops
cs) (JoinedEffects ops (AST ops) b -> m b)
-> (Fixpoint (JoinedEffects ops) Freer b
    -> JoinedEffects ops (AST ops) b)
-> Fixpoint (JoinedEffects ops) Freer b
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fixpoint (JoinedEffects ops) Freer b
-> JoinedEffects ops (AST ops) b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint)
        (Freer (Fixpoint (JoinedEffects ops) Freer) a -> m a)
-> (AST ops a -> Freer (Fixpoint (JoinedEffects ops) Freer) a)
-> AST ops a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST ops a -> Freer (Fixpoint (JoinedEffects ops) Freer) a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint

    interpJoinedEffs ::
      (Monad m) =>
      ConstraintList (InterpretEffect m) ops ->
      (forall b. AST allOps b -> m b) ->
      JoinedEffects ops (AST allOps) a ->
      m a
    interpJoinedEffs :: forall (m :: * -> *) (ops :: [(* -> *) -> * -> *])
       (allOps :: [(* -> *) -> * -> *]) a.
Monad m =>
ConstraintList (InterpretEffect m) ops
-> (forall b. AST allOps b -> m b)
-> JoinedEffects ops (AST allOps) a
-> m a
interpJoinedEffs ConstraintList (InterpretEffect m) ops
ConstraintNil forall b. AST allOps b -> m b
_ JoinedEffects ops (AST allOps) a
op = case JoinedEffects ops (AST allOps) a
op of {}
    interpJoinedEffs (ConstraintCons ConstraintList (InterpretEffect m) tys
_) forall b. AST allOps b -> m b
iAST (JoinedEffectsHere op (AST allOps) a
op) =
      (forall b. AST allOps b -> m b) -> op (AST allOps) a -> m a
forall (ops :: [(* -> *) -> * -> *]) a.
(forall b. AST ops b -> m b) -> op (AST ops) a -> m a
forall (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
InterpretEffect m op =>
(forall b. AST ops b -> m b) -> op (AST ops) a -> m a
interpretEffect AST allOps b -> m b
forall b. AST allOps b -> m b
iAST op (AST allOps) a
op
    interpJoinedEffs (ConstraintCons ConstraintList (InterpretEffect m) tys
cs') forall b. AST allOps b -> m b
iAST (JoinedEffectsThere JoinedEffects ops (AST allOps) a
op) =
      ConstraintList (InterpretEffect m) tys
-> (forall b. AST allOps b -> m b)
-> JoinedEffects tys (AST allOps) a
-> m a
forall (m :: * -> *) (ops :: [(* -> *) -> * -> *])
       (allOps :: [(* -> *) -> * -> *]) a.
Monad m =>
ConstraintList (InterpretEffect m) ops
-> (forall b. AST allOps b -> m b)
-> JoinedEffects ops (AST allOps) a
-> m a
interpJoinedEffs ConstraintList (InterpretEffect m) tys
cs' AST allOps b -> m b
forall b. AST allOps b -> m b
iAST JoinedEffects tys (AST allOps) a
JoinedEffects ops (AST allOps) a
op

-- * Interpreting 'AST's, statefully

-- | Write an instance of this class to define the "statefully modified"
-- interpretation of an effect type into a suitable domain. The intuition is
-- that you interpret effects of type @ops@ into the domain @m@, while also
-- passing a state of type @t x@ from step to step. This state will control how
-- effects are actually implemented in @m@.
--
-- If you want to use the function 'interpretASTStateful', this class has to be
-- implemented for all effect types in the 'AST' you're using.
--
-- Compared to logics like "Logic.Ltl", this is a low-level class; in the
-- standard applications of these logics, you'll never have to directly
-- interact with this class.
class InterpretEffectStateful (t :: Type -> Type) m op where
  -- | Given a function that describes how to interpret 'AST's statefully, a
  -- current "interpretation state", and an effect, return the stateful
  -- interpretation of the effect.
  interpretEffectStateful ::
    (forall b y. t y -> AST ops b -> m (b, t y)) ->
    t x ->
    op (AST ops) a ->
    m (a, t x)

-- | The constraint that all effects @ops@ are statefully interpretable with a
-- state of type @t@  into @m@ (in the sense of 'InterpretEffectStateful').
--
-- You should never have to manually write an instance of this class, it should
-- always be inferred.
class InterpretEffectsStateful t m ops where
  interpretEffectsStateful :: ConstraintList (InterpretEffectStateful t m) ops

instance InterpretEffectsStateful t m '[] where
  interpretEffectsStateful :: ConstraintList (InterpretEffectStateful t m) '[]
interpretEffectsStateful = ConstraintList (InterpretEffectStateful t m) '[]
forall {a} (c :: a -> Constraint). ConstraintList c '[]
ConstraintNil

instance
  (InterpretEffectStateful t m op, InterpretEffectsStateful t m ops) =>
  InterpretEffectsStateful t m (op ': ops)
  where
  interpretEffectsStateful :: ConstraintList (InterpretEffectStateful t m) (op : ops)
interpretEffectsStateful = ConstraintList (InterpretEffectStateful t m) ops
-> ConstraintList (InterpretEffectStateful t m) (op : ops)
forall {a} (c :: a -> Constraint) (ty :: a) (tys :: [a]).
c ty =>
ConstraintList c tys -> ConstraintList c (ty : tys)
ConstraintCons ConstraintList (InterpretEffectStateful t m) ops
forall (t :: * -> *) (m :: * -> *) (ops :: [(* -> *) -> * -> *]).
InterpretEffectsStateful t m ops =>
ConstraintList (InterpretEffectStateful t m) ops
interpretEffectsStateful

-- | If all effect types in @ops@ have an @InterpretEffectStateful t m@
-- instance, this function will interpret the 'AST', starting at a given
-- initial "interpretation state" of type @t x@ for some @x@.
interpretASTStateful :: (Monad m, InterpretEffectsStateful t m ops) => t x -> AST ops a -> m (a, t x)
interpretASTStateful :: forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *]) x
       a.
(Monad m, InterpretEffectsStateful t m ops) =>
t x -> AST ops a -> m (a, t x)
interpretASTStateful = ConstraintList (InterpretEffectStateful t m) ops
-> t x -> AST ops a -> m (a, t x)
forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *]) x
       a.
Monad m =>
ConstraintList (InterpretEffectStateful t m) ops
-> t x -> AST ops a -> m (a, t x)
interpASTState ConstraintList (InterpretEffectStateful t m) ops
constraintList
  where
    constraintList :: ConstraintList (InterpretEffectStateful t m) ops
constraintList = ConstraintList (InterpretEffectStateful t m) ops
forall (t :: * -> *) (m :: * -> *) (ops :: [(* -> *) -> * -> *]).
InterpretEffectsStateful t m ops =>
ConstraintList (InterpretEffectStateful t m) ops
interpretEffectsStateful

    interpASTState ::
      (Monad m) =>
      ConstraintList (InterpretEffectStateful t m) ops ->
      t x ->
      AST ops a ->
      m (a, t x)
    interpASTState :: forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *]) x
       a.
Monad m =>
ConstraintList (InterpretEffectStateful t m) ops
-> t x -> AST ops a -> m (a, t x)
interpASTState ConstraintList (InterpretEffectStateful t m) ops
cs t x
x =
      (forall b.
 t x -> Fixpoint (JoinedEffects ops) Freer b -> m (b, t x))
-> t x
-> Freer (Fixpoint (JoinedEffects ops) Freer) a
-> m (a, t x)
forall a.
(forall b.
 t x -> Fixpoint (JoinedEffects ops) Freer b -> m (b, t x))
-> t x
-> Freer (Fixpoint (JoinedEffects ops) Freer) a
-> m (a, t x)
forall x (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
InterpretOneLayerState x f g m =>
(forall b. x -> Fixpoint g f b -> m (b, x))
-> x -> f (Fixpoint g f) a -> m (a, x)
interpretOneLayerState
        ( \t x
x' Fixpoint (JoinedEffects ops) Freer b
acts ->
            ConstraintList (InterpretEffectStateful t m) ops
-> (forall b y. t y -> AST ops b -> m (b, t y))
-> t x
-> JoinedEffects ops (AST ops) b
-> m (b, t x)
forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *])
       (allOps :: [(* -> *) -> * -> *]) x a.
Monad m =>
ConstraintList (InterpretEffectStateful t m) ops
-> (forall b y. t y -> AST allOps b -> m (b, t y))
-> t x
-> JoinedEffects ops (AST allOps) a
-> m (a, t x)
interpJoinedEffsState
              ConstraintList (InterpretEffectStateful t m) ops
cs
              (ConstraintList (InterpretEffectStateful t m) ops
-> t y -> AST ops b -> m (b, t y)
forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *]) x
       a.
Monad m =>
ConstraintList (InterpretEffectStateful t m) ops
-> t x -> AST ops a -> m (a, t x)
interpASTState ConstraintList (InterpretEffectStateful t m) ops
cs)
              t x
x'
              (Fixpoint (JoinedEffects ops) Freer b
-> JoinedEffects ops (AST ops) b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint Fixpoint (JoinedEffects ops) Freer b
acts)
        )
        t x
x
        (Freer (Fixpoint (JoinedEffects ops) Freer) a -> m (a, t x))
-> (AST ops a -> Freer (Fixpoint (JoinedEffects ops) Freer) a)
-> AST ops a
-> m (a, t x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST ops a -> Freer (Fixpoint (JoinedEffects ops) Freer) a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint

    interpJoinedEffsState ::
      (Monad m) =>
      ConstraintList (InterpretEffectStateful t m) ops ->
      (forall b y. t y -> AST allOps b -> m (b, t y)) ->
      t x ->
      JoinedEffects ops (AST allOps) a ->
      m (a, t x)
    interpJoinedEffsState :: forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *])
       (allOps :: [(* -> *) -> * -> *]) x a.
Monad m =>
ConstraintList (InterpretEffectStateful t m) ops
-> (forall b y. t y -> AST allOps b -> m (b, t y))
-> t x
-> JoinedEffects ops (AST allOps) a
-> m (a, t x)
interpJoinedEffsState ConstraintList (InterpretEffectStateful t m) ops
ConstraintNil forall b y. t y -> AST allOps b -> m (b, t y)
_ t x
_ JoinedEffects ops (AST allOps) a
op = case JoinedEffects ops (AST allOps) a
op of {}
    interpJoinedEffsState (ConstraintCons ConstraintList (InterpretEffectStateful t m) tys
_) forall b y. t y -> AST allOps b -> m (b, t y)
iAST t x
x (JoinedEffectsHere op (AST allOps) a
op) =
      (forall b y. t y -> AST allOps b -> m (b, t y))
-> t x -> op (AST allOps) a -> m (a, t x)
forall (ops :: [(* -> *) -> * -> *]) x a.
(forall b y. t y -> AST ops b -> m (b, t y))
-> t x -> op (AST ops) a -> m (a, t x)
forall (t :: * -> *) (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) x a.
InterpretEffectStateful t m op =>
(forall b y. t y -> AST ops b -> m (b, t y))
-> t x -> op (AST ops) a -> m (a, t x)
interpretEffectStateful t y -> AST allOps b -> m (b, t y)
forall b y. t y -> AST allOps b -> m (b, t y)
iAST t x
x op (AST allOps) a
op
    interpJoinedEffsState (ConstraintCons ConstraintList (InterpretEffectStateful t m) tys
cs') forall b y. t y -> AST allOps b -> m (b, t y)
iAST t x
x (JoinedEffectsThere JoinedEffects ops (AST allOps) a
op) =
      ConstraintList (InterpretEffectStateful t m) tys
-> (forall b y. t y -> AST allOps b -> m (b, t y))
-> t x
-> JoinedEffects tys (AST allOps) a
-> m (a, t x)
forall (m :: * -> *) (t :: * -> *) (ops :: [(* -> *) -> * -> *])
       (allOps :: [(* -> *) -> * -> *]) x a.
Monad m =>
ConstraintList (InterpretEffectStateful t m) ops
-> (forall b y. t y -> AST allOps b -> m (b, t y))
-> t x
-> JoinedEffects ops (AST allOps) a
-> m (a, t x)
interpJoinedEffsState ConstraintList (InterpretEffectStateful t m) tys
cs' t y -> AST allOps b -> m (b, t y)
forall b y. t y -> AST allOps b -> m (b, t y)
iAST t x
x JoinedEffects tys (AST allOps) a
JoinedEffects ops (AST allOps) a
op