Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Semantic r a
- type Member e r = Member' e r
- run :: Semantic '[] a -> a
- runM :: Monad m => Semantic '[Lift m] a -> m a
- newtype Lift m (z :: * -> *) a where
- sendM :: Member (Lift m) r => m a -> Semantic r a
- raise :: forall e r a. Semantic r a -> Semantic (e ': r) a
- makeSemantic :: Name -> Q [Dec]
- makeSemantic_ :: Name -> Q [Dec]
- interpret :: FirstOrder e "interpret" => (forall x m. e m x -> Semantic r x) -> Semantic (e ': r) a -> Semantic r a
- intercept :: (Member e r, FirstOrder e "intercept") => (forall x m. e m x -> Semantic r x) -> Semantic r a -> Semantic r a
- reinterpret :: FirstOrder e1 "reinterpret" => (forall m x. e1 m x -> Semantic (e2 ': r) x) -> Semantic (e1 ': r) a -> Semantic (e2 ': r) a
- reinterpret2 :: FirstOrder e1 "reinterpret2" => (forall m x. e1 m x -> Semantic (e2 ': (e3 ': r)) x) -> Semantic (e1 ': r) a -> Semantic (e2 ': (e3 ': r)) a
- reinterpret3 :: FirstOrder e1 "reinterpret3" => (forall m x. e1 m x -> Semantic (e2 ': (e3 ': (e4 ': r))) x) -> Semantic (e1 ': r) a -> Semantic (e2 ': (e3 ': (e4 ': r))) a
- interpretH :: (forall x m. e m x -> Tactical e m r x) -> Semantic (e ': r) a -> Semantic r a
- interceptH :: Member e r => (forall x m. e m x -> Tactical e m r x) -> Semantic r a -> Semantic r a
- reinterpretH :: (forall m x. e1 m x -> Tactical e1 m (e2 ': r) x) -> Semantic (e1 ': r) a -> Semantic (e2 ': r) a
- reinterpret2H :: (forall m x. e1 m x -> Tactical e1 m (e2 ': (e3 ': r)) x) -> Semantic (e1 ': r) a -> Semantic (e2 ': (e3 ': r)) a
- reinterpret3H :: (forall m x. e1 m x -> Tactical e1 m (e2 ': (e3 ': (e4 ': r))) x) -> Semantic (e1 ': r) a -> Semantic (e2 ': (e3 ': (e4 ': r))) a
- inlineRecursiveCalls :: Q [Dec] -> Q [Dec]
- (.@) :: Monad m => (forall x. Semantic r x -> m x) -> (forall y. (forall x. Semantic r x -> m x) -> Semantic (e ': r) y -> Semantic r y) -> Semantic (e ': r) z -> m z
- (.@@) :: Monad m => (forall x. Semantic r x -> m x) -> (forall y. (forall x. Semantic r x -> m x) -> Semantic (e ': r) y -> Semantic r (f y)) -> Semantic (e ': r) z -> m (f z)
- type Tactical e m r x = forall f. (Functor f, Typeable1 f) => Semantic (WithTactics e f m r) (f x)
- type WithTactics e f m r = Tactics f m (e ': r) ': r
- getInitialStateT :: forall f m r e. Semantic (WithTactics e f m r) (f ())
- pureT :: a -> Tactical e m r a
- runT :: m a -> Semantic (WithTactics e f m r) (Semantic (e ': r) (f a))
- bindT :: (a -> m b) -> Semantic (WithTactics e f m r) (f a -> Semantic (e ': r) (f b))
- class Typeable (a :: k)
Core Types
The Semantic
monad handles computations of arbitrary extensible effects.
A value of type Semantic r
describes a program with the capabilities of
r
. For best results, r
should always be kept polymorphic, but you can
add capabilities via the Member
constraint.
The value of the Semantic
monad is that it allows you to write programs
against a set of effects without a predefined meaning, and provide that
meaning later. For example, unlike with mtl, you can decide to interpret an
Error
effect tradtionally as an Either
, or instead
significantly faster as an IO
Exception
. These
interpretations (and others that you might add) may be used interchangably
without needing to write any newtypes or Monad
instances. The only
change needed to swap interpretations is to change a call from
runError
to runErrorInIO
.
The effect stack r
can contain arbitrary other monads inside of it. These
monads are lifted into effects via the Lift
effect. Monadic values can be
lifted into a Semantic
via sendM
.
A Semantic
can be interpreted as a pure value (via run
) or as any
traditional Monad
(via runM
). Each effect E
comes equipped with some
interpreters of the form:
runE ::Semantic
(E ': r) a ->Semantic
r a
which is responsible for removing the effect E
from the effect stack. It
is the order in which you call the interpreters that determines the
monomorphic representation of the r
parameter.
After all of your effects are handled, you'll be left with either
a
or a Semantic
'[] a
value, which can be
consumed respectively by Semantic
'[ Lift
m ] arun
and runM
.
Examples
As an example of keeping r
polymorphic, we can consider the type
Member
(State
String) r =>Semantic
r ()
to be a program with access to
get
::Semantic
r Stringput
:: String ->Semantic
r ()
methods.
By also adding a
Member
(Error
Bool) r
constraint on r
, we gain access to the
throw
:: Bool ->Semantic
r acatch
::Semantic
r a -> (Bool ->Semantic
r a) ->Semantic
r a
functions as well.
In this sense, a
constraint is
analogous to mtl's Member
(State
s) r
and should
be thought of as such. However, unlike mtl, a MonadState
s mSemantic
monad may have
an arbitrary number of the same effect.
For example, we can write a Semantic
program which can output either
Int
s or Bool
s:
foo :: (Member
(Output
Int) r ,Member
(Output
Bool) r ) =>Semantic
r () foo = dooutput
@Int 5output
True
Notice that we must use -XTypeApplications
to specify that we'd like to
use the (Output
Int
) effect.
Instances
Monad (Semantic f) Source # | |
Functor (Semantic f) Source # | |
Member Fixpoint r => MonadFix (Semantic r) Source # | |
Defined in Polysemy.Internal | |
Applicative (Semantic f) Source # | |
Member (Lift IO) r => MonadIO (Semantic r) Source # | This instance will only lift |
Defined in Polysemy.Internal | |
Member NonDet r => Alternative (Semantic r) Source # | |
type Member e r = Member' e r Source #
A proof that the effect e
is available somewhere inside of the effect
stack r
.
Running Semantic
Interoperating With Other Monads
newtype Lift m (z :: * -> *) a where Source #
An effect which allows a regular Monad
m
into the Semantic
ecosystem. Monadic actions in m
can be lifted into Semantic
via
sendM
.
For example, you can use this effect to lift IO
actions directly into
Semantic
:
sendM
(putStrLn "hello") ::Member
(Lift
IO) r =>Semantic
r ()
That being said, you lose out on a significant amount of the benefits of
Semantic
by using sendM
directly in application code; doing so
will tie your application code directly to the underlying monad, and prevent
you from interpreting it differently. For best results, only use Lift
in
your effect interpreters.
Consider using trace
and runTraceIO
as
a substitute for using putStrLn
directly.
Lifting
Creating New Effects
Effects should be defined as a GADT (enable -XGADTs
), with kind (*
-> *) -> * -> *
. Every primitive action in the effect should be its
own constructor of the type. For example, we can model an effect which
interacts with a tty console as follows:
data Console m a where WriteLine :: String -> Console m () ReadLine :: Console m String
Notice that the a
parameter gets instataniated at the /desired return
type/ of the actions. Writing a line returns a '()', but reading one
returns String
.
By enabling -XTemplateHaskell
, we can use the makeSemantic
function
to generate smart constructors for the actions. These smart constructors
can be invoked directly inside of the Semantic
monad.
>>>
makeSemantic ''Console
results in the following definitions:
writeLine ::Member
Console r => String ->Semantic
r () readLine ::Member
Console r =>Semantic
r String
Effects which don't make use of the m
parameter are known as
"first-order effects."
Higher-Order Effects
Every effect has access to the m
parameter, which corresponds to the
Semantic
monad it's used in. Using this parameter, we're capable of
writing effects which themselves contain subcomputations.
For example, the definition of Error
is
dataError
e m a whereThrow
:: e ->Error
e m aCatch
:: m a -> (e -> m a) ->Error
e m a
where Catch
is an action that can run an exception
handler if its first argument calls throw
.
>>>
makeSemantic ''Error
throw
::Member
(Error
e) r => e ->Semantic
r acatch
::Member
(Error
e) r =>Semantic
r a -> (e ->Semantic
r a) ->Semantic
r a
As you see, in the smart constructors, the m
parameter has become
.Semantic
r
makeSemantic :: Name -> Q [Dec] Source #
If T
is a GADT representing an effect algebra, as described in the module
documentation for Polysemy, $(
automatically
generates a smart constructor for every data constructor of makeSemantic
''T)T
.
makeSemantic_ :: Name -> Q [Dec] Source #
Like makeSemantic
, but does not provide type signatures. This can be used
to attach Haddock comments to individual arguments for each generated
function.
data Lang m a where Output :: String -> Lang () makeSemantic_ ''Lang -- | Output a string. output :: Member Lang r => String -- ^ String to output. -> Semantic r () -- ^ No result.
Note that makeEffect_
must be used before the explicit type signatures.
Combinators for Interpreting First-Order Effects
:: FirstOrder e "interpret" | |
=> (forall x m. e m x -> Semantic r x) | A natural transformation from the handled effect to other effects
already in |
-> Semantic (e ': r) a | |
-> Semantic r a |
The simplest way to produce an effect handler. Interprets an effect e
by
transforming it into other effects inside of r
.
:: (Member e r, FirstOrder e "intercept") | |
=> (forall x m. e m x -> Semantic r x) | A natural transformation from the handled effect to other effects
already in |
-> Semantic r a | |
-> Semantic r a |
Like interpret
, but instead of handling the effect, allows responding to
the effect while leaving it unhandled. This allows you, for example, to
intercept other effects and insert logic around them.
:: FirstOrder e1 "reinterpret" | |
=> (forall m x. e1 m x -> Semantic (e2 ': r) x) | A natural transformation from the handled effect to the new effect. |
-> Semantic (e1 ': r) a | |
-> Semantic (e2 ': r) a |
Like interpret
, but instead of removing the effect e
, reencodes it in
some new effect f
. This function will fuse when followed by
runState
, meaning it's free to reinterpret
in terms of
the State
effect and immediately run it.
:: FirstOrder e1 "reinterpret2" | |
=> (forall m x. e1 m x -> Semantic (e2 ': (e3 ': r)) x) | A natural transformation from the handled effect to the new effects. |
-> Semantic (e1 ': r) a | |
-> Semantic (e2 ': (e3 ': r)) a |
Like reinterpret
, but introduces two intermediary effects.
:: FirstOrder e1 "reinterpret3" | |
=> (forall m x. e1 m x -> Semantic (e2 ': (e3 ': (e4 ': r))) x) | A natural transformation from the handled effect to the new effects. |
-> Semantic (e1 ': r) a | |
-> Semantic (e2 ': (e3 ': (e4 ': r))) a |
Like reinterpret
, but introduces three intermediary effects.
Combinators for Interpreting Higher-Order Effects
:: Member e r | |
=> (forall x m. e m x -> Tactical e m r x) | A natural transformation from the handled effect to other effects
already in |
-> Semantic r a | Unlike |
-> Semantic r a |
Like interceptH
, but for higher-order effects.
See the notes on Tactical
for how to use this function.
:: (forall m x. e1 m x -> Tactical e1 m (e2 ': r) x) | A natural transformation from the handled effect to the new effect. |
-> Semantic (e1 ': r) a | |
-> Semantic (e2 ': r) a |
Like reinterpret
, but for higher-order effects.
See the notes on Tactical
for how to use this function.
:: (forall m x. e1 m x -> Tactical e1 m (e2 ': (e3 ': r)) x) | A natural transformation from the handled effect to the new effects. |
-> Semantic (e1 ': r) a | |
-> Semantic (e2 ': (e3 ': r)) a |
Like reinterpret2
, but for higher-order effects.
See the notes on Tactical
for how to use this function.
:: (forall m x. e1 m x -> Tactical e1 m (e2 ': (e3 ': (e4 ': r))) x) | A natural transformation from the handled effect to the new effects. |
-> Semantic (e1 ': r) a | |
-> Semantic (e2 ': (e3 ': (e4 ': r))) a |
Like reinterpret3
, but for higher-order effects.
See the notes on Tactical
for how to use this function.
Improving Performance for Interpreters
inlineRecursiveCalls :: Q [Dec] -> Q [Dec] Source #
GHC has a really hard time inlining recursive calls---such as those used in interpreters for higher-order effects. This can have disastrous repercussions for your performance.
Fortunately there's a solution, but it's ugly boilerplate. You can enable
-XTemplateHaskell
and use inlineRecursiveCalls
to convince GHC to make
these functions fast again.
inlineRecursiveCalls
[d|runReader
:: i ->Semantic
(Reader
i ': r) a ->Semantic
r arunReader
i =interpretH
$ \caseAsk
->pureT
iLocal
f m -> do mm <-runT
mraise
$runReader
(f i) mm |]
Composing IO-based Interpreters
:: Monad m | |
=> (forall x. Semantic r x -> m x) | The lowering function, likely |
-> (forall y. (forall x. Semantic r x -> m x) -> Semantic (e ': r) y -> Semantic r y) | |
-> Semantic (e ': r) z | |
-> m z |
Some interpreters need to be able to lower down to the base monad (often
IO
) in order to function properly --- some good examples of this are
runErrorInIO
and runResource
.
However, these interpreters don't compose particularly nicely; for example,
to run runResource
, you must write:
runM . runErrorInIO runM
Notice that runM
is duplicated in two places here. The situation gets
exponentially worse the more intepreters you have that need to run in this
pattern.
Instead, .@
performs the composition we'd like. The above can be written as
(runM .@ runErrorInIO)
The parentheses here are important; without them you'll run into operator precedence errors.
:: Monad m | |
=> (forall x. Semantic r x -> m x) | The lowering function, likely |
-> (forall y. (forall x. Semantic r x -> m x) -> Semantic (e ': r) y -> Semantic r (f y)) | |
-> Semantic (e ': r) z | |
-> m (f z) |
Like .@
, but for interpreters which change the resulting type --- eg.
runErrorInIO
.
Tactics
Higher-order effects need to explicitly thread other effects' state through themselves. Tactics are a domain-specific language for describing exactly how this threading should take place.
The first computation to be run should use runT
, and subsequent
computations in the same environment should use bindT
. Any
first-order constructors which appear in a higher-order context may use
pureT
to satisfy the typechecker.
type Tactical e m r x = forall f. (Functor f, Typeable1 f) => Semantic (WithTactics e f m r) (f x) Source #
Tactical
is an environment in which you're capable of explicitly
threading higher-order effect states. This is provided by the (internal)
effect Tactics
, which is capable of rewriting monadic actions so they run
in the correct stateful environment.
Inside a Tactical
, you're capable of running pureT
, runT
and bindT
which are the main tools for rewriting monadic stateful environments.
For example, consider trying to write an interpreter for
Resource
, whose effect is defined as:
dataResource
m a whereBracket
:: m a -> (a -> m ()) -> (a -> m b) ->Resource
m b
Here we have an m a
which clearly needs to be run first, and then
subsequently call the a -> m ()
and a -> m b
arguments. In a Tactical
environment, we can write the threading code thusly:
Bracket
alloc dealloc use -> do alloc' <-runT
alloc dealloc' <-bindT
dealloc use' <-bindT
use
where
alloc' ::Semantic
(Resource
': r) (f a1) dealloc' :: f a1 ->Semantic
(Resource
': r) (f ()) use' :: f a1 ->Semantic
(Resource
': r) (f x)
The f
type here is existential and corresponds to "whatever
state the other effects want to keep track of." f
is always
a Functor
.
alloc'
, dealloc'
and use'
are now in a form that can be
easily consumed by your interpreter. At this point, simply bind
them in the desired order and continue on your merry way.
We can see from the types of dealloc'
and use'
that since they both
consume a f a1
, they must run in the same stateful environment. This
means, for illustration, any put
s run inside the use
block will not be visible inside of the dealloc
block.
Power users may explicitly use getInitialStateT
and bindT
to construct
whatever data flow they'd like; although this is usually unnecessary.
type WithTactics e f m r = Tactics f m (e ': r) ': r Source #
getInitialStateT :: forall f m r e. Semantic (WithTactics e f m r) (f ()) Source #
:: m a | The monadic action to lift. This is usually a parameter in your effect. |
-> Semantic (WithTactics e f m r) (Semantic (e ': r) (f a)) |
:: (a -> m b) | The monadic continuation to lift. This is usually a parameter in your effect. Continuations lifted via |
-> Semantic (WithTactics e f m r) (f a -> Semantic (e ': r) (f b)) |