Control.Monad.Hefty

Heftia is an extensible effects library that generalizes "Algebraic Effects and Handlers" to higher-order effects, providing users with maximum flexibility and delivering standard and reasonable speed. In its generalization, the focus is on ensuring predictable results based on simple, consistent semantics, while preserving soundness.

Basic Usage

The following is an example of defining, using, and interpreting the first-order effect Log for logging and the higher-order effect Span for representing named spans in a program.

import Control.Monad.Hefty
import Prelude hiding (log, span)

data Log a where
    Log :: String -> Log ()
makeEffectF [''Log]

data Span m (a :: Type) where
    Span :: String -> m a -> Span m a
makeEffectH [''Span]

runLog :: (IO <| ef) => Eff eh (Log ': ef) ~> Eff eh ef
runLog = interpret \(Log msg) -> liftIO $ putStrLn $ "[LOG] " <> msg

runSpan :: (IO <| ef) => Eff (Span ': eh) ef ~> Eff eh ef
runSpan = interpretH \(Span name m) -> do
    liftIO $ putStrLn $ "[Start span '" <> name <> "']"
    r <- m
    liftIO $ putStrLn $ "[End span '" <> name <> "']"
    pure r

prog :: IO ()
prog = runEff . runLog . runSpan $ do
    span "example program" do
        log "foo"

        span "greeting" do
            log "hello"
            log "world"

        log "bar"

>>> prog
[Start span 'example program']
[LOG] foo
[Start span 'greeting']
[LOG] hello
[LOG] world
[End span 'greeting']
[LOG] bar
[End span 'example program']

• When defining effects, you use the Template Haskell functions makeEffectF and makeEffectH.
• The first Eff type parameter is a type-level list of higher-order effects, the second is for first-order effects.

Glossary

Handler

Interpreter for first-order effects.

Elaborator

Interpreter for higher-order effects.

Elaboration is generally performed by editing first-order (or higher-order) effectful operations within the computation held by the higher-order effect being elaborated.

runCatch :: (Throw e <| ef) => Eff '[Catch e] ef ~> Eff '[] ef
runCatch = interpretH elabCatch

elabCatch :: (Throw e <| ef) => Catch e ~~> Eff '[] ef
elabCatch (Catch action hdl) = action & interposeWith \(Throw e) _ -> hdl e

Here, elabCatch is the elaborator for the Catch effect.

Interpretation / Handling / Elaboration

The act of performing interpretation, or the process thereof.

Also, an interpreter function refers to a function represented by a natural transformation ~> or of type Interpreter, that is, one that takes an effectful operation as an argument. On the other hand, when we say interpretation function, we mean a function of the form Eff eh ef ~> Eff eh' ef', that is, one that takes the Eff monad as an argument. In the previous example, elabCatch is the interpreter function for the Catch effect, and runCatch is the interpretation function for the Catch effect.

The interpretation function may also be called an interpreter.

Continuational stateful interpreter

An interpreter function that realizes features related to the continuation in algebraic effects.

It is a function that takes two arguments: an effectful operation and a continuation, which is the continuation of the computation from that operation, and returns the computation up to the end of the computation being interpreted.

By ignoring the continuation argument, it allows for global escapes like the Throw effect.

runThrow :: Eff '[] (Throw e ': r) a -> Eff '[] r (Either e a)
runThrow = interpretBy (pure . Right) handleThrow

handleThrow :: Interpreter (Throw e) (Eff '[] r) (Either e a)
handleThrow (Throw e) _ = pure $ Left e

Here, handleThrow is the continuational stateful handler for the Throw effect.

By calling the continuation argument multiple times, it allows for non-deterministic computations like the Data.Effect.NonDet effect.

runNonDet
    :: forall f ef a
    . (Alternative f)
    => Eff '[] (Choose ': Empty ': ef) a
    -> Eff '[] ef (f a)
runNonDet =
    bundleN @2
        >>> interpretBy
            (pure . pure)
            ( (\Choose k -> liftA2 (<|>) (k False) (k True))
                !+ (\Empty _ -> pure empty)
                !+ nil
            )

The function passed as the second argument to interpretBy is the continuational stateful handler.

Additionally, what is passed as the first argument to interpretBy is called a value handler. This extends the continuation in the computation being interpreted.

Continuational state

The state of the computation that appears through interpretation, behaving based on continuation-based semantics.

Naming Rules for Interpretation Functions

• Functions with an H, such as interpretH, are for higher-order effects, while those without are for first-order effects.

  interpret :: e ~> Eff eh ef -> Eff (e ': eh) ef ~> Eff eh ef
  interpretH :: e (Eff eh ef) ~> Eff eh ef -> Eff (e ': eh) ef ~> Eff eh ef
  

  Note: ~> binds more tightly than ->.

• Functions may additionally have With or By at the end of their names.

  • These provide functionality equivalent to "Algebraic Effects and Handlers," meaning they offer access to delimited continuations during interpretation.
  • Functions in the By family take two arguments: a value handler and a continuational stateful effect interpreter. They are the most generalized form.
  • Functions in the With family omit the value handler and take only the effect interpreter as an argument.
  • The difference between interpretBy ret f m and interpretWith f m >>= ret is that, during interpretation, the delimited continuation passed as the second argument k to f in the former extends up to when ret finishes, whereas in the latter, it only goes until m finishes (just before ret), so ret is not included in k.
  • Functions without With or By cannot manipulate continuations; therefore, you cannot maintain internal state or perform behaviors like global escapes or non-deterministic computations during interpretation.

• Functions that perform recursive continuational stateful interpretation have Rec additionally added.

  • Non-recursive continuational stateful interpretation functions like interpretWith cannot be used unless the higher-order effects are empty:

    interpretWith :: e ~> Eff '[] ef => Eff '[] (e ': ef) ~> Eff '[] ef
    

  • The Rec versions can be used even when eh is not empty.

    interpretRecWith :: e ~> Eff eh (e ': ef) ~> Eff eh ef
    

  • When using this type of function, pay attention to their reset semantics. This is discussed later.
  • In principle, they cannot take value handlers, so there is no combination with By.

Function names combine the above three attributes. Examples of complex combinations include interpretHBy and interpretRecHWith.

Semantics of effects

Consider the following example.

data SomeEff a where
    SomeAction :: SomeEff String
makeEffectF [''SomeEff]

-- | Throws an exception when 'SomeAction' is encountered
runSomeEff :: (Throw String <| ef) => Eff eh (SomeEff ': ef) ~> Eff eh ef
runSomeEff = interpret \SomeAction -> throw "not caught"

-- | Catches the exception if 'someAction' results in one
action :: (SomeEff <| ef, Catch String <<| eh, Throw String <| ef) => Eff eh ef
action = someAction `catch` \(_ :: String) -> pure "caught"

prog1 :: IO ()
prog1 = runPure . runThrow @String . runCatch @String . runSomeEff $ action

>>> prog1
Right "caught"

prog2 :: IO ()
prog2 = runPure . runThrow @String . runSomeEff . runCatch @String $ action

>>> prog2
Left "not caught"

When applying runCatch after runSomeEff in prog1, the exception is caught, but in the reverse order, it is not caught. We will now explain this behavior to understand it.

In Heftia, the behavior of higher-order effects is based on reduction semantics—that is, term rewriting semantics similar to those in "Algebraic Effects and Handlers." By properly understanding and becoming familiar with this semantics, users can quickly and easily predict execution results.

Let's revisit the definition of runCatch:

runCatch :: (Throw e <| ef) => Eff '[Catch e] ef ~> Eff '[] ef
runCatch = interpretH elabCatch

elabCatch :: (Throw e <| ef) => Catch e ~~> Eff '[] ef
elabCatch (Catch action hdl) = action & interposeWith \(Throw e) _ -> hdl e

When runCatch encounters code like ... (action `catch` hdl) ... in the program, it rewrites that part to ... (interposeWith (\(Throw e) _ -> hdl e) action) .... In general, functions like interpretH and interposeH behave this way—they recursively rewrite the target higher-order effects according to the given elaborator. Rewriting proceeds from the deepest scope toward the outer scopes.

The same applies to first-order effects. Handling an effect means rewriting the effects that appear in the program.

With this in mind, let's follow the rewriting step by step.

Looking at prog1. First, when runSomeEff is applied to action:

    runSomeEff action
 =  interpret (\SomeAction -> throw "not caught") $ someAction `catch` \(_ :: String) -> pure "caught"
==> throw "not caught" `catch` \(_ :: String) -> pure "caught"

The program is rewritten into a program like the above.

Next, when runCatch is applied to this, it evaluates to:

    runCatch @String $ throw "not caught" `catch` \(_ :: String) -> pure "caught"
==> interposeWith (\(Throw e) _ -> pure "caught") $ throw "not caught"
==> pure "caught"

In this way, the exception is caught.

On the other hand, in prog2, when runCatch is applied to action:

    runCatch @String action
 =  runCatch @String $ someAction `catch` \(_ :: String) -> pure "caught"
==> interposeWith (\(@Throw e) _ -> pure "caught") $ someAction

At this point, since there is no throw in the computation that is the target of interposeWith (only someAction appears, which is not throw!), interposeWith does nothing because there is no throw to rewrite:

==> someAction

Therefore, when runSomeEff is applied:

    runSomeEff someAction
==> throw "not caught"

Thus, the exception remains as is.

In other words, in prog2, at the point of runCatch, it is impossible for runCatch to know that someAction will later be rewritten into throw. Interpreters decide what to do based only on the current state of the program's rewriting. They do not change the result based on any other information.

This is all there is to the reduction semantics of algebraic effects.

Independence from IO Semantics

As seen in the initial example with logs and spans, IO operations are embedded as effects. Not limited to IO, any monad can be embedded as an effect.

Embedded IO can be viewed as instruction scripts, and to avoid confusion when using Heftia, it should be regarded as such. Rather than thinking "Haskell represents side effects via a type-level tag called IO", it's better to think:

• Haskell is a purely functional language where you cannot write anything other than pure functions.
• IO is just an opaque algebraic data type whose definition you cannot see, no different from others.
• The runtime system treats the value main as a sequence of instructions to be executed on the CPU.
• Programming with side effects in Haskell is meta-programming where you write a pure function program that outputs IO type instruction scripts.

In fact, the semantics of effects in Heftia are completely isolated from the level of IO. Considerations at the IO level, such as "asynchronous exceptions might be thrown", "what is the current state of exception masking", or "this state/environment value is local and not shared between threads", have no influence on effect interpretation and need not be considered. IO is just a data type representing programs with side effects, and we are merely meta-programming it. The consistent semantics of algebraic effects prevent leaks of abstraction from the IO level.

This is a significant difference from IO-fused effect system libraries like effectful and cleff.

Reset Semantics in Recursive Continuational Stateful Interpretation

When performing recursive continuational stateful interpretation, that is, when using functions with Rec, it's necessary to understand their semantics. If you are not using Rec functions, you don't need to pay particular attention to this section.

runStateRec is a variant of runState, a handler for the State effect that can be used even when higher-order effects are unelaborated:

runStateRec :: Eff eh (State s ': ef) ~> Eff eh ef
runState :: Eff '[] (State s ': ef) ~> Eff '[] ef

runStateRec uses Rec functions internally. When a function uses Rec functions internally, it's best to reflect that in its naming.

Now, if you perform runStateRec before elaborating higher-order effects, the following occurs. Note that we are using the Log and Span effects introduced in the first example.

import Prelude hiding (log, span)

prog :: IO ()
prog = runEff do
    runLog . runSpan . runStateRec @[Int] [] $ do

        modify @[Int] (++ [1])
        log . show =<< get @[Int]

        span "A" do
            modify @[Int] (++ [2])
            log . show =<< get @[Int]

        modify @[Int] (++ [3])
        log . show =<< get @[Int]

    pure ()

>>> prog
[LOG] [1]
[Start span A]
[LOG] [1,2]
[End span A]
[LOG] [1,3]

After exiting span A, the added 2 has disappeared. As shown, state changes within the scope may not be preserved after exiting the scope.

This is a fundamental limitation of state preservation. When attempting to perform continuational stateful interpretation of an effect, if there are unelaborated higher-order effects remaining, resets of this continuational state occur for each scope of those higher-order effects. For higher-order effects that have already been elaborated and removed from the list at that point, there is naturally no impact.

This is simply because runStateRec (generally all Rec functions) recursively applies runState to the scopes of unelaborated higher-order effects. Interpretation occurs independently for each scope, and the state is not carried over.

From the perspective of shift/reset delimited continuations, this phenomenon can be seen as resets being inserted at the scopes of unelaborated higher-order effects.

Whether this behavior occurs can be determined in advance. This reset behavior occurs only when using Rec functions and when the program passed to that function performs unelaborated higher-order effects internally. The reset behavior occurs locally only at the points where those effects are performed. Whether an unelaborated higher-order effect e is performed internally can generally be determined by looking at the type signature of the effectful program. Given an effectful program p, if its type signature includes e in the list of higher-order effects, or if the constraint part includes e <<| eh or e <<: m, then you know that higher-order effect is being used. If not, e cannot be performed internally in the function p.

If you do not desire this reset behavior, you can avoid it by elaborating all higher-order effects first and emptying them when performing continuational stateful interpretation without using Rec functions:

import Prelude hiding (log, span)

prog :: IO ()
prog = runEff do
    runLog . runState @[Int] [] . runSpan $ do

        modify @[Int] (++ [1])
        log . show =<< get @[Int]

        span "A" do
            modify @[Int] (++ [2])
            log . show =<< get @[Int]

        modify @[Int] (++ [3])
        log . show =<< get @[Int]

    pure ()

>>> prog
[LOG] [1]
[Start span A]
[LOG] [1,2]
[Ene span A]
[LOG] [1,2,3]

Interpreting Multiple Effects Simultaneously

For example, consider a situation where you want to use multiple Catch effects simultaneously. The following is a case where both String and Int appear as exception types:

prog :: Eff '[Catch String, Catch Int] '[Throw String, Throw Int] ()

In this case, you may get stuck trying to use runCatch. This is because runCatch has the following type signature:

runCatch :: (Throw e <| ef) => Eff '[Catch e] ef ~> Eff '[] ef

You cannot write runCatch @Int . runCatch @String. It requires the higher-order effects to be empty after interpretation:

runCatch @String . runCatch @Int $ prog
                   ^^^^^^^^^^^^^

• Couldn't match type: '[]
                 with: '[Catch String]
  Expected: Eff '[Catch Int] ef x -> Eff '[Catch String] ef x
    Actual: Eff '[Catch Int] ef x -> Eff '[] ef x
• In the second argument of ‘(.)’, namely ‘runCatch @Int’
  In the first argument of ‘($)’, namely
    ‘runCatch @String . runCatch @Int’
  In the expression: runCatch @String . runCatch @Int $ prog

In situations like this, where you want to perform continuational stateful elaboration on multiple higher-order effects simultaneously, you generally cannot reduce the higher-order effect list step by step or via multi-staging. Instead, you need to elaborate all of them at once simultaneously.

This is possible by pattern matching on the open union of higher-order effects using the !!+ operator.

prog' :: Eff '[] '[Throw String, Throw Int] ()
prog' = interpretH (elabCatch @String !!+ elabCatch @Int !!+ nilH) . bundleAllH $ prog

bundleAllH collects the entire list of higher-order effects into a single higher-order effect using an open union.

Similarly, this can be done for first-order effects using !+, nil, and bundleAll.

Basics

data Eff (eh :: [EffectH]) (ef :: [EffectF]) a

The Eff monad represents computations with effects. It supports higher-order effects eh and first-order effects ef.

Constructors

Val a

A pure value.

Op

An effectful operation, which can be either a higher-order effect or a first-order effect.

Fields

• (Either (UnionH eh (Eff eh ef) x) (Union ef x))
• (FTCQueue (Eff eh ef) x a)

  the continuation of the operation.

Instances

MemberBy key e ef => SendFOEBy (key :: k) e (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

sendFOEBy :: e a -> Eff eh ef a

MemberHBy key e eh => SendHOEBy (key :: k) e (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

sendHOEBy :: e (Eff eh ef) a -> Eff eh ef a

(SendFOEBy ReaderKey (Ask r) (Eff eh ef), SendHOEBy ReaderKey (Local r) (Eff eh ef), SendFOEBy WriterKey (Tell w) (Eff eh ef), SendHOEBy WriterKey (WriterH w) (Eff eh ef), SendFOEBy StateKey (State s) (Eff eh ef), Monoid w) => MonadRWS r w s (Eff eh ef)

Defined in Control.Monad.Hefty.Types

e <| ef => SendFOE e (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

sendFOE :: e a -> Eff eh ef a

e <<| eh => SendHOE e (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

sendHOE :: e (Eff eh ef) a -> Eff eh ef a

(SendFOEBy ErrorKey (Throw e) (Eff eh ef), SendHOEBy ErrorKey (Catch e) (Eff eh ef)) => MonadError e (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

throwError :: e -> Eff eh ef a

catchError :: Eff eh ef a -> (e -> Eff eh ef a) -> Eff eh ef a

(SendFOEBy ReaderKey (Ask r) (Eff eh ef), SendHOEBy ReaderKey (Local r) (Eff eh ef)) => MonadReader r (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

ask :: Eff eh ef r

local :: (r -> r) -> Eff eh ef a -> Eff eh ef a

reader :: (r -> a) -> Eff eh ef a

SendFOEBy StateKey (State s) (Eff eh ef) => MonadState s (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

get :: Eff eh ef s

put :: s -> Eff eh ef ()

state :: (s -> (a, s)) -> Eff eh ef a

(SendFOEBy WriterKey (Tell w) (Eff eh ef), SendHOEBy WriterKey (WriterH w) (Eff eh ef), Monoid w) => MonadWriter w (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

writer :: (a, w) -> Eff eh ef a

tell :: w -> Eff eh ef ()

listen :: Eff eh ef a -> Eff eh ef (a, w)

pass :: Eff eh ef (a, w -> w) -> Eff eh ef a

Fail <| ef => MonadFail (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

fail :: String -> Eff eh ef a

Fix <<| eh => MonadFix (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

mfix :: (a -> Eff eh ef a) -> Eff eh ef a

IO <| ef => MonadIO (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

liftIO :: IO a -> Eff eh ef a

(Empty <| ef, ChooseH <<| eh) => Alternative (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

empty :: Eff eh ef a

(<|>) :: Eff eh ef a -> Eff eh ef a -> Eff eh ef a

some :: Eff eh ef a -> Eff eh ef [a]

many :: Eff eh ef a -> Eff eh ef [a]

Applicative (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

pure :: a -> Eff eh ef a

(<*>) :: Eff eh ef (a -> b) -> Eff eh ef a -> Eff eh ef b

liftA2 :: (a -> b -> c) -> Eff eh ef a -> Eff eh ef b -> Eff eh ef c

(*>) :: Eff eh ef a -> Eff eh ef b -> Eff eh ef b

(<*) :: Eff eh ef a -> Eff eh ef b -> Eff eh ef a

Functor (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

fmap :: (a -> b) -> Eff eh ef a -> Eff eh ef b

(<$) :: a -> Eff eh ef b -> Eff eh ef a

Monad (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

(>>=) :: Eff eh ef a -> (a -> Eff eh ef b) -> Eff eh ef b

(>>) :: Eff eh ef a -> Eff eh ef b -> Eff eh ef b

return :: a -> Eff eh ef a

(Empty <| ef, ChooseH <<| eh) => MonadPlus (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

mzero :: Eff eh ef a

mplus :: Eff eh ef a -> Eff eh ef a -> Eff eh ef a

(UnliftIO <<| eh, IO <| ef) => MonadUnliftIO (Eff eh ef)

Defined in Control.Monad.Hefty.Types

Methods

withRunInIO :: ((forall a. Eff eh ef a -> IO a) -> IO b) -> Eff eh ef b

type (:!!) = Eff infixr 4

Type-level infix operator for Eff. Allows writing eh :!! ef instead of Eff eh ef.

type (!!) (eh :: EffectH) (ef :: EffectF) = SumToRecUnionList UnionH eh :!! SumToRecUnionList Union ef infixr 5

An infix operator version of Eff for sum notation.

Example:

Span !! FileSystem + Time + Log + IO ~> IO

type (+) = (:+:) :: (Type -> Type) -> (Type -> Type) -> Type -> Type infixr 5

Sum for first-order effects.

type (:+:) = (:+:) :: ((Type -> Type) -> Type -> Type) -> ((Type -> Type) -> Type -> Type) -> (Type -> Type) -> Type -> Type

Sum for higher-order effects.

type ($) (f :: Type -> Type) a = f a infixr 3

Type-level infix applcation for functors.

type ($$) (h :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) = h f infixr 4

Type-level infix applcation for higher-order functors.

type Interpreter (e :: Type -> Type) (m :: Type -> Type) ans = forall x. e x -> (x -> m ans) -> m ans

Type alias for an interpreter function.

Interpreter e m ans transforms an effect e into a computation in m where the result type (answer type) is ans.

type Elaborator (e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) ans = Interpreter (e m) m ans

Type alias for an elaborator function.

An Elaborator is an interpreter for higher-order effects.

type (~~>) (e :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) = e f ~> f infix 2

Type alias for a natural transformation style elaborator.

send :: forall (e :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]). e <| ef => e ~> Eff eh ef

Send a first-order effect e to the Eff carrier.

sendH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). e <<| eh => e (Eff eh ef) ~> Eff eh ef

Send a higher-order effect e to the Eff carrier.

send0 :: forall e (eh :: [EffectH]) (ef :: [Type -> Type]) x. e x -> Eff eh (e ': ef) x

Send the first-order effect e at the head of the list to the Eff carrier.

send0H :: forall e (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]) x. e (Eff (e ': eh) ef) x -> Eff (e ': eh) ef x

Send the higher-order effect e at the head of the list to the Eff carrier.

sendN :: forall (i :: Nat) (ef :: [Type -> Type]) (eh :: [EffectH]). KnownNat i => ElemAt i ef ~> Eff eh ef

Send the i-th first-order effect in the list to the Eff carrier.

sendNH :: forall (i :: Nat) (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]). KnownNat i => ElemAt i eh (Eff eh ef) ~> Eff eh ef

Send the i-th higher-order effect in the list to the Eff carrier.

sendUnion :: forall (ef :: [EffectF]) a (eh :: [EffectH]). Union ef a -> Eff eh ef a

Send an open union of all first-order effects to the Eff carrier.

sendUnionBy :: forall a (eh :: [EffectH]) (ef :: [EffectF]) ans. (a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans

Send an open union of all first-order effects, along with its continuation, to the Eff carrier.

sendUnionH :: forall (eh :: [EffectH]) (ef :: [EffectF]) a. UnionH eh (Eff eh ef) a -> Eff eh ef a

Send an open union of all higher-order effects to the Eff carrier.

sendUnionHBy :: forall a (eh :: [EffectH]) (ef :: [EffectF]) ans. (a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans

Send an open union of all higher-order effects, along with its continuation, to the Eff carrier.

Interpreting effects

Running Eff

runEff :: forall (m :: Type -> Type). Monad m => Eff ('[] :: [EffectH]) '[m] ~> m

Lowers the computation into a monad m by treating the effect as a monad.

runPure :: Eff ('[] :: [EffectH]) ('[] :: [EffectF]) a -> a

Extracts the value from a computation that contains only pure values without any effect.

Standard functions

For first-order effects

interpret

Arguments

:: forall (e :: Type -> Type) (ef :: [EffectF]) (eh :: [EffectH]). (e ~> Eff eh ef)

Effect handler

-> Eff eh (e ': ef) ~> Eff eh ef

Interprets the first-order effect e at the head of the list using the provided natural transformation style handler.

interpretWith

Arguments

:: forall (e :: Type -> Type) (ef :: [EffectF]) a. Interpreter e (Eff ('[] :: [EffectH]) ef) a

Effect handler

-> Eff ('[] :: [EffectH]) (e ': ef) a

-> Eff ('[] :: [EffectH]) ef a

Interprets the first-order effect e at the head of the list using the provided continuational stateful handler.

interpretBy

Arguments

:: forall (e :: Type -> Type) (ef :: [EffectF]) ans a. (a -> Eff ('[] :: [EffectH]) ef ans)

Value handler

-> Interpreter e (Eff ('[] :: [EffectH]) ef) ans

Effect handler

-> Eff ('[] :: [EffectH]) (e ': ef) a

-> Eff ('[] :: [EffectH]) ef ans

Interprets the first-order effect e at the head of the list using the provided value handler and continuational stateful handler.

interpretRecWith

Arguments

:: forall e (ef :: [EffectF]) (eh :: [EffectH]) a. (forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)

Effect handler

-> Eff eh (e ': ef) a

-> Eff eh ef a

Interprets the first-order effect e at the head of the list using the provided continuational stateful handler.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects eh. Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.

For higher-order effects

interpretH

Arguments

:: forall (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]). HFunctor e

=> (e ~~> Eff eh ef)

Effect elaborator

-> Eff (e ': eh) ef ~> Eff eh ef

Interprets the higher-order effect e at the head of the list using the provided natural transformation style elaborator.

interpretHWith

Arguments

:: forall (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]) a. HFunctor e

=> Interpreter (e (Eff '[e] ef)) (Eff eh ef) a

Effect elaborator

-> Eff '[e] ef a

-> Eff eh ef a

Interprets the single higher-order effect e using the provided continuational stateful elaborator.

interpretHBy

Arguments

:: forall (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]) ans a. HFunctor e

=> (a -> Eff eh ef ans)

Value handler

-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans

Effect elaborator

-> Eff '[e] ef a

-> Eff eh ef ans

Interprets the single higher-order effect e using the provided value handler and continuational stateful elaborator.

interpretRecHWith

Arguments

:: forall e (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]) a. HFunctor e

=> (forall ans x. e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)

Effect elaborator

-> Eff (e ': eh) ef a

-> Eff eh ef a

Interprets the higher-order effect e at the head of the list using the provided continuational stateful elaborator.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects eh. Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.

Reinterpretation functions

For first-order effects

reinterpret :: forall (e :: Type -> Type) (ef' :: [EffectF]) (ef :: [Type -> Type]) (eh :: [EffectH]). IsSuffixOf ef ef' => (e ~> Eff eh ef') -> Eff eh (e ': ef) ~> Eff eh ef'

reinterpretN :: forall (n :: Natural) (e :: Type -> Type) (ef' :: [EffectF]) (ef :: [EffectF]) (eh :: [EffectH]). WeakenN n ef ef' => (e ~> Eff eh ef') -> Eff eh (e ': ef) ~> Eff eh ef'

reinterpretNWith :: forall (n :: Natural) (e :: Type -> Type) (ef' :: [EffectF]) (ef :: [EffectF]) a. WeakenN n ef ef' => Interpreter e (Eff ('[] :: [EffectH]) ef') a -> Eff ('[] :: [EffectH]) (e ': ef) a -> Eff ('[] :: [EffectH]) ef' a

reinterpretBy :: forall (e :: Type -> Type) (ef' :: [EffectF]) (ef :: [Type -> Type]) ans a. IsSuffixOf ef ef' => (a -> Eff ('[] :: [EffectH]) ef' ans) -> Interpreter e (Eff ('[] :: [EffectH]) ef') ans -> Eff ('[] :: [EffectH]) (e ': ef) a -> Eff ('[] :: [EffectH]) ef' ans

reinterpretNBy :: forall (n :: Natural) (e :: Type -> Type) (ef' :: [EffectF]) (ef :: [EffectF]) ans a. WeakenN n ef ef' => (a -> Eff ('[] :: [EffectH]) ef' ans) -> Interpreter e (Eff ('[] :: [EffectH]) ef') ans -> Eff ('[] :: [EffectH]) (e ': ef) a -> Eff ('[] :: [EffectH]) ef' ans

reinterpretRecWith :: forall e (ef' :: [EffectF]) (ef :: [EffectF]) (eh :: [EffectH]) a. IsSuffixOf ef ef' => (forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans) -> Eff eh (e ': ef) a -> Eff eh ef' a

reinterpretRecNWith :: forall (n :: Natural) e (ef' :: [EffectF]) (ef :: [EffectF]) (eh :: [EffectH]) a. WeakenN n ef ef' => (forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans) -> Eff eh (e ': ef) a -> Eff eh ef' a

For higher-order effects

reinterpretH :: forall (e :: (Type -> Type) -> Type -> Type) (eh :: [(Type -> Type) -> Type -> Type]) (eh' :: [EffectH]) (ef :: [EffectF]). (HFunctor e, IsSuffixOf eh eh') => (e ~~> Eff eh' ef) -> Eff (e ': eh) ef ~> Eff eh' ef

reinterpretNH :: forall (n :: Natural) (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). (HFunctor e, WeakenN n eh eh') => (e ~~> Eff eh' ef) -> Eff (e ': eh) ef ~> Eff eh' ef

reinterpretHWith :: forall (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]) a. HFunctor e => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a -> Eff '[e] ef a -> Eff eh ef a

reinterpretNHWith :: forall (n :: Natural) (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]) a. (HFunctor e, WeakenN n ('[] :: [EffectH]) eh) => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a -> Eff '[e] ef a -> Eff eh ef a

reinterpretHBy :: forall (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]) ans a. HFunctor e => (a -> Eff eh ef ans) -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans -> Eff '[e] ef a -> Eff eh ef ans

reinterpretNHBy :: forall (n :: Natural) (e :: (Type -> Type) -> Type -> Type) (eh :: [EffectH]) (ef :: [EffectF]) ans a. (HFunctor e, WeakenN n ('[] :: [EffectH]) eh) => (a -> Eff eh ef ans) -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans -> Eff '[e] ef a -> Eff eh ef ans

reinterpretRecHWith :: forall e (eh :: [(Type -> Type) -> Type -> Type]) (eh' :: [EffectH]) (ef :: [EffectF]) a. (HFunctor e, IsSuffixOf eh eh') => (forall ans x. e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans) -> Eff (e ': eh) ef a -> Eff eh' ef a

reinterpretRecNHWith :: forall (n :: Natural) e (eh :: [(Type -> Type) -> Type -> Type]) (eh' :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]) a. (HFunctor e, WeakenN n eh eh') => (forall ans x. e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans) -> Eff (e ': eh) ef a -> Eff eh' ef a

Interposition functions

For first-order effects

interpose

Arguments

:: forall (e :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]). e <| ef

=> (e ~> Eff eh ef)

Effect handler

-> Eff eh ef ~> Eff eh ef

Reinterprets (hooks) the first-order effect e in the list using the provided natural transformation style handler.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

interposeWith

Arguments

:: forall (e :: EffectF) (ef :: [EffectF]) a. e <| ef

=> Interpreter e (Eff ('[] :: [EffectH]) ef) a

Effect handler

-> Eff ('[] :: [EffectH]) ef a

-> Eff ('[] :: [EffectH]) ef a

Reinterprets (hooks) the first-order effect e in the list using the provided continuational stateful handler.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

interposeBy

Arguments

:: forall (e :: EffectF) (ef :: [EffectF]) ans a. e <| ef

=> (a -> Eff ('[] :: [EffectH]) ef ans)

Value handler

-> Interpreter e (Eff ('[] :: [EffectH]) ef) ans

Effect handler

-> Eff ('[] :: [EffectH]) ef a

-> Eff ('[] :: [EffectH]) ef ans

Reinterprets (hooks) the first-order effect e in the list using the provided value handler and continuational stateful handler.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

interposeRecWith

Arguments

:: forall e (ef :: [EffectF]) (eh :: [EffectH]) a. e <| ef

=> (forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)

Effect handler

-> Eff eh ef a

-> Eff eh ef a

Reinterprets (hooks) the first-order effect e in the list using the provided continuational stateful handler.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects eh. Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

For higher-order effects

interposeH

Arguments

:: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). (e <<| eh, HFunctor e)

=> (e ~~> Eff eh ef)

Effect elaborator

-> Eff eh ef ~> Eff eh ef

Reinterprets (hooks) the higher-order effect e in the list using the provided natural transformation style elaborator.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

interposeRecHWith

Arguments

:: forall e (eh :: [EffectH]) (ef :: [EffectF]) a. (e <<| eh, HFunctor e)

=> (forall ans x. e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)

Effect elaborator

-> Eff eh ef a

-> Eff eh ef a

Reinterprets (hooks) the higher-order effect e in the list using the provided continuational stateful elaborator.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects eh. Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

Transformation to monads

iterEffBy

Arguments

:: forall (e :: Type -> Type) m ans a. Monad m

=> (a -> m ans)

Value handler

-> Interpreter e m ans

Effect handler

-> Eff ('[] :: [EffectH]) '[e] a

-> m ans

Traverses a computation containing only a single first-order effect e using the provided value handler and continuational stateful handler, transforming it into a monad m.

iterEffHBy

Arguments

:: forall (e :: (Type -> Type) -> Type -> Type) m ans a. (Monad m, HFunctor e)

=> (a -> m ans)

Value handler

-> Interpreter (e (Eff '[e] ('[] :: [EffectF]))) m ans

Effect handler

-> Eff '[e] ('[] :: [EffectF]) a

-> m ans

Traverses a computation containing only a single higher-order effect e using the provided value handler and continuational stateful elaborator, transforming it into a monad m.

iterEffRecH

Arguments

:: forall (e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type). (Monad m, HFunctor e)

=> (e ~~> m)

Effect elaborator

-> Eff '[e] ('[] :: [EffectF]) ~> m

Traverses a computation containing only a single higher-order effect e using the provided natural transformation elaborator, transforming it into a monad m.

Traversal is performed recursively with respect to the scope of the higher-order effect e. Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.

iterEffRecHWith

Arguments

:: forall e m. (Monad m, HFunctor e)

=> (forall ans x. e m x -> (x -> m ans) -> m ans)

Effect elaborator

-> Eff '[e] ('[] :: [EffectF]) ~> m

Traverses a computation containing only a single higher-order effect e using the provided continuational stateful elaborator, transforming it into a monad m.

Traversal is performed recursively with respect to the scope of the higher-order effect e. Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.

iterEffRecHFWith

Arguments

:: forall eh ef m. (Monad m, HFunctor eh)

=> (forall ans x. eh m x -> (x -> m ans) -> m ans)

Effect elaborator

-> (forall ans x. ef x -> (x -> m ans) -> m ans)

Effect handler

-> Eff '[eh] '[ef] ~> m

Traverses a computation containing only higher-order effects eh and first-order effects ef using the provided continuational stateful elaborator, transforming it into a monad m.

Traversal is performed recursively with respect to the scopes of higher-order effects. Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.

iterEffHFBy

Arguments

:: forall (eh :: (Type -> Type) -> Type -> Type) (ef :: EffectF) m ans a. (Monad m, HFunctor eh)

=> (a -> m ans)

Value handler

-> Interpreter (eh (Eff '[eh] '[ef])) m ans

Effect elaborator

-> Interpreter ef m ans

Effect handler

-> Eff '[eh] '[ef] a

-> m ans

Traverses a computation containing only higher-order effects eh and first-order effects ef using the provided value handler, continuational stateful elaborator, and handler, transforming it into a monad m.

iterAllEffHFBy

Arguments

:: forall (eh :: [EffectH]) (ef :: [EffectF]) m ans a. Monad m

=> (a -> m ans)

Value handler

-> Interpreter (UnionH eh (Eff eh ef)) m ans

Effect elaborator

-> Interpreter (Union ef) m ans

Effect handler

-> Eff eh ef a

-> m ans

Traverses all effects using the provided value handler, continuational stateful elaborator, and handler, transforming them into a monad m.

Utilities

stateless :: forall (e :: Type -> Type) (m :: Type -> Type) ans. Monad m => (e ~> m) -> Interpreter e m ans

Lifts a natural transformation into a continuational stateful interpreter.

Ad-hoc stateful interpretation

Theses entities provides an ad-hoc specialized version to accelerate interpretations that have a single state type s, especially for effects like State or Writer.

type StateElaborator s (e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) ans = StateInterpreter s (e m) m ans

An ad-hoc stateful version of Elaborator for performance.

type StateInterpreter s (e :: Type -> Type) (m :: Type -> Type) ans = forall x. e x -> s -> (s -> x -> m ans) -> m ans

An ad-hoc stateful version of Interpreter for performance.

Interpretation functions

interpretStateBy :: forall s (e :: Type -> Type) (ef :: [EffectF]) ans a. s -> (s -> a -> Eff ('[] :: [EffectH]) ef ans) -> StateInterpreter s e (Eff ('[] :: [EffectH]) ef) ans -> Eff ('[] :: [EffectH]) (e ': ef) a -> Eff ('[] :: [EffectH]) ef ans

reinterpretStateBy :: forall s (e :: Type -> Type) (ef' :: [EffectF]) (ef :: [Type -> Type]) ans a. IsSuffixOf ef ef' => s -> (s -> a -> Eff ('[] :: [EffectH]) ef' ans) -> StateInterpreter s e (Eff ('[] :: [EffectH]) ef') ans -> Eff ('[] :: [EffectH]) (e ': ef) a -> Eff ('[] :: [EffectH]) ef' ans

interpretStateRecWith :: forall s e (ef :: [EffectF]) (eh :: [EffectH]) a. s -> (forall ans x. e x -> s -> (s -> x -> Eff eh ef ans) -> Eff eh ef ans) -> Eff eh (e ': ef) a -> Eff eh ef a

reinterpretStateRecWith :: forall s e (ef' :: [EffectF]) (ef :: [EffectF]) (eh :: [EffectH]) a. IsSuffixOf ef ef' => s -> (forall ans x. e x -> s -> (s -> x -> Eff eh ef' ans) -> Eff eh ef' ans) -> Eff eh (e ': ef) a -> Eff eh ef' a

Interposition functions

interposeStateBy :: forall s (e :: EffectF) (ef :: [EffectF]) ans a. e <| ef => s -> (s -> a -> Eff ('[] :: [EffectH]) ef ans) -> StateInterpreter s e (Eff ('[] :: [EffectH]) ef) ans -> Eff ('[] :: [EffectH]) ef a -> Eff ('[] :: [EffectH]) ef ans

Transformation to monads

iterStateAllEffHFBy :: forall s (eh :: [EffectH]) (ef :: [EffectF]) m ans a. Monad m => s -> (s -> a -> m ans) -> StateInterpreter s (UnionH eh (Eff eh ef)) m ans -> StateInterpreter s (Union ef) m ans -> Eff eh ef a -> m ans

Transforming effects

Rewriting effectful operations

transform :: forall (e :: Type -> Type) (e' :: Type -> Type) (ef :: [Type -> Type]) (eh :: [EffectH]). (e ~> e') -> Eff eh (e ': ef) ~> Eff eh (e' ': ef)

Transforms the first-order effect e at the head of the list into another first-order effect e'.

transformH :: forall (e :: (Type -> Type) -> Type -> Type) (e' :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). HFunctor e => (e (Eff (e' ': eh) ef) ~> e' (Eff (e' ': eh) ef)) -> Eff (e ': eh) ef ~> Eff (e' ': eh) ef

Transforms the higher-order effect e at the head of the list into another higher-order effect e'.

translate :: forall (e :: Type -> Type) (e' :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]). e' <| ef => (e ~> e') -> Eff eh (e ': ef) ~> Eff eh ef

Transforms the first-order effect e at the head of the list into another first-order effect e' and embeds it into the list.

If multiple instances of e' exist in the list, the one closest to the head (with the smallest index) will be targeted.

translateH :: forall (e :: (Type -> Type) -> Type -> Type) (e' :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). (e' <<| eh, HFunctor e) => (e (Eff eh ef) ~> e' (Eff eh ef)) -> Eff (e ': eh) ef ~> Eff eh ef

Transforms the higher-order effect e at the head of the list into another higher-order effect e' and embeds it into the list.

If multiple instances of e' exist in the list, the one closest to the head (with the smallest index) will be targeted.

rewrite :: forall (e :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]). e <| ef => (e ~> e) -> Eff eh ef ~> Eff eh ef

Rewrites the first-order effect e in the list.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

rewriteH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). (e <<| eh, HFunctor e) => (e (Eff eh ef) ~> e (Eff eh ef)) -> Eff eh ef ~> Eff eh ef

Rewrites the higher-order effect e in the list.

If multiple instances of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

transEff :: forall (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'

Transforms all first-order effects in the open union at once.

transEffH :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef)) -> Eff eh ef ~> Eff eh' ef

Transforms all higher-order effects in the open union at once.

transEffHF :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]) (ef' :: [EffectF]). (UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef')) -> (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh' ef'

Transforms all higher-order and first-order effects in the open union at once.

Manipulating the effect list (without rewriting effectful operations)

Insertion functions

raise :: forall (e :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]) x. Eff eh ef x -> Eff eh (e ': ef) x

Adds an arbitrary first-order effect e to the head of the list.

raises :: forall (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). IsSuffixOf ef ef' => Eff eh ef ~> Eff eh ef'

Adds multiple arbitrary first-order effects to the head of the list.

raiseN :: forall (len :: Natural) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). WeakenN len ef ef' => Eff eh ef ~> Eff eh ef'

Adds a specified number len of arbitrary first-order effects to the head of the list.

raiseUnder :: forall (e1 :: EffectF) (e2 :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]) x. Eff eh (e1 ': ef) x -> Eff eh (e1 ': (e2 ': ef)) x

Inserts an arbitrary first-order effect e2 just below the head of the list.

raisesUnder :: forall (offset :: Natural) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). WeakenUnder offset ef ef' => Eff eh ef ~> Eff eh ef'

Inserts multiple arbitrary first-order effects at a position offset steps below the head of the list.

raiseNUnder :: forall (len :: Natural) (offset :: Natural) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). WeakenNUnder len offset ef ef' => Eff eh ef ~> Eff eh ef'

Inserts len arbitrary first-order effects at a position offset steps below the head of the list.

raiseH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]) x. Eff eh ef x -> Eff (e ': eh) ef x

Adds a specified number len of arbitrary higher-order effects to the head of the list.

raisesH :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). IsSuffixOf eh eh' => Eff eh ef ~> Eff eh' ef

Inserts an arbitrary higher-order effect e2 just below the head of the list.

raiseNH :: forall (len :: Natural) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). WeakenN len eh eh' => Eff eh ef ~> Eff eh' ef

Adds a specified number len of arbitrary higher-order effects to the head of the list.

raiseUnderH :: forall (e1 :: EffectH) (e2 :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]) x. Eff (e1 ': eh) ef x -> Eff (e1 ': (e2 ': eh)) ef x

Inserts an arbitrary higher-order effect e2 just below the head of the list.

raiseNUnderH :: forall (len :: Natural) (offset :: Natural) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). WeakenNUnder len offset eh eh' => Eff eh ef ~> Eff eh' ef

Inserts len arbitrary higher-order effects at a position offset steps below the head of the list.

Merging functions

subsume :: forall (e :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]). e <| ef => Eff eh (e ': ef) ~> Eff eh ef

Merges the first first-order effect e at the head of the list into the same type of effect e that is below it.

If multiple candidates of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

subsumes :: forall (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). Strengthen ef ef' => Eff eh ef ~> Eff eh ef'

Merges multiple first-order effects at the head of the list into effects of the same types that are below them.

subsumeN :: forall (len :: Natural) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). StrengthenN len ef ef' => Eff eh ef ~> Eff eh ef'

Merges a specified number len of first-order effects at the head of the list into effects of the same types that are below them.

subsumeUnder :: forall (e2 :: EffectF) (e1 :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]). e2 <| ef => Eff eh (e1 ': (e2 ': ef)) ~> Eff eh (e1 ': ef)

Merges the first-order effect e2 located just below the head into the same type of effect e2 that is below it.

subsumesUnder :: forall (offset :: Natural) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). StrengthenUnder offset ef ef' => Eff eh ef ~> Eff eh ef'

Merges multiple first-order effects at an offset below the head into effects of the same types that are below them.

subsumeNUnder :: forall (len :: Natural) (offset :: Natural) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). StrengthenNUnder len offset ef ef' => Eff eh ef ~> Eff eh ef'

Merges len first-order effects at an offset below the head into effects of the same types that are below them.

subsumeH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). e <<| eh => Eff (e ': eh) ef ~> Eff eh ef

Merges the first higher-order effect e at the head of the list into the same type of effect e that is below it.

If multiple candidates of e exist in the list, the one closest to the head (with the smallest index) will be targeted.

subsumesH :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). Strengthen eh eh' => Eff eh ef ~> Eff eh' ef

Merges multiple higher-order effects at the head of the list into effects of the same types that are below them.

subsumeNH :: forall (len :: Natural) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). StrengthenN len eh eh' => Eff eh ef ~> Eff eh' ef

Merges a specified number len of higher-order effects at the head of the list into effects of the same types that are below them.

subsumeUnderH :: forall (e2 :: EffectH) (e1 :: EffectH) (eh :: [EffectH]) (ef :: [EffectF]). e2 <<| eh => Eff (e1 ': (e2 ': eh)) ef ~> Eff (e1 ': eh) ef

Merges the higher-order effect e2 located just below the head into the same type of effect e2 that is below it.

subsumeNUnderH :: forall (len :: Natural) (offset :: Natural) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). StrengthenNUnder len offset eh eh' => Eff eh ef ~> Eff eh' ef

Merges len higher-order effects at an offset below the head into effects of the same types that are below them.

Bundling functions

bundle :: forall (ef :: [EffectF]) (bundle :: [EffectF]) (rest :: [EffectF]) (eh :: [EffectH]). Split ef bundle rest => Eff eh ef ~> Eff eh (Union bundle ': rest)

Bundles several effects at the head of the list into a single element using an open union.

bundleN :: forall (len :: Nat) (ef :: [EffectF]) (eh :: [EffectH]). KnownNat len => Eff eh ef ~> Eff eh (Union (Take len ef) ': Drop len ef)

Bundles the first len effects at the head of the list into a single element using an open union.

unbundle :: forall (ef :: [EffectF]) (bundle :: [EffectF]) (rest :: [EffectF]) (eh :: [EffectH]). Split ef bundle rest => Eff eh (Union bundle ': rest) ~> Eff eh ef

Expands effects that have been bundled into an open union.

unbundleN :: forall (len :: Nat) (ef :: [EffectF]) (eh :: [EffectH]). KnownNat len => Eff eh (Union (Take len ef) ': Drop len ef) ~> Eff eh ef

Expands the first len effects that have been bundled into an open union.

bundleUnder :: forall (offset :: Natural) (bundle :: [EffectF]) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). BundleUnder Union offset ef ef' bundle => Eff eh ef ~> Eff eh ef'

Expands effects at an offset below the head of the list into a single element using an open union.

unbundleUnder :: forall (offset :: Natural) (bundle :: [EffectF]) (ef :: [EffectF]) (ef' :: [EffectF]) (eh :: [EffectH]). BundleUnder Union offset ef ef' bundle => Eff eh ef' ~> Eff eh ef

Expands effects that have been bundled into an open union at an offset below the head of the list.

bundleAll :: forall (eh :: [EffectH]) (ef :: [EffectF]) x. Eff eh ef x -> Eff eh '[Union ef] x

Bundles all first-order effects into a single open union.

unbundleAll :: forall (eh :: [EffectH]) (ef :: [EffectF]) x. Eff eh '[Union ef] x -> Eff eh ef x

Expands all first-order effects from a single open union.

bundleH :: forall (eh :: [EffectH]) (bundle :: [EffectH]) (rest :: [EffectH]) (ef :: [EffectF]). Split eh bundle rest => Eff eh ef ~> Eff (UnionH bundle ': rest) ef

Bundles several effects at the head of the list into a single element using an open union.

unbundleH :: forall (eh :: [EffectH]) (bundle :: [EffectH]) (rest :: [EffectH]) (ef :: [EffectF]). Split eh bundle rest => Eff (UnionH bundle ': rest) ef ~> Eff eh ef

Expands effects that have been bundled into an open union.

bundleUnderH :: forall (offset :: Natural) (bundle :: [EffectH]) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). BundleUnder UnionH offset eh eh' bundle => Eff eh ef ~> Eff eh' ef

Expands effects at an offset below the head of the list into a single element using an open union.

unbundleUnderH :: forall (offset :: Natural) (bundle :: [EffectH]) (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [EffectF]). BundleUnder UnionH offset eh eh' bundle => Eff eh' ef ~> Eff eh ef

Expands effects that have been bundled into an open union at an offset below the head of the list.

bundleAllH :: forall (eh :: [EffectH]) (ef :: [EffectF]) x. Eff eh ef x -> Eff '[UnionH eh] ef x

Bundles all higher-order effects into a single open union.

unbundleAllH :: forall (eh :: [EffectH]) (ef :: [EffectF]) x. Eff '[UnionH eh] ef x -> Eff eh ef x

Expands all higher-order effects from a single open union.

Manipulating Tags & Keys

tag :: forall {k} (tag :: k) (e :: EffectF) (ef :: [EffectF]) (eh :: [EffectH]) x. Eff eh (e ': ef) x -> Eff eh ((e # tag) ': ef) x

Attaches the tag to the first-order effect at the head of the list.

untag :: forall {k} (tag :: k) (e :: EffectF) (ef :: [Type -> Type]) (eh :: [EffectH]) x. Eff eh ((e # tag) ': ef) x -> Eff eh (e ': ef) x

Removes the tag from the tagged first-order effect at the head of the list.

retag :: forall {k1} {k2} (tag' :: k1) (tag :: k2) (e :: EffectF) (ef :: [Type -> Type]) (eh :: [EffectH]) x. Eff eh ((e # tag) ': ef) x -> Eff eh ((e # tag') ': ef) x

Changes the tag of the tagged first-order effect at the head of the list to another tag tag'.

tagH :: forall {k} (tag :: k) (e :: (Type -> Type) -> Type -> Type) (ef :: [EffectF]) (eh :: [(Type -> Type) -> Type -> Type]). HFunctor e => Eff (e ': eh) ef ~> Eff ((e ## tag) ': eh) ef

Attaches the tag to the higher-order effect at the head of the list.

untagH :: forall {k} (tag :: k) (e :: (Type -> Type) -> Type -> Type) (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]). HFunctor e => Eff ((e ## tag) ': eh) ef ~> Eff (e ': eh) ef

Removes the tag from the tagged higher-order effect at the head of the list.

retagH :: forall {k1} {k2} (tag' :: k1) (tag :: k2) (e :: (Type -> Type) -> Type -> Type) (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]). HFunctor e => Eff ((e ## tag) ': eh) ef ~> Eff ((e ## tag') ': eh) ef

Changes the tag of the tagged higher-order effect at the head of the list to another tag tag'.

unkey :: forall {k} (key :: k) (e :: EffectF) (ef :: [Type -> Type]) (eh :: [EffectH]) x. Eff eh ((key #> e) ': ef) x -> Eff eh (e ': ef) x

Removes the key from the keyed first-order effect at the head of the list.

rekey :: forall {k1} {k2} (key' :: k1) (key :: k2) (e :: EffectF) (ef :: [Type -> Type]) (eh :: [EffectH]) x. Eff eh ((key #> e) ': ef) x -> Eff eh ((key' #> e) ': ef) x

Changes the key of the keyed first-order effect at the head of the list to another key key'.

unkeyH :: forall {k} (key :: k) (e :: (Type -> Type) -> Type -> Type) (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]). HFunctor e => Eff ((key ##> e) ': eh) ef ~> Eff (e ': eh) ef

Removes the key from the keyed higher-order effect at the head of the list.

rekeyH :: forall {k1} {k2} (key' :: k1) (key :: k2) (e :: (Type -> Type) -> Type -> Type) (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [EffectF]). HFunctor e => Eff ((key ##> e) ': eh) ef ~> Eff ((key' ##> e) ': eh) ef

Changes the key of the keyed higher-order effect at the head of the list to another key key'.

Misc

class HFunctor (h :: (Type -> Type) -> Type -> Type)

This class represents higher-order functors (Johann, Ghani, POPL '08) which are endofunctors on the category of endofunctors.

Minimal complete definition

hfmap

Instances

() => HFunctor Fix

Defined in Data.Effect.Fix

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Fix f :-> Fix g

() => HFunctor ChooseH

Defined in Data.Effect.NonDet

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> ChooseH f :-> ChooseH g

() => HFunctor Resource

Defined in Data.Effect.Resource

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Resource f :-> Resource g

() => HFunctor Reset

Defined in Data.Effect.ShiftReset

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Reset f :-> Reset g

() => HFunctor (ChronicleH c)

Defined in Data.Effect.Chronicle

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> ChronicleH c f :-> ChronicleH c g

() => HFunctor (Thread' tid)

Defined in Data.Effect.Concurrent.Thread

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Thread' tid f :-> Thread' tid g

() => HFunctor (Catch e)

Defined in Data.Effect.Except

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Catch e f :-> Catch e g

() => HFunctor (Local r)

Defined in Data.Effect.Reader

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Local r f :-> Local r g

() => HFunctor (Shift_' b)

Defined in Data.Effect.ShiftReset

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Shift_' b f :-> Shift_' b g

() => HFunctor (UnliftBase b)

Defined in Data.Effect.Unlift

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> UnliftBase b f :-> UnliftBase b g

() => HFunctor (WriterH w)

Defined in Data.Effect.Writer

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> WriterH w f :-> WriterH w g

HFunctor (LiftFOE ins)

Defined in Data.Effect

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> LiftFOE ins f :-> LiftFOE ins g

HFunctor (UnionH es)

Defined in Data.Effect.OpenUnion.Internal.HO

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> UnionH es f :-> UnionH es g

() => HFunctor (Shift' r b)

Defined in Data.Effect.ShiftReset

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Shift' r b f :-> Shift' r b g

HFunctor (HCont ff g)

Defined in Data.Effect.HFunctor.HCont

Methods

hfmap :: forall (f :: Type -> Type) (g0 :: Type -> Type). (f :-> g0) -> HCont ff g f :-> HCont ff g g0

Functor f => HFunctor (Compose f :: (Type -> Type) -> Type -> Type)

Defined in Data.Comp.Multi.HFunctor

Methods

hfmap :: forall (f0 :: Type -> Type) (g :: Type -> Type). (f0 :-> g) -> Compose f f0 :-> Compose f g

HFunctor f => HFunctor (f :&: a)

Defined in Data.Comp.Multi.Ops

Methods

hfmap :: forall (f0 :: Type -> Type) (g :: Type -> Type). (f0 :-> g) -> (f :&: a) f0 :-> (f :&: a) g

(HFunctor f, HFunctor g) => HFunctor (f :+: g)

Defined in Data.Comp.Multi.Ops

Methods

hfmap :: forall (f0 :: Type -> Type) (g0 :: Type -> Type). (f0 :-> g0) -> (f :+: g) f0 :-> (f :+: g) g0

() => HFunctor (Provider' ctx i b)

Defined in Data.Effect.Provider

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> Provider' ctx i b f :-> Provider' ctx i b g

HFunctor sig => HFunctor (KeyH key sig)

Defined in Data.Effect.Key

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> KeyH key sig f :-> KeyH key sig g

HFunctor sig => HFunctor (TagH sig tag)

Defined in Data.Effect.Tag

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> TagH sig tag f :-> TagH sig tag g

data ReaderKey

A key to be attached to the effect targeted by the MonadReader instance.

Since MonadReader has a functional dependency on r, this is needed to uniquely specify r.

data WriterKey

A key to be attached to the effect targeted by the MonadWriter instance.

Since MonadWriter has a functional dependency on w, this is needed to uniquely specify w.

data StateKey

A key to be attached to the effect targeted by the MonadState instance.

Since MonadState has a functional dependency on s, this is needed to uniquely specify s.

data ErrorKey

A key to be attached to the effect targeted by the MonadError instance.

Since MonadError has a functional dependency on e, this is needed to uniquely specify e.

type Type = TYPE LiftedRep

The kind of types with lifted values. For example Int :: Type.

liftIO :: MonadIO m => IO a -> m a

Lift a computation from the IO monad. This allows us to run IO computations in any monadic stack, so long as it supports these kinds of operations (i.e. IO is the base monad for the stack).

Example

import Control.Monad.Trans.State -- from the "transformers" library

printState :: Show s => StateT s IO ()
printState = do
  state <- get
  liftIO $ print state

Had we omitted liftIO, we would have ended up with this error:

• Couldn't match type ‘IO’ with ‘StateT s IO’
 Expected type: StateT s IO ()
   Actual type: IO ()

The important part here is the mismatch between StateT s IO () and IO ().

Luckily, we know of a function that takes an IO a and returns an (m a): liftIO, enabling us to run the program and see the expected results:

> evalStateT printState "hello"
"hello"

> evalStateT printState 3
3

module Data.Effect.OpenUnion

module Data.Effect

module Data.Effect.TH

module Control.Effect