{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE LambdaCase #-}
-- ------------------------------------------------------------------------
-- | A monadic library for communication between a handler and
-- its client, the administered computation
--
-- Original work available at .
-- This module implements extensible effects as an alternative to monad transformers,
-- as described in and
-- .
--
-- Extensible Effects are implemented as typeclass constraints on an Eff[ect] datatype.
-- A contrived example can be found under "Control.Eff.Example". To run the
-- effects, consult the tests.
module Control.Eff.Internal where
import qualified Control.Arrow as A
import qualified Control.Category as C
import Control.Monad.Base (MonadBase(..))
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Trans.Control (MonadBaseControl(..))
import qualified Control.Exception as Exc
import safe Data.OpenUnion
import safe Data.FTCQueue
import GHC.Exts (inline)
import Data.Function (fix)
-- | Effectful arrow type: a function from a to b that also does effects
-- denoted by r
type Arr r a b = a -> Eff r b
-- | An effectful function from @a@ to @b@ that is a composition of one or more
-- effectful functions. The paremeter r describes the overall effect.
--
-- The composition members are accumulated in a type-aligned queue. Using a
-- newtype here enables us to define `C.Category' and `A.Arrow' instances.
newtype Arrs r a b = Arrs (FTCQueue (Eff r) a b)
-- | 'Arrs' can be composed and have a natural identity.
instance C.Category (Arrs r) where
id = ident
f . g = comp g f
-- | As the name suggests, 'Arrs' also has an 'A.Arrow' instance.
instance A.Arrow (Arrs r) where
arr = arr
first = singleK . first . (^$)
first :: Arr r a b -> Arr r (a, c) (b, c)
first x = \(a,c) -> (, c) `fmap` x a
-- | convert single effectful arrow into composable type. i.e., convert 'Arr' to
-- 'Arrs'
{-# INLINE [2] singleK #-}
singleK :: Arr r a b -> Arrs r a b
singleK k = Arrs (tsingleton k)
{-# RULES
"singleK/qApp" [~2] forall q. singleK (qApp q) = q
#-}
-- | Application to the `generalized effectful function' @Arrs r b w@, i.e.,
-- convert 'Arrs' to 'Arr'
{-# INLINABLE [2] qApp #-}
qApp :: forall r b w. Arrs r b w -> Arr r b w
qApp (Arrs q) x = viewlMap (inline tviewl q) ($ x) cons
where
cons :: forall x. Arr r b x -> FTCQueue (Eff r) x w -> Eff r w
cons = \k t -> case k x of
Val y -> qApp (Arrs t) y
E (Arrs q0) u -> E (Arrs (q0 >< t)) u
{-
-- A bit more understandable version
qApp :: Arrs r b w -> b -> Eff r w
qApp q x = case tviewl q of
TOne k -> k x
k :| t -> bind' (k x) t
where
bind' :: Eff r a -> Arrs r a b -> Eff r b
bind' (Pure y) k = qApp k y
bind' (Impure u q) k = Impure u (q >< k)
-}
-- | Syntactic sugar for 'qApp'
{-# INLINE [2] (^$) #-}
(^$) :: forall r b w. Arrs r b w -> b -> Eff r w
q ^$ x = q `qApp` x
-- | Lift a function to an arrow
arr :: (a -> b) -> Arrs r a b
arr f = singleK (Val . f)
-- | The identity arrow
ident :: Arrs r a a
ident = arr id
-- | Arrow composition
{-# INLINE comp #-}
comp :: Arrs r a b -> Arrs r b c -> Arrs r a c
comp (Arrs f) (Arrs g) = Arrs (f >< g)
-- | Common pattern: append 'Arr' to 'Arrs'
(^|>) :: Arrs r a b -> Arr r b c -> Arrs r a c
(Arrs f) ^|> g = Arrs (f |> g)
-- | The monad that all effects in this library are based on.
--
-- An effectful computation is a value of type `Eff r a`.
-- In this signature, @r@ is a type-level list of effects that are being
-- requested and need to be handled inside an effectful computation.
-- @a@ is the computation's result similar to other monads.
--
-- A computation's result can be retrieved via the 'run' function.
-- However, all effects used in the computation need to be handled by the use
-- of the effects' @run*@ functions before unwrapping the final result.
-- For additional details, see the documentation of the effects you are using.
data Eff r a = Val a
| forall b. E (Arrs r b a) (Union r b)
-- | Case analysis for 'Eff' datatype. If the value is @'Val' a@ apply
-- the first function to @a@; if it is @'E' u q@, apply the second
-- function.
{-# INLINE eff #-}
eff :: (a -> b)
-> (forall v. Arrs r v a -> Union r v -> b)
-> Eff r a -> b
eff f _ (Val a) = f a
eff _ g (E q u) = g q u
-- | The usual 'bind' fnuction with arguments flipped. This is a
-- common pattern for Eff.
{-# INLINE bind #-}
bind :: Arr r a b -> Eff r a -> Eff r b
bind k e = eff k (E . (^|> k)) e -- just accumulates continuations
-- | Compose effectful arrows (and possibly change the effect!)
{-# INLINE qComp #-}
qComp :: Arrs r a b -> (Eff r b -> k) -> (a -> k)
-- qComp g h = (h . (g `qApp`))
qComp g h = \a -> h (g ^$ a)
-- | Compose effectful arrows (and possibly change the effect!)
{-# INLINE qComps #-}
qComps :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arrs r' a c
qComps g h = singleK $ qComp g h
instance Functor (Eff r) where
{-# INLINE fmap #-}
fmap f x = bind (Val . f) x
instance Applicative (Eff r) where
{-# INLINE pure #-}
pure = Val
mf <*> e = bind (`fmap` e) mf
instance Monad (Eff r) where
{-# INLINE return #-}
{-# INLINE [2] (>>=) #-}
return = pure
m >>= f = bind f m
{-
Val _ >> m = m
E q u >> m = E (q ^|> const m) u
-}
-- | Send a request and wait for a reply (resulting in an effectful
-- computation).
{-# INLINE [2] send #-}
send :: Member t r => t v -> Eff r v
send t = E (singleK Val) (inj t)
-- This seems to be a very beneficial rule! On micro-benchmarks, cuts
-- the needed memory in half and speeds up almost twice.
{-# RULES
"send/bind" [~3] forall t k. send t >>= k = E (singleK k) (inj t)
#-}
-- ------------------------------------------------------------------------
-- | Get the result from a pure computation
--
-- A pure computation has type @Eff '[] a@. The empty effect-list indicates that
-- no further effects need to be handled.
run :: Eff '[] w -> w
run (Val x) = x
-- | @Union []@ has no nonbottom values.
-- Due to laziness it is possible to get into this branch but its union argument
-- cannot terminate.
-- To extract the true error, the evaluation of union is forced.
-- 'run' is a total function if its argument is different from bottom.
run (E _ union) =
union `seq` error "extensible-effects: the impossible happened!"
-- | Abstract the recursive 'relay' pattern, i.e., "somebody else's problem".
class Relay k r where
relay :: (v -> k) -> Union r v -> k
instance Relay (Eff r w) r where
{-# INLINABLE relay #-}
relay q u = E (singleK q) u
instance Relay k r => Relay (s -> k) r where
{-# INLINABLE relay #-}
relay q u s = relay (\x -> q x s) u
-- | Respond to requests of type @t@. The handlers themselves are expressed in
-- open-recursion style.
class Handle t r a k where
handle :: (Eff r a -> k) -- ^ untied recursive knot
-> Arrs r v a -- ^ coroutine awaiting response
-> t v -- ^ request
-> k
-- | A convenient pattern: given a request (in an open union), either handle
-- it (using default Handler) or relay it.
--
-- "Handle" implies that all requests of type @t@ are dealt with, i.e., @k@
-- (the response type) doesn't have @t@ as part of its effect list. The @Relay
-- k r@ constraint ensures that @k@ is an effectful computation (with
-- effectlist @r@).
--
-- Note that we can only handle the leftmost effect type (a consequence of the
-- 'Data.OpenUnion' implementation.
handle_relay :: r ~ (t ': r') => Relay k r'
=> (a -> k) -- ^ return
-> (Eff r a -> k) -- ^ untied recursive knot
-> Eff r a -> k
handle_relay ret step m = eff ret
(\q u -> case u of
U0 x -> handle step q x
U1 u' -> relay (qComp q step) u')
m
-- | Intercept the request and possibly respond to it, but leave it
-- unhandled. The @Relay k r@ constraint ensures that @k@ is an effectful
-- computation (with effectlist @r@). As such, the effect type @t@ will show
-- up in the response type @k@. There are two natural / commmon options for
-- @k@: the implicit effect domain (i.e., Eff r (f a)), or the explicit effect
-- domain (i.e., s1 -> s2 -> ... -> sn -> Eff r (f a s1 s2 ... sn)).
--
-- There are three different ways in which we may want to alter behaviour:
--
-- 1. __Before__: This work should be done before 'respond_relay' is called.
--
-- 2. __During__: This work should be done by altering the handler being
-- passed to 'respond_relay'. This allows us to modify the requests "in
-- flight".
--
-- 3. __After__: This work should be done be altering the @ret@ being passed
-- to 'respond_relay'. This allows us to overwrite changes or discard them
-- altogether. If this seems magical, note that we have the flexibility of
-- altering the target domain @k@. Specifically, the explicit domain
-- representation gives us access to the "effect" realm allowing us to
-- manipulate it directly.
respond_relay :: Member t r => Relay k r
=> (a -> k) -- ^ return
-> (Eff r a -> k) -- ^ untied recursive knot
-> Eff r a -> k
respond_relay ret step m = eff ret
(\q u -> case u of
U0' x -> handle @t step q x
_ -> relay (qComp q step) u)
m
-- | A less commonly needed variant with an explicit handler (instead
-- of @Handle t r a k@ constraint).
{-# INLINE handle_relay' #-}
handle_relay' :: r ~ (t ': r') => Relay k r'
=> (forall v. (Eff r a -> k) -> Arrs r v a -> t v -> k) -- ^ handler
-> (a -> k) -- ^ return
-> (Eff r a -> k) -- ^ untied recursive knot
-> Eff r a -> k
handle_relay' hdl ret step m = eff ret
(\q u -> case u of
U0 x -> hdl step q x
U1 u' -> relay (qComp q step) u')
m
-- | Variant with an explicit handler (instead of @Handle t r a k@
-- constraint).
{-# INLINE respond_relay' #-}
respond_relay' :: Member t r => Relay k r
=> (forall v. (Eff r a -> k) -> Arrs r v a -> t v -> k) -- ^ handler
-> (a -> k) -- ^ return
-> (Eff r a -> k) -- ^ recursive knot
-> Eff r a -> k
respond_relay' hdl ret step m = eff ret
(\q u -> case u of
U0' x -> hdl step q x
_ -> relay (qComp q step) u)
m
-- | Embeds a less-constrained 'Eff' into a more-constrained one. Analogous to
-- MTL's 'lift'.
raise :: Eff r a -> Eff (e ': r) a
raise (Val x) = pure x
raise (E q u) = E k (U1 u)
where k = qComps q raise
{-# INLINE raise #-}
-- ------------------------------------------------------------------------
-- | Lifting: emulating monad transformers
newtype Lift m a = Lift { unLift :: m a }
-- |A convenient alias to @SetMember Lift (Lift m) r@, which allows us
-- to assert that the lifted type occurs ony once in the effect list.
type Lifted m r = SetMember Lift (Lift m) r
-- |Same as 'Lifted' but with additional 'MonadBaseControl' constraint
type LiftedBase m r = ( SetMember Lift (Lift m) r
, MonadBaseControl m (Eff r)
)
-- | embed an operation of type `m a` into the `Eff` monad when @Lift m@ is in
-- a part of the effect-list.
lift :: Lifted m r => m a -> Eff r a
lift = send . Lift
-- | Handle lifted requests by running them sequentially
instance Monad m => Handle (Lift m) r a (m k) where
handle step q (Lift x) = x >>= (step . (q ^$))
-- | The handler of Lift requests. It is meant to be terminal: we only
-- allow a single Lifted Monad. Note, too, how this is different from
-- other handlers.
runLift :: Monad m => Eff '[Lift m] w -> m w
runLift m = fix step m
where
step :: Monad m => (Eff '[Lift m] w -> m w) -> Eff '[Lift m] w -> m w
step next m' = eff return
(\q u -> case u of
U0' x -> handle next q x
_ -> error "Impossible: Nothing to relay!")
m'
-- | Catching of dynamic exceptions
-- See the problem in
-- http://okmij.org/ftp/Haskell/misc.html#catch-MonadIO
catchDynE :: forall e a r.
(Lifted IO r, Exc.Exception e) =>
Eff r a -> (e -> Eff r a) -> Eff r a
catchDynE m eh = fix (respond_relay' h return) m
where
-- Polymorphic local binding: signature is needed
h :: (Eff r a -> Eff r a) -> Arrs r v a -> Lift IO v -> Eff r a
h step q (Lift em) = lift (Exc.try em) >>= either eh k
where k = step . (q ^$)
-- | You need this when using 'catchesDynE'.
data HandlerDynE r a =
forall e. (Exc.Exception e, Lifted IO r) => HandlerDynE (e -> Eff r a)
-- | Catch multiple dynamic exceptions. The implementation follows
-- that in Control.Exception almost exactly. Not yet tested.
-- Could this be useful for control with cut?
catchesDynE :: Lifted IO r => Eff r a -> [HandlerDynE r a] -> Eff r a
catchesDynE m hs = m `catchDynE` catchesHandler hs where
catchesHandler :: Lifted IO r => [HandlerDynE r a] -> Exc.SomeException -> Eff r a
catchesHandler handlers e = foldr tryHandler (lift . Exc.throw $ e) handlers
where
tryHandler (HandlerDynE h) res = maybe res h (Exc.fromException e)
instance (MonadBase b m, Lifted m r) => MonadBase b (Eff r) where
liftBase = lift . liftBase
{-# INLINE liftBase #-}
instance (MonadBase m m) => MonadBaseControl m (Eff '[Lift m]) where
type StM (Eff '[Lift m]) a = a
liftBaseWith f = lift (f runLift)
{-# INLINE liftBaseWith #-}
restoreM = return
{-# INLINE restoreM #-}
instance (MonadIO m, Lifted m r) => MonadIO (Eff r) where
liftIO = lift . liftIO
{-# INLINE liftIO #-}