Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Algebraic effects and named handlers
Algebraic effect handlers are a powerful framework for user-defined effects with a simple equational intuition.
Algebraic effect handlers are expressive enough to define various effects
from scratch. In comparison, the runState
handler from
Bluefin.State requires mutable references (IORef
), relying on IO
's
built-in statefulness. In terms of pure expressiveness, delimited
continuations are all you need.
An "algebraic effect" is a signature for a set of operations which we
represent with a GADT. For example, the "state effect" State s
contains
two operations: Get
takes no parameter and returns a value of type s
,
and Put
takes a value of type s
and returns ()
. The constructors
Get
and Put
are "uninterpreted operations": they only describe the types
of arguments and results, with no intrinsic meaning.
dataState
s r where Get ::State
s s Put :: s ->State
s ()
Below is an example of a stateful computation: a term of some type
with
a state handler Eff
zz ah ::
in scope (Handler
(State
s) zz :> zz
).
The State
operations can be called using call
and the state handler h
.
-- Increment a counter and return its previous value. incr :: z :> zz =>Handler
(State
Int) z ->Eff
zz Int incr h = do n <- get put (n + 1) pure n where get =call
h Get put s =call
h (Put s)
We handle the state effect by giving an interpretation of the Get
and Put
operations, as a function f ::
.HandlerBody
(State s) zz a
To call
Get
or Put
is to call the function f
supplied by handle
.
The following equations show how handle
propagates an interpretation
f
throughout a computation that calls Get
and Put
:
handle
f (\h ->call
h Get >>= k h) = f Get (handle
f (\h -> k h))handle
f (\h ->call
h (Put s) >>= k h) = f (Put s) (handle
f (\h -> k h))handle
f (\h -> pure r) = pure r
With those equations,
applied to the above handle
fincr
simplifies to:
handle
f incr =
f Get \n ->
f (Put (n+1)) \() ->
pure n
References
- Handling Algebraic Effects (2013) by Gordon D. Plotkin and Matija Pretnar.
- First-class names for effect handlers (2021) by Ningning Xie, Youyou Cong, and Daan Leijen.
Synopsis
- type AEffect = Type -> Type
- type HandlerBody f ss a = forall x. f x -> (x -> Eff ss a) -> Eff ss a
- data Handler f s
- type ScopedEff f ss a = forall s. Handler f s -> Eff (s :& ss) a
- handle :: HandlerBody f ss a -> ScopedEff f ss a -> Eff ss a
- call :: s :> ss => Handler f s -> f a -> Eff ss a
- type HandlerBody' f ss a = forall ss0 x. f x -> Continuation ss0 ss x a -> Eff ss a
- handle' :: HandlerBody' f ss a -> ScopedEff f ss a -> Eff ss a
- continue :: Continuation t s b a -> b -> Eff s a
- cancel :: Continuation t s b a -> Eff s ()
Documentation
Simple interface
type HandlerBody f ss a = forall x. f x -> (x -> Eff ss a) -> Eff ss a Source #
Interpretation of an algebraic effect f
: a function to handle the operations of f
.
handle :: HandlerBody f ss a -> ScopedEff f ss a -> Eff ss a Source #
Handle operations of f
.
Warning for exception-like effects
If the handler might not call the continuation (like for an exception effect), and
if the handled computation manages resources (e.g., opening files, transactions)
prefer handle'
to trigger resource clean up with cancellable continuations.
call :: s :> ss => Handler f s -> f a -> Eff ss a Source #
Call an operation of algebraic effect f
with a handler.
Cancellable continuations
Cancellable continuations are useful to work with resource-management schemes
with exception handlers such as bracket
Cancellable continuations should be called exactly once (via continue
or cancel
):
- at least once to ensure resources are eventually freed (no leaks);
- at most once to avoid use-after-free errors.
Enforcing this requirement with linear types would be a welcome contribution.
Example
Problem
Given bracket
and a Fail
effect,
the simple handle
may cause resource leaks:
handle
(\_e _k -> pure Nothing) (bracket
ex acquire release (\_ ->call
h Fail))
bracket
is intended to ensure that the acquired resource is
released even if the bracketed function throws an exception. However, when
the Fail
operation is called, the handler (\_e _k -> pure Nothing)
discards the continuation _k
which contains the exception handler
installed by bracket
.
The resource leaks because release
will never be called.
Solution
Using handle'
instead lets us cancel
the continuation.
handle'
(\_e k ->cancel
k >> pure Nothing) (bracket
acquire release (\_ ->call
h Fail))
type HandlerBody' f ss a = forall ss0 x. f x -> Continuation ss0 ss x a -> Eff ss a Source #
Generalization of HandlerBody
with cancellable continuations.
handle' :: HandlerBody' f ss a -> ScopedEff f ss a -> Eff ss a Source #
Generalization of handle
with cancellable continuations.
continue :: Continuation t s b a -> b -> Eff s a Source #
Resume a cancellable continuation with a result.
In other words, this converts a cancellable continuation to a simple continuation.
cancel :: Continuation t s b a -> Eff s () Source #
Cancel a continuation: resume by throwing a scoped exception and catch it.
The continuation SHOULD re-throw unknown exceptions. (That is guaranteed if you don't use Exception.Dynamic.)