Named algebraic effect handlers in Bluefin
This package leverages the delimited continuations primitives added in
GHC 9.6 to implement algebraic effects in the Bluefin effect system.
Algebraic effects are a minimalistic basis for user-defined effects.
Using algebraic effects, we can reimplement, from scratch, effects that
were built-in the Bluefin library, and more.
This is an experimental project. There are surprising performance
characteristics which may be problematic for practical applications.
Details down below.
Free monads in IO
An algebraic effect library is basically a free monad library with support for
extensible effects.
Effect handlers---the core primitive of algebraic effects---are conceptually
folds of trees, aka.
iter in free
or cata in recursion-schemes.
Effect systems---such as Bluefin---enable combinations of effects within a
single parameterized monad. Bluefin Algae seamlessly integrates with Bluefin's
infrastructure in order to compose algebraic effects.
The main novelties in Bluefin Algae are:
-
computations use the same representation as IO (State# s -> (# State# s, a #))
instead of recursive types or continuation-passing encodings.
This is possible thanks to the recently available primitives for delimited
continuations.
-
thanks to Bluefin, effects are statically scoped: performing an operation
requires a handle which identifies a specific handler.
This enables new forms of abstraction boundaries.
A function Eff s a -> Eff s a cannot handle the operations of its argument.
The argument must be explicitly parameterized by the handler to allow
handling by its caller: (forall z. Handler f z -> Eff (z : s) a) -> Eff s a.
Highlights
Concurrency
In the following example, two threads yield a string back and forth, appending
a suffix every time.
import Bluefin.Algae.Coroutine
pingpong :: Eff ss String
pingpong = withCoroutine coThread mainThread
where
coThread z0 h = do
z1 <- yield h (z0 ++ "pong")
z2 <- yield h (z1 ++ "dong")
yield h (z2 ++ "bong")
mainThread h = do
s1 <- yield h "ping"
s2 <- yield h (s1 ++ "ding")
s3 <- yield h (s2 ++ "bing")
pure s3
-- runPureEff pingpong == "pingpongdingdongbingbong"
Note that coThread and mainThread are just IO computations under the hood.
And we can interleave their executions without native multithreading. This is the
power of delimited continuations.
Nondeterminism
With the ability to interrupt and resume operations freely, we can do
backtracking search in the Eff monad.
import Bluefin.Algae.NonDeterminism as NonDet
pythagoras :: z :> zz => Handler Choice z -> Eff zz (Int, Int, Int)
pythagoras choice = do
x <- pick choice [1 .. 10]
y <- pick choice [1 .. 10]
z <- pick choice [1 .. 10]
assume choice (x .^ 2 + y .^ 2 == z .^ 2)
pure (x, y, z)
where (.^) = (Prelude.^) :: Int -> Int -> Int
-- runPureEff (NonDet.toList pythagoras) == [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]
Backtracking and state
Resuming continuations more than once exposes the impurity of the
implementation of the built-in state effect in Bluefin.State.
Here is a program using nondeterminism and state. There are two branches
(choose), both modify the state (incr).
import qualified Bluefin.State as B
nsExampleB :: [Int]
nsExampleB = runPureEff $ NonDet.toList \choice ->
snd <$> B.runState 0 \state -> do
_ <- choose choice True False
B.modify (+ 1) state
-- nsExampleB == [1,2]
The state handler (runState) is under the nondeterminism handler
(NonDet.toList), which suggests a state-passing interpetation, where the
original state is restored upon backtracking (both branches return 1):
nsExamplePure :: [Int]
nsExamplePure = runPureEff $ NonDet.toList \choice ->
let state = 0 -- initial state
_ <- choose choice True False
let state' = state' + 1 -- modify' (+ 1)
pure state' -- (snd <$> runState) returns the final state
-- nsExamplePure == [1,1]
Because Bluefin.State is backed by IORef, the mutation persists
through backtracking (the second branch returns 2 in the first example).
In comparison, the state effect defined using algebraic effects
(Bluefin.Algae.State) has the state-passing semantics.
import qualified Bluefin.Algae.State as A
nsExampleA :: [Int]
nsExampleA = runPureEff $ NonDet.toList \choice ->
A.execState 0 \state -> do
_ <- choose choice True False
A.modify' (+ 1) state
-- nsExampleA == [1,1]
Truly scoped exceptions.
The scoped exceptions from Bluefin.Exception are not completely scoped because
they can be observed by bracket. That is probably the right behavior in practice,
but makes the semantics of Bluefin less clear. For the sake of science,
Bluefin.Algae.Exception provides truly scoped exceptions, and implements
"bracket-observable" scoped exceptions on top.
Lowlights
Quadratic behavior of non-tail recursion.
For example, the following recursive counter will take time quadratic in n
because every call of modify' traverses the call stack to find its handler
and capture the continuation.
leftRecCounter :: z :> zz => Handler (State Int) z -> Int -> Eff zz ()
leftRecCounter _state 0 = pure ()
leftRecCounter state n = do
leftRecCounter state (n - 1)
modify' state (+ 1)
Comparison
Bluefin
The Bluefin effect system provides a well-scoped handle pattern.
Unlike algebraic effects with which other computational effects can be
user-defined, Bluefin provides a collection of built-in effects
(state, exceptions, coroutines).
Without delimited continuations, only tail-resumptive algebraic effect handlers
are expressible in Bluefin. Those are effect handlers restricted to the
following form, which is equivalent to type forall r. f r -> Eff ss r.
(\e k -> _ >>= k)
:: forall r. f r -> (r -> Eff ss a) -> Eff ss a
More reading
Named effect handlers are described in the literature in:
