Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
In brief
Bluefin is an effect system which allows you to freely mix a variety of effects, including
- Bluefin.EarlyReturn, for early return
- Bluefin.Exception, for exceptions
- Bluefin.IO, for I/O
- Bluefin.State, for mutable state
- Bluefin.Stream, for streams
and to create your own effects in terms of existing ones (Bluefin.Compound). Bluefin effects are accessed explicitly through value-level handles.
Introduction
Bluefin is a Haskell effect system with a new style of API.
It is distinct from prior effect systems because effects are
accessed explicitly through value-level handles which occur as
arguments to effectful operations. Handles (such as
State
handles, which allow access to mutable
state) are introduced by handlers (such as
evalState
, which sets the initial state).
Here's an example where a mutable state effect handle, sn
, is
introduced by its handler, evalState
.
-- Ifn < 10
then add 10 to it, otherwise -- return it unchanged example1 :: Int -> Int example1 n =runPureEff
$ -- Create a new state handle, sn, and -- initialize the value of the state to nevalState
n $ \sn -> do n' <-get
sn when (n' < 10) $modify
sn (+ 10) get sn
>>> example1 5 15 >>> example1 12 12
The handle sn
is used in much the same way as an
STRef
or IORef
.
Multiple effects of the same type
A benefit of value-level effect handles is that it's simple to have multiple effects of the same type in scope at the same time. It is simple to disambiguate them, because they are distinct values! By contrast, existing effect systems require the disambiguation to occur at the type level, which imposes challenges.
Here is a Bluefin example with two mutable Int
state effects
in scope.
-- Compare two values and add 10 -- to the smaller example2 :: (Int, Int) -> (Int, Int) example2 (m, n) =runPureEff
$evalState
m $ \sm -> do evalState n $ \sn -> do do n' <-get
sn m' <- get sm if n' < m' thenmodify
sn (+ 10) else modify sm (+ 10) n' <- get sn m' <- get sm pure (n', m')
>>> example2 (5, 10) (15, 10) >>> example2 (30, 3) (30, 13)
Exception handles
Bluefin exceptions are accessed through
Exception
handles. An Exception
handle
is introduced by a handler, such as try
,
and that handler is where the exception, if thrown, will be
handled. This arrangement differs from normal Haskell
exceptions in two ways. Firstly, every Bluefin exception will
be handled – it is not possible to have an unhandled Bluefin
exception. Secondly, a Bluefin exception can be handled in
only one place – normal Haskell exceptions can be handled in a
variety of places, and the closest handler of matching type on
the stack will be the one that will be chosen upon
throw
.
example3
shows how to use Bluefin to calculate the sum of
numbers from 1 to n
, but stop if the sum becomes bigger than
20. The exception handle, ex
, which has type Exception
String e
, cannot escape the scope of its handler, try
. If
thrown it will be handled at that try
, and nowhere else.
example3 :: Int -> Either String Int example3 n =runPureEff
$try
$ \ex -> doevalState
0 $ \total -> do for_ [1..n] $ \i -> do soFar <-get
total when (soFar > 20) $ dothrow
ex ("Became too big: " ++ show soFar)put
total (soFar + i)get
total
>>> example3 4 Right 10 >>> example3 10 Left "Became too big: 21"
Effect scoping
Bluefin's use of the type system is very similar to Control.Monad.ST: it ensures that a handle can never escape the scope of its handler. That is, once the handler has finished running there is no way you can use the handle anymore.
Type signatures
The type signatures of Bluefin functions follow a common pattern which looks like
(e1 :> es, ...) -> <Handle> e1 -> ... -> Eff es r
Here <Handle>
could be, for example, State Int
,
Exception String
or IOE
. Consider the function below,
incrementReadLine
. It reads integers from standard input,
accumulates them into a state; it returns when it reads the
input integer 0
and it throws an exception if it encounters
an input line it cannot parse.
Firstly, let's look at the arguments, which are all handles to
Bluefin effects. There is a state handle, an exception handle,
and an IO handle, which allow modification of an Int
state,
throwing a String
exception, and performing IO
operations
respectively. They are each tagged with a different effect
type, e1
, e2
and e3
respectively, which are always kept
polymorphic.
Secondly, let's look at the return value, Eff es ()
. This
means the computation is performed in the Eff
monad and the resulting value produced is of type ()
. Eff
is tagged with the effect type es
, which is also always kept
polymorphic.
Finally, let's look at the constraints. They are what tie
together the effect tags of the arguments to the effect tag of
the result. For every argument effect tag en
we have a
constraint en :> es
. That tells us the that effect handle
with tag en
is allowed to be used within the effectful
computation. If we didn't have the e1 :> es
constraint, for
example, that would tell us that the State Int e1
isn't
actually used anywhere in the computation.
GHC and editor tools like HLS do a good job of inferring these type signatures.
incrementReadLine :: (e1 :> es, e2 :> es, e3 :> es) => State Int e1 -> Exception String e2 -> IOE e3 -> Eff es () incrementReadLine state exception io = dowithJump
$ \break ->forever
$ do line <-effIO
io getLine i <- casereadMaybe
line of Nothing ->throw
exception ("Couldn't read: " ++ line) Just i -> pure i when (i == 0) $jumpTo
breakmodify
state (+ i)
Now let's look at how we can run such a function. Each effect
must be handled by a corresponding handler, for example
runState
for the state effect,
try
for the exception effect and
runEff
for the IO
effect. The type signatures
of handlers also follow a common pattern, which looks like
(forall e. <Handle> e -> Eff (e :& es) a) -> Eff es r
This means that the effect e
, corresponding to the handle
<Handle> e
, has been handled and removed from the set of
remaining effects, es
. (The signatures for
runEff
and runPureEff
are slightly
different because they remove Eff
itself.) Here, then, is
how we can run incrementReadLine
:
runIncrementReadLine :: IO (Either String Int) runIncrementReadLine =runEff
$ \io -> dotry
$ \exception -> do ((), r) <-runState
0 $ \state -> do incrementReadLine state exception io pure r >>> runIncrementReadLine 1 2 3 0 Right 6 >>>> runIncrementReadLine 1 2 3 Hello Left "Couldn't read: Hello"
Comparison to other effect systems
Everything except effectful
The design of Bluefin is strongly inspired by and based on effectful. All the points in effectful's comparison of itself to other effect systems apply to Bluefin too.
effectful
The major difference between Bluefin and effectful is that in
Bluefin effects are represented as value-level handles whereas
in effectful they are represented only at the type level.
effectful could be described as "a well-typed implementation of
the ReaderT
IO
pattern", and Bluefin could be described as
a well-typed implementation of something even simpler: the
Handle
pattern.
The aim of the Bluefin style of value-level effect tracking is
to make it even easier to mix effects, especially effects of
the same type. Only time will tell which approach is preferable
in practice.
"Why not just implement Bluefin as an alternative API on top of effectful?"
It would be great to share code between the two projects! But I don't know to implement Bluefin's Bluefin.Compound effects in effectful.
Implementation
Bluefin has a similar implementation style to effectful.
Eff
is an opaque wrapper around IO
,
State
is an opaque wrapper around
IORef
, and throw
throws an
actual IO
exception. Coroutine
is
implemented simply as a function.
newtypeEff
(es ::Effects
) a =UnsafeMkEff
(IO a) newtypeState
s (st :: Effects) =UnsafeMkState
(IORef s) newtypeCoroutine
a b (s :: Effects) =UnsafeMkCoroutine
(a -> IO b)
The type parameters of kind Effects
are phantom
type parameters which track which effects can be used in an
operation. Bluefin uses them to ensure that effects cannot
escape the scope of their handler, in the same way that the
type parameter to the ST
monad ensures that
mutable state references cannot escape
runST
. When the type system indicates that
there are no unhandled effects it is safe to run the underlying
IO
action using unsafePerformIO
, which is
the approach taken to implement runPureEff
.
Consequently, it is impossible for a pure value retured from
runPureEff
to access any Bluefin internal state or throw a
Bluefin internal exception.
Tips
- Use
NoMonoLocalBinds
andNoMonomorphismRestriction
for better type inference. (You can always change back to the default after adding inferred type signatures.) - Writing a handler often requires an explicit type signature.
Creating your own effects
See Bluefin.Compound.
Example
countPositivesNegatives :: [Int] -> String countPositivesNegatives is =runPureEff
$evalState
(0 :: Int) $ \positives -> do r <-try
$ \ex -> evalState (0 :: Int) $ \negatives -> do for_ is $ \i -> do case compare i 0 of GT ->modify
positives (+ 1) EQ -> throw ex () LT -> modify negatives (+ 1) p <-get
positives n <- get negatives pure $ "Positives: " ++ show p ++ ", negatives " ++ show n case r of Right r' -> pure r' Left () -> do p <- get positives pure $ "We saw a zero, but before that there were " ++ show p ++ " positives"