{-# LANGUAGE BangPatterns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Extensible.Effect -- Copyright : (c) Fumiaki Kinoshita 2018 -- License : BSD3 -- -- Maintainer : Fumiaki Kinoshita <fumiexcel@gmail.com> -- -- Name-based extensible effects ----------------------------------------------------------------------------- module Data.Extensible.Effect ( -- * Base Instruction(..) , Eff , liftEff , liftsEff , hoistEff , castEff -- * Step-wise handling , Interpreter(..) , handleEff -- * Peeling , peelEff , Rebinder , rebindEff0 , peelEff0 , rebindEff1 , peelEff1 , rebindEff2 , leaveEff , retractEff -- * Anonymous actions , Action(..) , Function , runAction , (@!?) , peelAction , peelAction0 -- * transformers-compatible actions and handlers -- ** Reader , ReaderEff , askEff , asksEff , localEff , runReaderEff -- ** State , State , getEff , getsEff , putEff , modifyEff , stateEff , runStateEff , execStateEff , evalStateEff -- ** Writer , WriterEff , writerEff , tellEff , listenEff , passEff , runWriterEff , execWriterEff -- ** Maybe , MaybeEff , nothingEff , runMaybeEff -- ** Either , EitherEff , throwEff , catchEff , runEitherEff , mapLeftEff -- ** Iter , Identity , tickEff , runIterEff -- ** Cont , ContT , contEff , runContEff , callCCEff ) where import Control.Applicative import Data.Bifunctor (first) import Control.Monad.Skeleton import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Cont (ContT(..)) import Data.Extensible.Field import Data.Extensible.Inclusion import Data.Extensible.Internal.Rig import Data.Extensible.Product import Data.Extensible.Class import Data.Kind (Type) import Data.Functor.Identity import Data.Type.Equality import Type.Membership -- | A unit of named effects. This is a variant of @(':|')@ specialised for -- 'Type -> Type'. data Instruction (xs :: [Assoc k (Type -> Type)]) a where Instruction :: !(Membership xs kv) -> TargetOf kv a -> Instruction xs a -- | The extensible operational monad type Eff xs = Skeleton (Instruction xs) -- | Lift an instruction onto an 'Eff' action. liftEff :: forall s t xs a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff :: Proxy s -> t a -> Eff xs a liftEff Proxy s p t a x = Proxy s -> t a -> (a -> a) -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. Lookup xs s t => Proxy s -> t a -> (a -> r) -> Eff xs r liftsEff Proxy s p t a x a -> a forall a. a -> a id {-# INLINE liftEff #-} -- | Lift an instruction onto an 'Eff' action and apply a function to the result. liftsEff :: forall s t xs a r. Lookup xs s t => Proxy s -> t a -> (a -> r) -> Eff xs r liftsEff :: Proxy s -> t a -> (a -> r) -> Eff xs r liftsEff Proxy s _ t a x a -> r k = MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall a b. (a -> b) -> a -> b $ Membership xs (s ':> t) -> TargetOf (s ':> t) a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction (Membership xs (s ':> t) forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1). Lookup xs k2 v => Membership xs (k2 ':> v) association :: Membership xs (s ':> t)) t a TargetOf (s ':> t) a x Instruction xs a -> (a -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= r -> Eff xs r forall (m :: * -> *) a. Monad m => a -> m a return (r -> Eff xs r) -> (a -> r) -> a -> Eff xs r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> r k {-# INLINE liftsEff #-} -- | Censor a specific type of effects in an action. hoistEff :: forall s t xs a. Lookup xs s t => Proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a hoistEff :: Proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a hoistEff Proxy s _ forall x. t x -> t x f = (forall x. Instruction xs x -> Instruction xs x) -> Eff xs a -> Eff xs a forall (s :: * -> *) (t :: * -> *) a. (forall x. s x -> t x) -> Skeleton s a -> Skeleton t a hoistSkeleton ((forall x. Instruction xs x -> Instruction xs x) -> Eff xs a -> Eff xs a) -> (forall x. Instruction xs x -> Instruction xs x) -> Eff xs a -> Eff xs a forall a b. (a -> b) -> a -> b $ \(Instruction i t) -> case Membership xs (s ':> t) -> Membership xs kv -> Either Ordering ((s ':> t) :~: kv) forall k (xs :: [k]) (x :: k) (y :: k). Membership xs x -> Membership xs y -> Either Ordering (x :~: y) compareMembership (Membership xs (s ':> t) forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1). Lookup xs k2 v => Membership xs (k2 ':> v) association :: Membership xs (s ':> t)) Membership xs kv i of Right (s ':> t) :~: kv Refl -> Membership xs kv -> TargetOf kv x -> Instruction xs x forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i (t x -> t x forall x. t x -> t x f t x TargetOf kv x t) Either Ordering ((s ':> t) :~: kv) _ -> Membership xs kv -> TargetOf kv x -> Instruction xs x forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i TargetOf kv x t {-# INLINABLE hoistEff #-} -- | Upcast an action. castEff :: IncludeAssoc ys xs => Eff xs a -> Eff ys a castEff :: Eff xs a -> Eff ys a castEff = (forall x. Instruction xs x -> Instruction ys x) -> Eff xs a -> Eff ys a forall (s :: * -> *) (t :: * -> *) a. (forall x. s x -> t x) -> Skeleton s a -> Skeleton t a hoistSkeleton ((forall x. Instruction xs x -> Instruction ys x) -> Eff xs a -> Eff ys a) -> (forall x. Instruction xs x -> Instruction ys x) -> Eff xs a -> Eff ys a forall a b. (a -> b) -> a -> b $ \(Instruction i t) -> Membership ys kv -> TargetOf kv x -> Instruction ys x forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction (Membership xs kv -> (xs :& Membership ys) -> Membership ys kv forall k (xs :: [k]) (x :: k) (h :: k -> *). Membership xs x -> (xs :& h) -> h x hlookup Membership xs kv i xs :& Membership ys forall k v (xs :: [Assoc k v]) (ys :: [Assoc k v]). IncludeAssoc ys xs => xs :& Membership ys inclusionAssoc) TargetOf kv x t -- | Build a relay-style handler from a triple of functions. -- -- @ -- runStateEff = peelEff1 (\a s -> return (a, s)) -- (\m k s -> let (a, s') = runState m s in k a s') -- @ -- peelEff :: forall k t xs a r . Rebinder xs r -- ^ Re-bind an unrelated action -> (a -> r) -- ^ return the result -> (forall x. t x -> (x -> r) -> r) -- ^ Handle the foremost type of an action -> Eff (k >: t ': xs) a -> r peelEff :: Rebinder xs r -> (a -> r) -> (forall x. t x -> (x -> r) -> r) -> Eff ((k >: t) : xs) a -> r peelEff Rebinder xs r pass a -> r ret forall x. t x -> (x -> r) -> r wrap = Eff ((k >: t) : xs) a -> r go where go :: Eff ((k >: t) : xs) a -> r go Eff ((k >: t) : xs) a m = case Eff ((k >: t) : xs) a -> MonadView (Instruction ((k >: t) : xs)) (Skeleton (Instruction ((k >: t) : xs))) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff ((k >: t) : xs) a m of Return a a -> a -> r ret a a Instruction i t :>>= a -> Eff ((k >: t) : xs) a k -> Membership ((k >: t) : xs) kv -> ((kv :~: (k >: t)) -> r) -> (Membership xs kv -> r) -> r forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership ((k >: t) : xs) kv i (\kv :~: (k >: t) Refl -> t a -> (a -> r) -> r forall x. t x -> (x -> r) -> r wrap t a TargetOf kv a t (Eff ((k >: t) : xs) a -> r go (Eff ((k >: t) : xs) a -> r) -> (a -> Eff ((k >: t) : xs) a) -> a -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: t) : xs) a k)) (\Membership xs kv j -> Instruction xs a -> (a -> r) -> r Rebinder xs r pass (Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv j TargetOf kv a t) (Eff ((k >: t) : xs) a -> r go (Eff ((k >: t) : xs) a -> r) -> (a -> Eff ((k >: t) : xs) a) -> a -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: t) : xs) a k)) {-# INLINE peelEff #-} -- | 'peelEff' specialised for continuations with no argument peelEff0 :: forall k t xs a r. (a -> Eff xs r) -- ^ return the result -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -- ^ Handle the foremost type of an action -> Eff (k >: t ': xs) a -> Eff xs r peelEff0 :: (a -> Eff xs r) -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -> Eff ((k >: t) : xs) a -> Eff xs r peelEff0 = Rebinder xs (Eff xs r) -> (a -> Eff xs r) -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -> Eff ((k >: t) : xs) a -> Eff xs r forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. Rebinder xs r -> (a -> r) -> (forall x. t x -> (x -> r) -> r) -> Eff ((k >: t) : xs) a -> r peelEff Rebinder xs (Eff xs r) forall k (xs :: [Assoc k (* -> *)]) r. Rebinder xs (Eff xs r) rebindEff0 {-# INLINE peelEff0 #-} -- | 'peelEff' specialised for 1-argument continuation peelEff1 :: forall k t xs a b r. (a -> b -> Eff xs r) -- ^ return the result -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -- ^ Handle the foremost type of an action -> Eff (k >: t ': xs) a -> b -> Eff xs r peelEff1 :: (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r peelEff1 = Rebinder xs (b -> Eff xs r) -> (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. Rebinder xs r -> (a -> r) -> (forall x. t x -> (x -> r) -> r) -> Eff ((k >: t) : xs) a -> r peelEff Rebinder xs (b -> Eff xs r) forall k (xs :: [Assoc k (* -> *)]) a r. Rebinder xs (a -> Eff xs r) rebindEff1 {-# INLINE peelEff1 #-} -- | A function to bind an 'Instruction' in 'peelEff'. type Rebinder xs r = forall x. Instruction xs x -> (x -> r) -> r -- | A common value for the second argument of 'peelEff'. Binds an instruction -- directly. rebindEff0 :: Rebinder xs (Eff xs r) rebindEff0 :: Instruction xs x -> (x -> Eff xs r) -> Eff xs r rebindEff0 Instruction xs x i x -> Eff xs r k = MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall a b. (a -> b) -> a -> b $ Instruction xs x i Instruction xs x -> (x -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= x -> Eff xs r k -- | A pre-defined value for the second argument of 'peelEff'. -- Preserves the argument of the continuation. rebindEff1 :: Rebinder xs (a -> Eff xs r) rebindEff1 :: Instruction xs x -> (x -> a -> Eff xs r) -> a -> Eff xs r rebindEff1 Instruction xs x i x -> a -> Eff xs r k a a = MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall a b. (a -> b) -> a -> b $ Instruction xs x i Instruction xs x -> (x -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= (x -> a -> Eff xs r) -> a -> x -> Eff xs r forall a b c. (a -> b -> c) -> b -> a -> c flip x -> a -> Eff xs r k a a -- | A pre-defined value for the second argument of 'peelEff'. -- Preserves two arguments of the continuation. rebindEff2 :: Rebinder xs (a -> b -> Eff xs r) rebindEff2 :: Instruction xs x -> (x -> a -> b -> Eff xs r) -> a -> b -> Eff xs r rebindEff2 Instruction xs x i x -> a -> b -> Eff xs r k a a b b = MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r -> Eff xs r forall a b. (a -> b) -> a -> b $ Instruction xs x i Instruction xs x -> (x -> Eff xs r) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) r forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= \x x -> x -> a -> b -> Eff xs r k x x a a b b -- | Reveal the final result of 'Eff'. leaveEff :: Eff '[] a -> a leaveEff :: Eff '[] a -> a leaveEff Eff '[] a m = case Eff '[] a -> MonadView (Instruction '[]) (Skeleton (Instruction '[])) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff '[] a m of Return a a -> a a MonadView (Instruction '[]) (Skeleton (Instruction '[])) a _ -> [Char] -> a forall a. HasCallStack => [Char] -> a error [Char] "Impossible" -- | Tear down an action using the 'Monad' instance of the instruction. retractEff :: forall k m a. Monad m => Eff '[k >: m] a -> m a retractEff :: Eff '[k >: m] a -> m a retractEff Eff '[k >: m] a m = case Eff '[k >: m] a -> MonadView (Instruction '[k >: m]) (Skeleton (Instruction '[k >: m])) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff '[k >: m] a m of Return a a -> a -> m a forall (m :: * -> *) a. Monad m => a -> m a return a a Instruction Membership '[k >: m] kv i TargetOf kv a t :>>= a -> Eff '[k >: m] a k -> Membership '[k >: m] kv -> ((kv :~: (k >: m)) -> m a) -> (Membership '[] kv -> m a) -> m a forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership '[k >: m] kv i (\kv :~: (k >: m) Refl -> m a TargetOf kv a t m a -> (a -> m a) -> m a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= Eff '[k >: m] a -> m a forall k (k :: k) (m :: * -> *) a. Monad m => Eff '[k >: m] a -> m a retractEff (Eff '[k >: m] a -> m a) -> (a -> Eff '[k >: m] a) -> a -> m a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff '[k >: m] a k) ((Membership '[] kv -> m a) -> m a) -> (Membership '[] kv -> m a) -> m a forall a b. (a -> b) -> a -> b $ [Char] -> Membership '[] kv -> m a forall a. HasCallStack => [Char] -> a error [Char] "Impossible" -- | Transformation between effects newtype Interpreter f g = Interpreter { Interpreter f g -> forall (a :: k). g a -> f a runInterpreter :: forall a. g a -> f a } -- | Process an 'Eff' action using a record of 'Interpreter's. handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a handleEff RecordOf (Interpreter m) xs hs Eff xs a m = case Eff xs a -> MonadView (Instruction xs) (Eff xs) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff xs a m of Instruction Membership xs kv i TargetOf kv a t :>>= a -> Eff xs a k -> Optic' (->) (Const (TargetOf kv a -> m a)) (RecordOf (Interpreter m) xs) (Field (Interpreter m) kv) -> (Field (Interpreter m) kv -> TargetOf kv a -> m a) -> RecordOf (Interpreter m) xs -> TargetOf kv a -> m a forall r s a. Optic' (->) (Const r) s a -> (a -> r) -> s -> r views (Membership xs kv -> Optic' (->) (Const (TargetOf kv a -> m a)) (RecordOf (Interpreter m) xs) (Field (Interpreter m) kv) forall k (f :: * -> *) (p :: * -> * -> *) (t :: [k] -> (k -> *) -> *) (xs :: [k]) (h :: k -> *) (x :: k). (Extensible f p t, ExtensibleConstr t xs h x) => Membership xs x -> Optic' p f (t xs h) (h x) pieceAt Membership xs kv i) (\(Field (Interpreter x)) -> TargetOf kv a -> m a forall a. TargetOf kv a -> m a x) RecordOf (Interpreter m) xs hs TargetOf kv a t m a -> (a -> Eff xs a) -> MonadView m (Eff xs) a forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= a -> Eff xs a k Return a a -> a -> MonadView m (Eff xs) a forall x (t :: * -> *) (m :: * -> *). x -> MonadView t m x Return a a -- | Anonymous representation of instructions. data Action (args :: [Type]) a r where AResult :: Action '[] a a AArgument :: x -> Action xs a r -> Action (x ': xs) a r -- | @'Function' [a, b, c] r@ is @a -> b -> c -> r@ type family Function args r :: Type where Function '[] r = r Function (x ': xs) r = x -> Function xs r -- | Pass the arguments of 'Action' to the supplied function. runAction :: Function xs (f a) -> Action xs a r -> f r runAction :: Function xs (f a) -> Action xs a r -> f r runAction Function xs (f a) r Action xs a r AResult = f r Function xs (f a) r runAction Function xs (f a) f (AArgument x x Action xs a r a) = Function xs (f a) -> Action xs a r -> f r forall k (xs :: [*]) (f :: k -> *) (a :: k) (r :: k). Function xs (f a) -> Action xs a r -> f r runAction (Function xs (f a) x -> Function xs (f a) f x x) Action xs a r a -- | Create a 'Field' of a 'Interpreter' for an 'Action'. (@!?) :: FieldName k -> Function xs (f a) -> Field (Interpreter f) (k ':> Action xs a) FieldName k _ @!? :: FieldName k -> Function xs (f a) -> Field (Interpreter f) (k ':> Action xs a) @!? Function xs (f a) f = Interpreter f (TargetOf (k ':> Action xs a)) -> Field (Interpreter f) (k ':> Action xs a) forall v k (h :: v -> *) (kv :: Assoc k v). h (TargetOf kv) -> Field h kv Field (Interpreter f (TargetOf (k ':> Action xs a)) -> Field (Interpreter f) (k ':> Action xs a)) -> Interpreter f (TargetOf (k ':> Action xs a)) -> Field (Interpreter f) (k ':> Action xs a) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Action xs a a -> f a) -> Interpreter f (Action xs a) forall k (f :: k -> *) (g :: k -> *). (forall (a :: k). g a -> f a) -> Interpreter f g Interpreter ((forall (a :: k). Action xs a a -> f a) -> Interpreter f (Action xs a)) -> (forall (a :: k). Action xs a a -> f a) -> Interpreter f (Action xs a) forall a b. (a -> b) -> a -> b $ Function xs (f a) -> Action xs a a -> f a forall k (xs :: [*]) (f :: k -> *) (a :: k) (r :: k). Function xs (f a) -> Action xs a r -> f r runAction Function xs (f a) f infix 1 @!? -- | Specialised version of 'peelEff' for 'Action's. -- You can pass a function @a -> b -> ... -> (q -> r) -> r@ as a handler for -- @'Action' '[a, b, ...] q@. peelAction :: forall k ps q xs a r . (forall x. Instruction xs x -> (x -> r) -> r) -- ^ Re-bind an unrelated action -> (a -> r) -- ^ return the result -> Function ps ((q -> r) -> r) -- ^ Handle the foremost action -> Eff (k >: Action ps q ': xs) a -> r peelAction :: (forall x. Instruction xs x -> (x -> r) -> r) -> (a -> r) -> Function ps ((q -> r) -> r) -> Eff ((k >: Action ps q) : xs) a -> r peelAction forall x. Instruction xs x -> (x -> r) -> r pass a -> r ret Function ps ((q -> r) -> r) wrap = Eff ((k >: Action ps q) : xs) a -> r go where go :: Eff ((k >: Action ps q) : xs) a -> r go Eff ((k >: Action ps q) : xs) a m = case Eff ((k >: Action ps q) : xs) a -> MonadView (Instruction ((k >: Action ps q) : xs)) (Skeleton (Instruction ((k >: Action ps q) : xs))) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff ((k >: Action ps q) : xs) a m of Return a a -> a -> r ret a a Instruction i t :>>= a -> Eff ((k >: Action ps q) : xs) a k -> Membership ((k >: Action ps q) : xs) kv -> ((kv :~: (k >: Action ps q)) -> r) -> (Membership xs kv -> r) -> r forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership ((k >: Action ps q) : xs) kv i (\kv :~: (k >: Action ps q) Refl -> case TargetOf kv a t of (_ :: Action ps q x) -> let run :: forall t. Function t ((q -> r) -> r) -> Action t q x -> r run :: Function t ((q -> r) -> r) -> Action t q a -> r run Function t ((q -> r) -> r) f Action t q a AResult = Function t ((q -> r) -> r) (a -> r) -> r f (Eff ((k >: Action ps q) : xs) a -> r go (Eff ((k >: Action ps q) : xs) a -> r) -> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: Action ps q) : xs) a k) run Function t ((q -> r) -> r) f (AArgument x x Action xs q a a) = Function xs ((q -> r) -> r) -> Action xs q a -> r forall (t :: [*]). Function t ((q -> r) -> r) -> Action t q a -> r run (Function t ((q -> r) -> r) x -> Function xs ((q -> r) -> r) f x x) Action xs q a a in Function ps ((q -> r) -> r) -> Action ps q a -> r forall (t :: [*]). Function t ((q -> r) -> r) -> Action t q a -> r run Function ps ((q -> r) -> r) wrap TargetOf kv a Action ps q a t) ((Membership xs kv -> r) -> r) -> (Membership xs kv -> r) -> r forall a b. (a -> b) -> a -> b $ \Membership xs kv j -> Instruction xs a -> (a -> r) -> r forall x. Instruction xs x -> (x -> r) -> r pass (Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv j TargetOf kv a t) (Eff ((k >: Action ps q) : xs) a -> r go (Eff ((k >: Action ps q) : xs) a -> r) -> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: Action ps q) : xs) a k) {-# INLINE peelAction #-} -- | Non continuation-passing variant of 'peelAction'. peelAction0 :: forall k ps q xs a. Function ps (Eff xs q) -- ^ Handle the foremost action -> Eff (k >: Action ps q ': xs) a -> Eff xs a peelAction0 :: Function ps (Eff xs q) -> Eff ((k >: Action ps q) : xs) a -> Eff xs a peelAction0 Function ps (Eff xs q) wrap = Eff ((k >: Action ps q) : xs) a -> Eff xs a go where go :: Eff ((k >: Action ps q) : xs) a -> Eff xs a go Eff ((k >: Action ps q) : xs) a m = case Eff ((k >: Action ps q) : xs) a -> MonadView (Instruction ((k >: Action ps q) : xs)) (Skeleton (Instruction ((k >: Action ps q) : xs))) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff ((k >: Action ps q) : xs) a m of Return a a -> a -> Eff xs a forall (m :: * -> *) a. Monad m => a -> m a return a a Instruction i t :>>= a -> Eff ((k >: Action ps q) : xs) a k -> Membership ((k >: Action ps q) : xs) kv -> ((kv :~: (k >: Action ps q)) -> Eff xs a) -> (Membership xs kv -> Eff xs a) -> Eff xs a forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership ((k >: Action ps q) : xs) kv i (\kv :~: (k >: Action ps q) Refl -> case TargetOf kv a t of (_ :: Action ps q x) -> let run :: forall t. Function t (Eff xs q) -> Action t q x -> Eff xs a run :: Function t (Eff xs q) -> Action t q a -> Eff xs a run Function t (Eff xs q) f Action t q a AResult = Skeleton (Instruction xs) a Function t (Eff xs q) f Skeleton (Instruction xs) a -> (a -> Eff xs a) -> Eff xs a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= Eff ((k >: Action ps q) : xs) a -> Eff xs a go (Eff ((k >: Action ps q) : xs) a -> Eff xs a) -> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: Action ps q) : xs) a k run Function t (Eff xs q) f (AArgument x x Action xs q a a) = Function xs (Eff xs q) -> Action xs q a -> Eff xs a forall (t :: [*]). Function t (Eff xs q) -> Action t q a -> Eff xs a run (Function t (Eff xs q) x -> Function xs (Eff xs q) f x x) Action xs q a a in Function ps (Eff xs q) -> Action ps q a -> Eff xs a forall (t :: [*]). Function t (Eff xs q) -> Action t q a -> Eff xs a run Function ps (Eff xs q) wrap TargetOf kv a Action ps q a t) ((Membership xs kv -> Eff xs a) -> Eff xs a) -> (Membership xs kv -> Eff xs a) -> Eff xs a forall a b. (a -> b) -> a -> b $ \Membership xs kv j -> Instruction xs a -> (a -> Eff xs a) -> Eff xs a forall k (xs :: [Assoc k (* -> *)]) r. Rebinder xs (Eff xs r) rebindEff0 (Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv j TargetOf kv a t) (Eff ((k >: Action ps q) : xs) a -> Eff xs a go (Eff ((k >: Action ps q) : xs) a -> Eff xs a) -> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: Action ps q) : xs) a k) {-# INLINE peelAction0 #-} -- | The reader monad is characterised by a type equality between the result -- type and the enviroment type. type ReaderEff = (:~:) -- | Fetch the environment. askEff :: forall k r xs. Lookup xs k (ReaderEff r) => Proxy k -> Eff xs r askEff :: Proxy k -> Eff xs r askEff Proxy k p = Proxy k -> (r :~: r) -> Eff xs r forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k p r :~: r forall k (a :: k). a :~: a Refl {-# INLINE askEff #-} -- | Pass the environment to a function. asksEff :: forall k r xs a. Lookup xs k (ReaderEff r) => Proxy k -> (r -> a) -> Eff xs a asksEff :: Proxy k -> (r -> a) -> Eff xs a asksEff Proxy k p = Proxy k -> (r :~: r) -> (r -> a) -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. Lookup xs s t => Proxy s -> t a -> (a -> r) -> Eff xs r liftsEff Proxy k p r :~: r forall k (a :: k). a :~: a Refl {-# INLINE asksEff #-} -- | Modify the enviroment locally. localEff :: forall k r xs a. Lookup xs k (ReaderEff r) => Proxy k -> (r -> r) -> Eff xs a -> Eff xs a localEff :: Proxy k -> (r -> r) -> Eff xs a -> Eff xs a localEff Proxy k _ r -> r f = Eff xs a -> Eff xs a go where go :: Eff xs a -> Eff xs a go Eff xs a m = case Eff xs a -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff xs a m of Return a a -> a -> Eff xs a forall (m :: * -> *) a. Monad m => a -> m a return a a Instruction i t :>>= a -> Eff xs a k -> case Membership xs (k >: ReaderEff r) -> Membership xs kv -> Either Ordering ((k >: ReaderEff r) :~: kv) forall k (xs :: [k]) (x :: k) (y :: k). Membership xs x -> Membership xs y -> Either Ordering (x :~: y) compareMembership (Membership xs (k >: ReaderEff r) forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1). Lookup xs k2 v => Membership xs (k2 ':> v) association :: Membership xs (k >: ReaderEff r)) Membership xs kv i of Left Ordering _ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i TargetOf kv a t Instruction xs a -> (a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= Eff xs a -> Eff xs a go (Eff xs a -> Eff xs a) -> (a -> Eff xs a) -> a -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff xs a k Right (k >: ReaderEff r) :~: kv Refl -> case TargetOf kv a t of TargetOf kv a Refl -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv r -> Instruction xs r forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i TargetOf kv r TargetOf kv a t Instruction xs r -> (r -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= Eff xs a -> Eff xs a go (Eff xs a -> Eff xs a) -> (r -> Eff xs a) -> r -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff xs a k (a -> Eff xs a) -> (r -> a) -> r -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . r -> r r -> a f {-# INLINE localEff #-} -- | Run the frontal reader effect. runReaderEff :: forall k r xs a. Eff (k >: ReaderEff r ': xs) a -> r -> Eff xs a runReaderEff :: Eff ((k >: ReaderEff r) : xs) a -> r -> Eff xs a runReaderEff Eff ((k >: ReaderEff r) : xs) a m r r = (a -> Eff xs a) -> (forall x. ReaderEff r x -> (x -> Eff xs a) -> Eff xs a) -> Eff ((k >: ReaderEff r) : xs) a -> Eff xs a forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. (a -> Eff xs r) -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -> Eff ((k >: t) : xs) a -> Eff xs r peelEff0 a -> Eff xs a forall (m :: * -> *) a. Monad m => a -> m a return (\ReaderEff r x Refl x -> Eff xs a k -> x -> Eff xs a k r x r) Eff ((k >: ReaderEff r) : xs) a m {-# INLINE runReaderEff #-} -- | Get the current state. getEff :: forall k s xs. Lookup xs k (State s) => Proxy k -> Eff xs s getEff :: Proxy k -> Eff xs s getEff Proxy k k = Proxy k -> StateT s Identity s -> Eff xs s forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k StateT s Identity s forall (m :: * -> *) s. Monad m => StateT s m s get {-# INLINE getEff #-} -- | Pass the current state to a function. getsEff :: forall k s a xs. Lookup xs k (State s) => Proxy k -> (s -> a) -> Eff xs a getsEff :: Proxy k -> (s -> a) -> Eff xs a getsEff Proxy k k = Proxy k -> StateT s Identity s -> (s -> a) -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. Lookup xs s t => Proxy s -> t a -> (a -> r) -> Eff xs r liftsEff Proxy k k StateT s Identity s forall (m :: * -> *) s. Monad m => StateT s m s get {-# INLINE getsEff #-} -- | Replace the state with a new value. putEff :: forall k s xs. Lookup xs k (State s) => Proxy k -> s -> Eff xs () putEff :: Proxy k -> s -> Eff xs () putEff Proxy k k = Proxy k -> StateT s Identity () -> Eff xs () forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (StateT s Identity () -> Eff xs ()) -> (s -> StateT s Identity ()) -> s -> Eff xs () forall b c a. (b -> c) -> (a -> b) -> a -> c . s -> StateT s Identity () forall (m :: * -> *) s. Monad m => s -> StateT s m () put {-# INLINE putEff #-} -- | Modify the state. modifyEff :: forall k s xs. Lookup xs k (State s) => Proxy k -> (s -> s) -> Eff xs () modifyEff :: Proxy k -> (s -> s) -> Eff xs () modifyEff Proxy k k s -> s f = Proxy k -> StateT s Identity () -> Eff xs () forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (StateT s Identity () -> Eff xs ()) -> StateT s Identity () -> Eff xs () forall a b. (a -> b) -> a -> b $ (s -> ((), s)) -> StateT s Identity () forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a state ((s -> ((), s)) -> StateT s Identity ()) -> (s -> ((), s)) -> StateT s Identity () forall a b. (a -> b) -> a -> b $ \s s -> ((), s -> s f s s) {-# INLINE modifyEff #-} -- | Lift a state modification function. stateEff :: forall k s xs a. Lookup xs k (State s) => Proxy k -> (s -> (a, s)) -> Eff xs a stateEff :: Proxy k -> (s -> (a, s)) -> Eff xs a stateEff Proxy k k = Proxy k -> StateT s Identity a -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (StateT s Identity a -> Eff xs a) -> ((s -> (a, s)) -> StateT s Identity a) -> (s -> (a, s)) -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . (s -> (a, s)) -> StateT s Identity a forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a state {-# INLINE stateEff #-} contState :: State s a -> (a -> s -> r) -> s -> r contState :: State s a -> (a -> s -> r) -> s -> r contState State s a m a -> s -> r k s s = let (a a, s s') = State s a -> s -> (a, s) forall s a. State s a -> s -> (a, s) runState State s a m s s in a -> s -> r k a a (s -> r) -> s -> r forall a b. (a -> b) -> a -> b $! s s' -- | Run the frontal state effect. runStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs (a, s) runStateEff :: Eff ((k >: State s) : xs) a -> s -> Eff xs (a, s) runStateEff = (a -> s -> Eff xs (a, s)) -> (forall x. State s x -> (x -> s -> Eff xs (a, s)) -> s -> Eff xs (a, s)) -> Eff ((k >: State s) : xs) a -> s -> Eff xs (a, s) forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r. (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r peelEff1 (\a a s s -> (a, s) -> Eff xs (a, s) forall (m :: * -> *) a. Monad m => a -> m a return (a a, s s)) forall x. State s x -> (x -> s -> Eff xs (a, s)) -> s -> Eff xs (a, s) forall s a r. State s a -> (a -> s -> r) -> s -> r contState {-# INLINE runStateEff #-} -- | Run the frontal state effect and return the final state. execStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs s execStateEff :: Eff ((k >: State s) : xs) a -> s -> Eff xs s execStateEff = (a -> s -> Eff xs s) -> (forall x. State s x -> (x -> s -> Eff xs s) -> s -> Eff xs s) -> Eff ((k >: State s) : xs) a -> s -> Eff xs s forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r. (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r peelEff1 ((s -> Eff xs s) -> a -> s -> Eff xs s forall a b. a -> b -> a const s -> Eff xs s forall (m :: * -> *) a. Monad m => a -> m a return) forall x. State s x -> (x -> s -> Eff xs s) -> s -> Eff xs s forall s a r. State s a -> (a -> s -> r) -> s -> r contState {-# INLINE execStateEff #-} -- | Run the frontal state effect and return the final result. evalStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs a evalStateEff :: Eff ((k >: State s) : xs) a -> s -> Eff xs a evalStateEff = (a -> s -> Eff xs a) -> (forall x. State s x -> (x -> s -> Eff xs a) -> s -> Eff xs a) -> Eff ((k >: State s) : xs) a -> s -> Eff xs a forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r. (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r peelEff1 (Eff xs a -> s -> Eff xs a forall a b. a -> b -> a const (Eff xs a -> s -> Eff xs a) -> (a -> Eff xs a) -> a -> s -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff xs a forall (m :: * -> *) a. Monad m => a -> m a return) forall x. State s x -> (x -> s -> Eff xs a) -> s -> Eff xs a forall s a r. State s a -> (a -> s -> r) -> s -> r contState {-# INLINE evalStateEff #-} -- | @(,)@ already is a writer monad. type WriterEff w = (,) w -- | Write the second element and return the first element. writerEff :: forall k w xs a. (Lookup xs k (WriterEff w)) => Proxy k -> (a, w) -> Eff xs a writerEff :: Proxy k -> (a, w) -> Eff xs a writerEff Proxy k k (a a, w w) = Proxy k -> (w, a) -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (w w, a a) {-# INLINE writerEff #-} -- | Write a value. tellEff :: forall k w xs. (Lookup xs k (WriterEff w)) => Proxy k -> w -> Eff xs () tellEff :: Proxy k -> w -> Eff xs () tellEff Proxy k k w w = Proxy k -> (w, ()) -> Eff xs () forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (w w, ()) {-# INLINE tellEff #-} -- | Squash the outputs into one step and return it. listenEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w) => Proxy k -> Eff xs a -> Eff xs (a, w) listenEff :: Proxy k -> Eff xs a -> Eff xs (a, w) listenEff Proxy k p = w -> Eff xs a -> Eff xs (a, w) go w forall a. Monoid a => a mempty where go :: w -> Eff xs a -> Eff xs (a, w) go w w Eff xs a m = case Eff xs a -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff xs a m of Return a a -> Proxy k -> ((a, w), w) -> Eff xs (a, w) forall k (k :: k) w (xs :: [Assoc k (* -> *)]) a. Lookup xs k (WriterEff w) => Proxy k -> (a, w) -> Eff xs a writerEff Proxy k p ((a a, w w), w w) Instruction i t :>>= a -> Eff xs a k -> case Membership xs (k ':> (,) w) -> Membership xs kv -> Either Ordering ((k ':> (,) w) :~: kv) forall k (xs :: [k]) (x :: k) (y :: k). Membership xs x -> Membership xs y -> Either Ordering (x :~: y) compareMembership (Membership xs (k ':> (,) w) forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1). Lookup xs k2 v => Membership xs (k2 ':> v) association :: Membership xs (k ':> (,) w)) Membership xs kv i of Left Ordering _ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w) -> Eff xs (a, w) forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w) -> Eff xs (a, w)) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w) -> Eff xs (a, w) forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i TargetOf kv a t Instruction xs a -> (a -> Eff xs (a, w)) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w) forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= w -> Eff xs a -> Eff xs (a, w) go w w (Eff xs a -> Eff xs (a, w)) -> (a -> Eff xs a) -> a -> Eff xs (a, w) forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff xs a k Right (k ':> (,) w) :~: kv Refl -> let (w w', a a) = (w, a) TargetOf kv a t !w'' :: w w'' = w -> w -> w forall a. Monoid a => a -> a -> a mappend w w w w' in w -> Eff xs a -> Eff xs (a, w) go w w'' (a -> Eff xs a k a a) {-# INLINE listenEff #-} -- | Modify the output using the function in the result. passEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w) => Proxy k -> Eff xs (a, w -> w) -> Eff xs a passEff :: Proxy k -> Eff xs (a, w -> w) -> Eff xs a passEff Proxy k p = w -> Eff xs (a, w -> w) -> Eff xs a go w forall a. Monoid a => a mempty where go :: w -> Eff xs (a, w -> w) -> Eff xs a go w w Eff xs (a, w -> w) m = case Eff xs (a, w -> w) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w -> w) forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff xs (a, w -> w) m of Return (a a, w -> w f) -> Proxy k -> (a, w) -> Eff xs a forall k (k :: k) w (xs :: [Assoc k (* -> *)]) a. Lookup xs k (WriterEff w) => Proxy k -> (a, w) -> Eff xs a writerEff Proxy k p (a a, w -> w f w w) Instruction i t :>>= a -> Eff xs (a, w -> w) k -> case Membership xs (k ':> (,) w) -> Membership xs kv -> Either Ordering ((k ':> (,) w) :~: kv) forall k (xs :: [k]) (x :: k) (y :: k). Membership xs x -> Membership xs y -> Either Ordering (x :~: y) compareMembership (Membership xs (k ':> (,) w) forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1). Lookup xs k2 v => Membership xs (k2 ':> v) association :: Membership xs (k ':> (,) w)) Membership xs kv i of Left Ordering _ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i TargetOf kv a t Instruction xs a -> (a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= w -> Eff xs (a, w -> w) -> Eff xs a go w w (Eff xs (a, w -> w) -> Eff xs a) -> (a -> Eff xs (a, w -> w)) -> a -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff xs (a, w -> w) k Right (k ':> (,) w) :~: kv Refl -> let (w w', a a) = (w, a) TargetOf kv a t !w'' :: w w'' = w -> w -> w forall a. Monoid a => a -> a -> a mappend w w w w' in w -> Eff xs (a, w -> w) -> Eff xs a go w w'' (a -> Eff xs (a, w -> w) k a a) {-# INLINE passEff #-} contWriter :: Monoid w => (w, a) -> (a -> w -> r) -> w -> r contWriter :: (w, a) -> (a -> w -> r) -> w -> r contWriter (w w', a a) a -> w -> r k w w = a -> w -> r k a a (w -> r) -> w -> r forall a b. (a -> b) -> a -> b $! w -> w -> w forall a. Monoid a => a -> a -> a mappend w w w w' -- | Run the frontal writer effect. runWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs (a, w) runWriterEff :: Eff ((k >: WriterEff w) : xs) a -> Eff xs (a, w) runWriterEff = (a -> w -> Eff xs (a, w)) -> (forall x. WriterEff w x -> (x -> w -> Eff xs (a, w)) -> w -> Eff xs (a, w)) -> Eff ((k >: WriterEff w) : xs) a -> w -> Eff xs (a, w) forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r. (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r peelEff1 (\a a w w -> (a, w) -> Eff xs (a, w) forall (m :: * -> *) a. Monad m => a -> m a return (a a, w w)) forall x. WriterEff w x -> (x -> w -> Eff xs (a, w)) -> w -> Eff xs (a, w) forall w a r. Monoid w => (w, a) -> (a -> w -> r) -> w -> r contWriter (Eff ((k >: WriterEff w) : xs) a -> w -> Eff xs (a, w)) -> w -> Eff ((k >: WriterEff w) : xs) a -> Eff xs (a, w) forall a b c. (a -> b -> c) -> b -> a -> c `flip` w forall a. Monoid a => a mempty {-# INLINE runWriterEff #-} -- | Run the frontal state effect. execWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs w execWriterEff :: Eff ((k >: WriterEff w) : xs) a -> Eff xs w execWriterEff = (a -> w -> Eff xs w) -> (forall x. WriterEff w x -> (x -> w -> Eff xs w) -> w -> Eff xs w) -> Eff ((k >: WriterEff w) : xs) a -> w -> Eff xs w forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r. (a -> b -> Eff xs r) -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -> Eff ((k >: t) : xs) a -> b -> Eff xs r peelEff1 ((w -> Eff xs w) -> a -> w -> Eff xs w forall a b. a -> b -> a const w -> Eff xs w forall (m :: * -> *) a. Monad m => a -> m a return) forall x. WriterEff w x -> (x -> w -> Eff xs w) -> w -> Eff xs w forall w a r. Monoid w => (w, a) -> (a -> w -> r) -> w -> r contWriter (Eff ((k >: WriterEff w) : xs) a -> w -> Eff xs w) -> w -> Eff ((k >: WriterEff w) : xs) a -> Eff xs w forall a b c. (a -> b -> c) -> b -> a -> c `flip` w forall a. Monoid a => a mempty {-# INLINE execWriterEff #-} -- | An effect with no result type MaybeEff = Const () -- | Break out of the computation. Similar to 'Nothing'. nothingEff :: Lookup xs k MaybeEff => Proxy k -> Eff xs a nothingEff :: Proxy k -> Eff xs a nothingEff = (Proxy k -> () -> Eff xs a) -> () -> Proxy k -> Eff xs a forall a b c. (a -> b -> c) -> b -> a -> c flip Proxy k -> () -> Eff xs a forall k (xs :: [Assoc k (* -> *)]) (k :: k) e a. Lookup xs k (EitherEff e) => Proxy k -> e -> Eff xs a throwEff () -- | Run an effect which may fail in the name of @k@. runMaybeEff :: forall k xs a. Eff (k >: MaybeEff ': xs) a -> Eff xs (Maybe a) runMaybeEff :: Eff ((k >: MaybeEff) : xs) a -> Eff xs (Maybe a) runMaybeEff = (a -> Eff xs (Maybe a)) -> (forall x. MaybeEff x -> (x -> Eff xs (Maybe a)) -> Eff xs (Maybe a)) -> Eff ((k >: MaybeEff) : xs) a -> Eff xs (Maybe a) forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. (a -> Eff xs r) -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -> Eff ((k >: t) : xs) a -> Eff xs r peelEff0 (Maybe a -> Eff xs (Maybe a) forall (m :: * -> *) a. Monad m => a -> m a return (Maybe a -> Eff xs (Maybe a)) -> (a -> Maybe a) -> a -> Eff xs (Maybe a) forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Maybe a forall a. a -> Maybe a Just) ((forall x. MaybeEff x -> (x -> Eff xs (Maybe a)) -> Eff xs (Maybe a)) -> Eff ((k >: MaybeEff) : xs) a -> Eff xs (Maybe a)) -> (forall x. MaybeEff x -> (x -> Eff xs (Maybe a)) -> Eff xs (Maybe a)) -> Eff ((k >: MaybeEff) : xs) a -> Eff xs (Maybe a) forall a b. (a -> b) -> a -> b $ \MaybeEff x _ x -> Eff xs (Maybe a) _ -> Maybe a -> Eff xs (Maybe a) forall (m :: * -> *) a. Monad m => a -> m a return Maybe a forall a. Maybe a Nothing {-# INLINE runMaybeEff #-} -- | Throwing an exception type EitherEff = Const -- | Throw an exception @e@, throwing the rest of the computation away. throwEff :: Lookup xs k (EitherEff e) => Proxy k -> e -> Eff xs a throwEff :: Proxy k -> e -> Eff xs a throwEff Proxy k k = Proxy k -> Const e a -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (Const e a -> Eff xs a) -> (e -> Const e a) -> e -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . e -> Const e a forall k a (b :: k). a -> Const a b Const {-# INLINE throwEff #-} -- | Attach a handler for an exception. catchEff :: forall k e xs a. (Lookup xs k (EitherEff e)) => Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a catchEff :: Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a catchEff Proxy k _ Eff xs a m0 e -> Eff xs a handler = Eff xs a -> Eff xs a go Eff xs a m0 where go :: Eff xs a -> Eff xs a go Eff xs a m = case Eff xs a -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff xs a m of Return a a -> a -> Eff xs a forall (m :: * -> *) a. Monad m => a -> m a return a a Instruction i t :>>= a -> Eff xs a k -> case Membership xs (k ':> Const e) -> Membership xs kv -> Either Ordering ((k ':> Const e) :~: kv) forall k (xs :: [k]) (x :: k) (y :: k). Membership xs x -> Membership xs y -> Either Ordering (x :~: y) compareMembership (Membership xs (k ':> Const e) forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1). Lookup xs k2 v => Membership xs (k2 ':> v) association :: Membership xs (k ':> Const e)) Membership xs kv i of Left Ordering _ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a -> Eff xs a forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv i TargetOf kv a t Instruction xs a -> (a -> Eff xs a) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= Eff xs a -> Eff xs a go (Eff xs a -> Eff xs a) -> (a -> Eff xs a) -> a -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff xs a k Right (k ':> Const e) :~: kv Refl -> e -> Eff xs a handler (Const e a -> e forall a k (b :: k). Const a b -> a getConst Const e a TargetOf kv a t) {-# INLINE catchEff #-} -- | Run an action and abort on 'throwEff'. runEitherEff :: forall k e xs a. Eff (k >: EitherEff e ': xs) a -> Eff xs (Either e a) runEitherEff :: Eff ((k >: EitherEff e) : xs) a -> Eff xs (Either e a) runEitherEff = (a -> Eff xs (Either e a)) -> (forall x. EitherEff e x -> (x -> Eff xs (Either e a)) -> Eff xs (Either e a)) -> Eff ((k >: EitherEff e) : xs) a -> Eff xs (Either e a) forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r. (a -> Eff xs r) -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -> Eff ((k >: t) : xs) a -> Eff xs r peelEff0 (Either e a -> Eff xs (Either e a) forall (m :: * -> *) a. Monad m => a -> m a return (Either e a -> Eff xs (Either e a)) -> (a -> Either e a) -> a -> Eff xs (Either e a) forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Either e a forall a b. b -> Either a b Right) ((forall x. EitherEff e x -> (x -> Eff xs (Either e a)) -> Eff xs (Either e a)) -> Eff ((k >: EitherEff e) : xs) a -> Eff xs (Either e a)) -> (forall x. EitherEff e x -> (x -> Eff xs (Either e a)) -> Eff xs (Either e a)) -> Eff ((k >: EitherEff e) : xs) a -> Eff xs (Either e a) forall a b. (a -> b) -> a -> b $ \(Const e) x -> Eff xs (Either e a) _ -> Either e a -> Eff xs (Either e a) forall (m :: * -> *) a. Monad m => a -> m a return (Either e a -> Eff xs (Either e a)) -> Either e a -> Eff xs (Either e a) forall a b. (a -> b) -> a -> b $ e -> Either e a forall a b. a -> Either a b Left e e {-# INLINE runEitherEff #-} -- | Put a milestone on a computation. tickEff :: Lookup xs k Identity => Proxy k -> Eff xs () tickEff :: Proxy k -> Eff xs () tickEff Proxy k k = Proxy k -> Identity () -> Eff xs () forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (Identity () -> Eff xs ()) -> Identity () -> Eff xs () forall a b. (a -> b) -> a -> b $ () -> Identity () forall a. a -> Identity a Identity () {-# INLINE tickEff #-} mapHeadEff :: (forall x. s x -> t x) -> Eff ((k >: s) ': xs) a -> Eff ((k' >: t) ': xs) a mapHeadEff :: (forall x. s x -> t x) -> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a mapHeadEff forall x. s x -> t x f = (forall x. Instruction ((k >: s) : xs) x -> Instruction ((k' >: t) : xs) x) -> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a forall (s :: * -> *) (t :: * -> *) a. (forall x. s x -> t x) -> Skeleton s a -> Skeleton t a hoistSkeleton ((forall x. Instruction ((k >: s) : xs) x -> Instruction ((k' >: t) : xs) x) -> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a) -> (forall x. Instruction ((k >: s) : xs) x -> Instruction ((k' >: t) : xs) x) -> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a forall a b. (a -> b) -> a -> b $ \(Instruction i t) -> Membership ((k >: s) : xs) kv -> ((kv :~: (k >: s)) -> Instruction ((k' >: t) : xs) x) -> (Membership xs kv -> Instruction ((k' >: t) : xs) x) -> Instruction ((k' >: t) : xs) x forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership ((k >: s) : xs) kv i (\kv :~: (k >: s) Refl -> Membership ((k' >: t) : xs) (k' >: t) -> TargetOf (k' >: t) x -> Instruction ((k' >: t) : xs) x forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership ((k' >: t) : xs) (k' >: t) forall k (x :: k) (xs :: [k]). Membership (x : xs) x leadership (TargetOf (k' >: t) x -> Instruction ((k' >: t) : xs) x) -> TargetOf (k' >: t) x -> Instruction ((k' >: t) : xs) x forall a b. (a -> b) -> a -> b $ s x -> t x forall x. s x -> t x f s x TargetOf kv x t) (\Membership xs kv j -> Membership ((k' >: t) : xs) kv -> TargetOf kv x -> Instruction ((k' >: t) : xs) x forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction (Membership xs kv -> Membership ((k' >: t) : xs) kv forall k (xs :: [k]) (y :: k) (x :: k). Membership xs y -> Membership (x : xs) y nextMembership Membership xs kv j) TargetOf kv x t) -- | Take a function and applies it to an Either effect iff the effect takes the form Left _. mapLeftEff :: (e -> e') -> Eff ((k >: EitherEff e) ': xs) a -> Eff ((k >: EitherEff e') ': xs) a mapLeftEff :: (e -> e') -> Eff ((k >: EitherEff e) : xs) a -> Eff ((k >: EitherEff e') : xs) a mapLeftEff e -> e' f = (forall x. EitherEff e x -> EitherEff e' x) -> Eff ((k >: EitherEff e) : xs) a -> Eff ((k >: EitherEff e') : xs) a forall k (s :: * -> *) (t :: * -> *) (k :: k) (xs :: [Assoc k (* -> *)]) a (k' :: k). (forall x. s x -> t x) -> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a mapHeadEff ((e -> e') -> Const e x -> Const e' x forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first e -> e' f) -- | Run a computation until the first call of 'tickEff'. runIterEff :: Eff (k >: Identity ': xs) a -> Eff xs (Either a (Eff (k >: Identity ': xs) a)) runIterEff :: Eff ((k >: Identity) : xs) a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) runIterEff Eff ((k >: Identity) : xs) a m = case Eff ((k >: Identity) : xs) a -> MonadView (Instruction ((k >: Identity) : xs)) (Skeleton (Instruction ((k >: Identity) : xs))) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff ((k >: Identity) : xs) a m of Return a a -> Either a (Eff ((k >: Identity) : xs) a) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall (m :: * -> *) a. Monad m => a -> m a return (a -> Either a (Eff ((k >: Identity) : xs) a) forall a b. a -> Either a b Left a a) Instruction Membership ((k >: Identity) : xs) kv i TargetOf kv a t :>>= a -> Eff ((k >: Identity) : xs) a k -> Membership ((k >: Identity) : xs) kv -> ((kv :~: (k >: Identity)) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> (Membership xs kv -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership ((k >: Identity) : xs) kv i (\kv :~: (k >: Identity) Refl -> Either a (Eff ((k >: Identity) : xs) a) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall (m :: * -> *) a. Monad m => a -> m a return (Either a (Eff ((k >: Identity) : xs) a) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> Either a (Eff ((k >: Identity) : xs) a) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall a b. (a -> b) -> a -> b $ Eff ((k >: Identity) : xs) a -> Either a (Eff ((k >: Identity) : xs) a) forall a b. b -> Either a b Right (Eff ((k >: Identity) : xs) a -> Either a (Eff ((k >: Identity) : xs) a)) -> Eff ((k >: Identity) : xs) a -> Either a (Eff ((k >: Identity) : xs) a) forall a b. (a -> b) -> a -> b $ a -> Eff ((k >: Identity) : xs) a k (a -> Eff ((k >: Identity) : xs) a) -> a -> Eff ((k >: Identity) : xs) a forall a b. (a -> b) -> a -> b $ Identity a -> a forall a. Identity a -> a runIdentity Identity a TargetOf kv a t) ((Membership xs kv -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> (Membership xs kv -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall a b. (a -> b) -> a -> b $ \Membership xs kv j -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (Either a (Eff ((k >: Identity) : xs) a)) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) (Either a (Eff ((k >: Identity) : xs) a)) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (Either a (Eff ((k >: Identity) : xs) a)) -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv j TargetOf kv a t Instruction xs a -> (a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (Either a (Eff ((k >: Identity) : xs) a)) forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= Eff ((k >: Identity) : xs) a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall k (k :: k) (xs :: [Assoc k (* -> *)]) a. Eff ((k >: Identity) : xs) a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) runIterEff (Eff ((k >: Identity) : xs) a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a))) -> (a -> Eff ((k >: Identity) : xs) a) -> a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)) forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: Identity) : xs) a k -- | Place a continuation-passing action. contEff :: Lookup xs k (ContT r m) => Proxy k -> ((a -> m r) -> m r) -> Eff xs a contEff :: Proxy k -> ((a -> m r) -> m r) -> Eff xs a contEff Proxy k k = Proxy k -> ContT r m a -> Eff xs a forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a. Lookup xs s t => Proxy s -> t a -> Eff xs a liftEff Proxy k k (ContT r m a -> Eff xs a) -> (((a -> m r) -> m r) -> ContT r m a) -> ((a -> m r) -> m r) -> Eff xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . ((a -> m r) -> m r) -> ContT r m a forall k (r :: k) (m :: k -> *) a. ((a -> m r) -> m r) -> ContT r m a ContT -- | Unwrap a continuation. runContEff :: forall k r xs a. Eff (k >: ContT r (Eff xs) ': xs) a -> (a -> Eff xs r) -> Eff xs r runContEff :: Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r runContEff Eff ((k >: ContT r (Eff xs)) : xs) a m a -> Eff xs r cont = case Eff ((k >: ContT r (Eff xs)) : xs) a -> MonadView (Instruction ((k >: ContT r (Eff xs)) : xs)) (Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs))) a forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a debone Eff ((k >: ContT r (Eff xs)) : xs) a m of Return a a -> a -> Eff xs r cont a a Instruction Membership ((k >: ContT r (Eff xs)) : xs) kv i TargetOf kv a t :>>= a -> Eff ((k >: ContT r (Eff xs)) : xs) a k -> Membership ((k >: ContT r (Eff xs)) : xs) kv -> ((kv :~: (k >: ContT r (Eff xs))) -> Eff xs r) -> (Membership xs kv -> Eff xs r) -> Eff xs r forall k (y :: k) (xs :: [k]) (x :: k) r. Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r testMembership Membership ((k >: ContT r (Eff xs)) : xs) kv i (\kv :~: (k >: ContT r (Eff xs)) Refl -> ContT r (Eff xs) a -> (a -> Eff xs r) -> Eff xs r forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r runContT TargetOf kv a ContT r (Eff xs) a t ((Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r) -> (a -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) a -> Eff xs r forall a b c. (a -> b -> c) -> b -> a -> c flip Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a. Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r runContEff a -> Eff xs r cont (Eff ((k >: ContT r (Eff xs)) : xs) a -> Eff xs r) -> (a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> a -> Eff xs r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: ContT r (Eff xs)) : xs) a k)) ((Membership xs kv -> Eff xs r) -> Eff xs r) -> (Membership xs kv -> Eff xs r) -> Eff xs r forall a b. (a -> b) -> a -> b $ \Membership xs kv j -> MonadView (Instruction xs) (Eff xs) r -> Eff xs r forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction xs) (Eff xs) r -> Eff xs r) -> MonadView (Instruction xs) (Eff xs) r -> Eff xs r forall a b. (a -> b) -> a -> b $ Membership xs kv -> TargetOf kv a -> Instruction xs a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership xs kv j TargetOf kv a t Instruction xs a -> (a -> Eff xs r) -> MonadView (Instruction xs) (Eff xs) r forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= (Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r) -> (a -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) a -> Eff xs r forall a b c. (a -> b -> c) -> b -> a -> c flip Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a. Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r runContEff a -> Eff xs r cont (Eff ((k >: ContT r (Eff xs)) : xs) a -> Eff xs r) -> (a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> a -> Eff xs r forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Eff ((k >: ContT r (Eff xs)) : xs) a k -- | Call a function with the current continuation as its argument callCCEff :: Proxy k -> ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> Eff ((k >: ContT r (Eff xs)) : xs) a callCCEff :: Proxy k -> ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> Eff ((k >: ContT r (Eff xs)) : xs) a callCCEff Proxy k k (a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a f = Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a. Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a contHead Proxy k k (ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> (((a -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) a) -> ((a -> Eff xs r) -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) a forall b c a. (b -> c) -> (a -> b) -> a -> c . ((a -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) a forall k (r :: k) (m :: k -> *) a. ((a -> m r) -> m r) -> ContT r m a ContT (((a -> Eff xs r) -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> ((a -> Eff xs r) -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) a forall a b. (a -> b) -> a -> b $ \a -> Eff xs r c -> Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a. Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r runContEff ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a f (\a x -> Proxy k -> ContT r (Eff xs) b -> Eff ((k >: ContT r (Eff xs)) : xs) b forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a. Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a contHead Proxy k k (ContT r (Eff xs) b -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> (((b -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) b) -> ((b -> Eff xs r) -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) b forall b c a. (b -> c) -> (a -> b) -> a -> c . ((b -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) b forall k (r :: k) (m :: k -> *) a. ((a -> m r) -> m r) -> ContT r m a ContT (((b -> Eff xs r) -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> ((b -> Eff xs r) -> Eff xs r) -> Eff ((k >: ContT r (Eff xs)) : xs) b forall a b. (a -> b) -> a -> b $ \b -> Eff xs r _ -> a -> Eff xs r c a x)) a -> Eff xs r c where contHead :: Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) ': xs) a contHead :: Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a contHead Proxy k _ ContT r (Eff xs) a c = MonadView (Instruction ((k >: ContT r (Eff xs)) : xs)) (Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs))) a -> Eff ((k >: ContT r (Eff xs)) : xs) a forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a boned (MonadView (Instruction ((k >: ContT r (Eff xs)) : xs)) (Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs))) a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> MonadView (Instruction ((k >: ContT r (Eff xs)) : xs)) (Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs))) a -> Eff ((k >: ContT r (Eff xs)) : xs) a forall a b. (a -> b) -> a -> b $ Membership ((k >: ContT r (Eff xs)) : xs) (k >: ContT r (Eff xs)) -> TargetOf (k >: ContT r (Eff xs)) a -> Instruction ((k >: ContT r (Eff xs)) : xs) a forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a. Membership xs kv -> TargetOf kv a -> Instruction xs a Instruction Membership ((k >: ContT r (Eff xs)) : xs) (k >: ContT r (Eff xs)) forall k (x :: k) (xs :: [k]). Membership (x : xs) x leadership TargetOf (k >: ContT r (Eff xs)) a ContT r (Eff xs) a c Instruction ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> MonadView (Instruction ((k >: ContT r (Eff xs)) : xs)) (Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs))) a forall (t :: * -> *) a (m :: * -> *) x. t a -> (a -> m x) -> MonadView t m x :>>= a -> Eff ((k >: ContT r (Eff xs)) : xs) a forall (m :: * -> *) a. Monad m => a -> m a return