{-# LANGUAGE  TypeOperators,            -- h :* e                     (looks nice but not required)
              ConstraintKinds,          -- type (h ?: e) = In h e     (looks nice but not required)
              FlexibleInstances,        -- instance Sub () e          (non type variable in head)
              FlexibleContexts,         -- (State Int ?: e) => ...    (non type variable argument)
              DataKinds, TypeFamilies,  -- type family HEqual h h' :: Bool
              UndecidableInstances,     -- InEq (HEqual h h') h h' e => ... (duplicate instance variable)
              ScopedTypeVariables,
              GADTs,
              MultiParamTypeClasses,
              Rank2Types
#-}
{-|
Description : Efficient effect handlers based on Evidence Passing Semantics
Copyright   : (c) 2021, Ningning Xie, Daan Leijen
License     : MIT
Maintainer  : xnning@hku.hk; daan@microsoft.com
Stability   : Experimental

Efficient effect handlers based on Evidence passing semantics. The implementation
is based on /"Generalized Evidence Passing for Effect Handlers"/, Ningning Xie and Daan Leijen, 2021 [(pdf)](https://www.microsoft.com/en-us/research/publication/generalized-evidence-passing-for-effect-handlers/),
The implementation is closely based on the [Ev.Eff](https://hackage.haskell.org/package/eveff) 
library described in detail in /"Effect Handlers in Haskell, Evidently"/, Ningning Xie and Daan Leijen, Haskell 2020 [(pdf)](https://www.microsoft.com/en-us/research/publication/effect-handlers-in-haskell-evidently).
The _Mp.Eff_ and _Ev.Eff_ libraries expose the exact same interface, but
the _Mp.Eff_ library can express full effect handler semantics, including non-scoped resumptions --
it is slightly slower though (see the 2021 paper for benchmarks and a detailed comparison).

An example of defining and using a @Reader@ effect:

@
\{\-\# LANGUAGE  TypeOperators, FlexibleContexts, Rank2Types  \#\-\}
import Control.Mp.Eff

-- A @Reader@ effect definition with one operation @ask@ of type @()@ to @a@.
data Reader a e ans = Reader{ ask :: `Op` () a e ans }

greet :: (Reader String `:?` e) => `Eff` e String
greet = do s <- `perform` ask ()
           return ("hello " ++ s)

test :: String
test = `runEff` $
       `handler` (Reader{ ask = `value` "world" }) $  -- @:: Reader String () Int@
       do s <- greet                              -- executes in context @:: `Eff` (Reader String `:*` ()) Int@
          return (length s)
@

Enjoy,

Ningning Xie and Daan Leijen,  Mar 2021.

-}
module Control.Mp.Eff(
            -- * Effect monad
              Eff
            , runEff          -- :: Eff () a -> a

            -- * Effect context
            , (:?)            -- h :? e,  is h in e?
            , (:*)            -- h :* e,  cons h in front of e
            -- , In           -- alias for :?

            -- * Perform and Handlers
            , perform         -- :: (h :? e) => (forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
            , handler         -- :: h e ans -> Eff (h :* e) ans -> Eff e ans
            , handlerRet      -- :: (ans -> b) -> h e b -> Eff (h :* e) ans -> Eff e b
            , handlerHide     -- :: h (h' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* e) ans
            , mask            -- :: Eff e ans -> Eff (h :* e) ans

            -- * Defining operations
            , Op
            , value           -- :: a -> Op () a e ans
            , function        -- :: (a -> Eff e b) -> Op a b e ans
            , except          -- :: (a -> Eff e ans) -> Op a b e ans
            , operation       -- :: (a -> (b -> Eff e ans)) -> Op a b e ans

            -- * Local state
            , Local           -- Local a e ans

            , local           -- :: a -> Eff (Local a :* e) ans -> Eff e ans
            , localRet        -- :: a -> (ans -> a -> b) -> Eff (Local a :* e) ans -> Eff e b
            , handlerLocal    -- :: a -> h (Local a :* e) ans -> Eff (h :* e) ans -> Eff e ans
            , handlerLocalRet -- :: a -> (ans -> a -> b) -> h (Local a :* e) b -> Eff (h :* e) ans -> Eff e b

            , lget            -- :: (Local a :? e) => Eff e a
            , lput            -- :: (Local a :? e) => a -> Eff e ()
            , lmodify         -- :: (Local a :? e) => (a -> a) -> Eff e ()

            , localGet        -- :: Eff (Local a :* e) a
            , localPut        -- :: a -> Eff (Local a :* e) ()
            , localModify     -- :: (a -> a) -> Eff (Local a :* e) a

            ) where

import Prelude hiding (read,flip)
import Control.Monad( ap, liftM )
import Data.Type.Equality( (:~:)( Refl ) )
import Control.Monad.Primitive

-------------------------------------------------------
-- Assume some way to generate a fresh prompt marker
-- associated with specific effect and answer type.
-------------------------------------------------------
import Unsafe.Coerce     (unsafeCoerce)
import System.IO.Unsafe ( unsafePerformIO )
import Data.IORef

-- an abstract marker
data Marker (h:: * -> * -> *) e a = Marker !Integer

instance Show (Marker h e a) where
  show :: Marker h e a -> String
show (Marker Integer
i) = Integer -> String
forall a. Show a => a -> String
show Integer
i

-- if markers match, their types are the same
mmatch :: Marker h e a -> Marker h' e' b -> Maybe ((h e a, a, e) :~: (h' e' b, b, e'))
mmatch :: Marker h e a
-> Marker h' e' b -> Maybe ((h e a, a, e) :~: (h' e' b, b, e'))
mmatch (Marker Integer
i) (Marker Integer
j) | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j  = ((h e a, a, e) :~: (h' e' b, b, e'))
-> Maybe ((h e a, a, e) :~: (h' e' b, b, e'))
forall a. a -> Maybe a
Just ((Any :~: Any) -> (h e a, a, e) :~: (h' e' b, b, e')
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
mmatch Marker h e a
_ Marker h' e' b
_ = Maybe ((h e a, a, e) :~: (h' e' b, b, e'))
forall a. Maybe a
Nothing

{-# NOINLINE unique #-}
unique :: IORef Integer
unique :: IORef Integer
unique = IO (IORef Integer) -> IORef Integer
forall a. IO a -> a
unsafePerformIO (Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0)

-- evaluate a action with a fresh marker
{-# NOINLINE freshMarker #-}
freshMarker :: (Marker h e a -> Eff e a) -> Eff e a
freshMarker :: (Marker h e a -> Eff e a) -> Eff e a
freshMarker Marker h e a -> Eff e a
f
  = let m :: Integer
m = IO Integer -> Integer
forall a. IO a -> a
unsafePerformIO (IO Integer -> Integer) -> IO Integer -> Integer
forall a b. (a -> b) -> a -> b
$
            do Integer
i <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
unique;
               IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
unique (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1);
               Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
i
    in Integer -> Eff e a -> Eff e a
seq Integer
m (Marker h e a -> Eff e a
f (Integer -> Marker h e a
forall (h :: * -> * -> *) e a. Integer -> Marker h e a
Marker Integer
m))

-------------------------------------------------------
-- The handler context
-------------------------------------------------------
infixr 5 :*

data (h :: * -> * -> *) :* e

data Context e where
  CCons :: !(Marker h e' ans) -> !(h e' ans) -> !(ContextT e e') -> !(Context e) -> Context (h :* e)
  CNil  :: Context ()

data ContextT e e' where
  CTCons :: !(Marker h e' ans) -> !(h e' ans) -> !(ContextT e e') -> ContextT e (h :* e)
  CTId   :: ContextT e e
  -- CTComp :: ContextT e'' e' -> ContextT e e'' -> ContextT e e'
  -- CTFun :: !(Context e -> Context e') -> ContextT e e'

-- apply a context transformer
applyT :: ContextT e e' -> Context e -> Context e'
applyT :: ContextT e e' -> Context e -> Context e'
applyT (CTCons Marker h e' ans
m h e' ans
h ContextT e e'
g) Context e
ctx = Marker h e' ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
forall (h :: * -> * -> *) e' ans e.
Marker h e' ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker h e' ans
m h e' ans
h ContextT e e'
g Context e
ctx
applyT (ContextT e e'
CTId) Context e
ctx         = Context e
Context e'
ctx
--applyT (CTComp c1 c2) ctx = applyT c1 (applyT c2 ctx)
--applyT (CTFun f) ctx = f ctx

-- the tail of a context
ctail :: Context (h :* e) -> Context e
ctail :: Context (h :* e) -> Context e
ctail (CCons Marker h e' ans
_ h e' ans
_ ContextT e e'
_ Context e
ctx)   = Context e
Context e
ctx

-------------------------------------------------------
-- The Multi Prompt control monad
-- ans: the answer type, i.e. the type of the handler/prompt context.
-- e' : the answer effect, i.e. the effect in the handler/prompt context.
-- b  : the result type of the operation
-------------------------------------------------------
data Ctl e a = Pure { Ctl e a -> a
result :: !a }
             | forall h b e' ans.
               Control{ ()
marker :: Marker h e' ans,                    -- prompt marker to yield to (in type context `::ans`)
                        ()
op     :: !((b -> Eff e' ans) -> Eff e' ans),  -- the final action, just needs the resumption (:: b -> Eff e' ans) to be evaluated.
                        ()
cont   :: !(b -> Eff e a) }                    -- the (partially) build up resumption; (b -> Eff e a) :~: (b -> Eff e' ans)` by the time we reach the prompt


newtype Eff e a = Eff { Eff e a -> Context e -> Ctl e a
unEff :: Context e -> Ctl e a }

{-# INLINE lift #-}
lift :: Ctl e a -> Eff e a
lift :: Ctl e a -> Eff e a
lift Ctl e a
ctl = (Context e -> Ctl e a) -> Eff e a
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e
ctx -> Ctl e a
ctl)

{-# INLINE ctxMap #-}
ctxMap :: (Context e' -> Context e) -> Eff e a -> Eff e' a
ctxMap :: (Context e' -> Context e) -> Eff e a -> Eff e' a
ctxMap Context e' -> Context e
f Eff e a
eff = (Context e' -> Ctl e' a) -> Eff e' a
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e'
ctx -> (Context e' -> Context e) -> Ctl e a -> Ctl e' a
forall e' e a. (Context e' -> Context e) -> Ctl e a -> Ctl e' a
ctxMapCtl Context e' -> Context e
f (Ctl e a -> Ctl e' a) -> Ctl e a -> Ctl e' a
forall a b. (a -> b) -> a -> b
$ Eff e a -> Context e -> Ctl e a
forall e a. Eff e a -> Context e -> Ctl e a
unEff Eff e a
eff (Context e' -> Context e
f Context e'
ctx))

{-# INLINE ctxMapCtl #-}
ctxMapCtl :: (Context e' -> Context e) -> Ctl e a -> Ctl e' a
ctxMapCtl :: (Context e' -> Context e) -> Ctl e a -> Ctl e' a
ctxMapCtl Context e' -> Context e
f (Pure a
x) = a -> Ctl e' a
forall e a. a -> Ctl e a
Pure a
x
ctxMapCtl Context e' -> Context e
f (Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e a
cont) = Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e' a) -> Ctl e' a
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op (\b
b -> (Context e' -> Context e) -> Eff e a -> Eff e' a
forall e' e a. (Context e' -> Context e) -> Eff e a -> Eff e' a
ctxMap Context e' -> Context e
f (b -> Eff e a
cont b
b))

{-# INLINE hideSecond #-}
hideSecond :: Eff (h :* e) a -> Eff (h :* h' :* e) a
hideSecond :: Eff (h :* e) a -> Eff (h :* (h' :* e)) a
hideSecond Eff (h :* e) a
eff = (Context (h :* (h' :* e)) -> Context (h :* e))
-> Eff (h :* e) a -> Eff (h :* (h' :* e)) a
forall e' e a. (Context e' -> Context e) -> Eff e a -> Eff e' a
ctxMap (\(CCons Marker h e' ans
m h e' ans
h ContextT e e'
CTId (CCons Marker h e' ans
m' h e' ans
h' ContextT e e'
g' Context e
ctx)) ->
                             Marker h e' ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
forall (h :: * -> * -> *) e' ans e.
Marker h e' ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker h e' ans
m h e' ans
h (Marker h e' ans -> h e' ans -> ContextT e e' -> ContextT e (h :* e)
forall (h :: * -> * -> *) e' ans e.
Marker h e' ans -> h e' ans -> ContextT e e' -> ContextT e (h :* e)
CTCons Marker h e' ans
m' h e' ans
h' ContextT e e'
g') Context e
ctx) Eff (h :* e) a
eff

under :: In h e => Marker h e' ans -> Context e' -> Eff e' b -> Eff e b
under :: Marker h e' ans -> Context e' -> Eff e' b -> Eff e b
under Marker h e' ans
m Context e'
ctx (Eff Context e' -> Ctl e' b
eff) = (Context e -> Ctl e b) -> Eff e b
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e
_ -> case Context e' -> Ctl e' b
eff Context e'
ctx of
                                       Pure b
x -> b -> Ctl e b
forall e a. a -> Ctl e a
Pure b
x
                                       Control Marker h e' ans
n (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e' b
cont -> Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e b) -> Ctl e b
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
n (b -> Eff e' ans) -> Eff e' ans
op (Marker h e' ans -> Context e' -> (b -> Eff e' b) -> b -> Eff e b
forall (h :: * -> * -> *) a b e e' ans.
In h e =>
Marker h e' ans -> Context e' -> (b -> Eff e' a) -> b -> Eff e a
resumeUnder Marker h e' ans
m Context e'
ctx b -> Eff e' b
cont))
                                       -- Control n op cont -> Control n op (under m ctx . cont)) -- wrong

resumeUnder :: forall h a b e e' ans. In h e => Marker h e' ans -> Context e' -> (b -> Eff e' a) -> (b -> Eff e a)
resumeUnder :: Marker h e' ans -> Context e' -> (b -> Eff e' a) -> b -> Eff e a
resumeUnder Marker h e' ans
m Context e'
ctx b -> Eff e' a
cont b
x
  = (SubContext h -> Eff e a) -> Eff e a
forall (h :: * -> * -> *) e a.
(h :? e) =>
(SubContext h -> Eff e a) -> Eff e a
withSubContext ((SubContext h -> Eff e a) -> Eff e a)
-> (SubContext h -> Eff e a) -> Eff e a
forall a b. (a -> b) -> a -> b
$ \(SubContext (CCons Marker h e' ans
m' h e' ans
h' ContextT e e'
g' Context e
ctx') :: SubContext h) ->
    case Marker h e' ans
-> Marker h e' ans
-> Maybe ((h e' ans, ans, e') :~: (h e' ans, ans, e'))
forall (h :: * -> * -> *) e a (h' :: * -> * -> *) e' b.
Marker h e a
-> Marker h' e' b -> Maybe ((h e a, a, e) :~: (h' e' b, b, e'))
mmatch Marker h e' ans
m Marker h e' ans
m' of
      Just (h e' ans, ans, e') :~: (h e' ans, ans, e')
Refl -> Marker h e' ans -> Context e' -> Eff e' a -> Eff e a
forall (h :: * -> * -> *) e e' ans b.
In h e =>
Marker h e' ans -> Context e' -> Eff e' b -> Eff e b
under Marker h e' ans
m (ContextT e e' -> Context e -> Context e'
forall e e'. ContextT e e' -> Context e -> Context e'
applyT ContextT e e'
g' Context e
ctx') (b -> Eff e' a
cont b
x)
      Maybe ((h e' ans, ans, e') :~: (h e' ans, ans, e'))
Nothing   -> String -> Eff e a
forall a. HasCallStack => String -> a
error String
"EffEv.resumeUnder: marker does not match anymore (this should never happen?)"


instance Functor (Eff e) where
  fmap :: (a -> b) -> Eff e a -> Eff e b
fmap  = (a -> b) -> Eff e a -> Eff e b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Applicative (Eff e) where
  pure :: a -> Eff e a
pure  = a -> Eff e a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Eff e (a -> b) -> Eff e a -> Eff e b
(<*>) = Eff e (a -> b) -> Eff e a -> Eff e b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad (Eff e) where
  return :: a -> Eff e a
return a
x   = (Context e -> Ctl e a) -> Eff e a
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e
evv -> a -> Ctl e a
forall e a. a -> Ctl e a
Pure a
x)
  >>= :: Eff e a -> (a -> Eff e b) -> Eff e b
(>>=)      = Eff e a -> (a -> Eff e b) -> Eff e b
forall e a b. Eff e a -> (a -> Eff e b) -> Eff e b
bind

-- start yielding (with an initially empty continuation)
{-# INLINE yield #-}
yield :: Marker h e ans -> ((b -> Eff e ans) -> Eff e ans) -> Eff e' b
yield :: Marker h e ans -> ((b -> Eff e ans) -> Eff e ans) -> Eff e' b
yield Marker h e ans
m (b -> Eff e ans) -> Eff e ans
op  = (Context e' -> Ctl e' b) -> Eff e' b
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e'
ctx -> Marker h e ans
-> ((b -> Eff e ans) -> Eff e ans) -> (b -> Eff e' b) -> Ctl e' b
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e ans
m (b -> Eff e ans) -> Eff e ans
op b -> Eff e' b
forall (f :: * -> *) a. Applicative f => a -> f a
pure)

{-# INLINE kcompose #-}
kcompose :: (b -> Eff e c) -> (a -> Eff e b) -> a -> Eff e c      -- Kleisli composition
kcompose :: (b -> Eff e c) -> (a -> Eff e b) -> a -> Eff e c
kcompose b -> Eff e c
g a -> Eff e b
f a
x =
  case a -> Eff e b
f a
x of
    -- bind (f x) g
    Eff Context e -> Ctl e b
eff -> (Context e -> Ctl e c) -> Eff e c
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e
ctx -> case Context e -> Ctl e b
eff Context e
ctx of
                              Pure b
x -> Eff e c -> Context e -> Ctl e c
forall e a. Eff e a -> Context e -> Ctl e a
unEff (b -> Eff e c
g b
x) Context e
ctx
                              Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e b
cont -> Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e c) -> Ctl e c
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op (b -> Eff e c
g (b -> Eff e c) -> (b -> Eff e b) -> b -> Eff e c
forall b e c a. (b -> Eff e c) -> (a -> Eff e b) -> a -> Eff e c
`kcompose` b -> Eff e b
cont))

{-# INLINE bind #-}
bind :: Eff e a -> (a -> Eff e b) -> Eff e b
bind :: Eff e a -> (a -> Eff e b) -> Eff e b
bind (Eff Context e -> Ctl e a
eff) a -> Eff e b
f
  = (Context e -> Ctl e b) -> Eff e b
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff (\Context e
ctx -> case Context e -> Ctl e a
eff Context e
ctx of
                   Pure a
x            -> Eff e b -> Context e -> Ctl e b
forall e a. Eff e a -> Context e -> Ctl e a
unEff (a -> Eff e b
f a
x) Context e
ctx
                   Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e a
cont -> Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e b) -> Ctl e b
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op (a -> Eff e b
f (a -> Eff e b) -> (b -> Eff e a) -> b -> Eff e b
forall b e c a. (b -> Eff e c) -> (a -> Eff e b) -> a -> Eff e c
`kcompose` b -> Eff e a
cont))  -- keep yielding with an extended continuation

instance Functor (Ctl e) where
  fmap :: (a -> b) -> Ctl e a -> Ctl e b
fmap  = (a -> b) -> Ctl e a -> Ctl e b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Applicative (Ctl e) where
  pure :: a -> Ctl e a
pure  = a -> Ctl e a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Ctl e (a -> b) -> Ctl e a -> Ctl e b
(<*>) = Ctl e (a -> b) -> Ctl e a -> Ctl e b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad (Ctl e) where
  return :: a -> Ctl e a
return a
x      = a -> Ctl e a
forall e a. a -> Ctl e a
Pure a
x
  Pure a
x >>= :: Ctl e a -> (a -> Ctl e b) -> Ctl e b
>>= a -> Ctl e b
f  = a -> Ctl e b
f a
x
  (Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e a
cont) >>= a -> Ctl e b
f
    = Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e b) -> Ctl e b
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op (a -> Ctl e b
f (a -> Ctl e b) -> (b -> Eff e a) -> b -> Eff e b
forall b e c a. (b -> Ctl e c) -> (a -> Eff e b) -> a -> Eff e c
`kcompose2` b -> Eff e a
cont)

kcompose2 :: (b -> Ctl e c) -> (a -> Eff e b) -> a -> Eff e c
kcompose2 :: (b -> Ctl e c) -> (a -> Eff e b) -> a -> Eff e c
kcompose2 b -> Ctl e c
g a -> Eff e b
f a
x
  = (Context e -> Ctl e c) -> Eff e c
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff ((Context e -> Ctl e c) -> Eff e c)
-> (Context e -> Ctl e c) -> Eff e c
forall a b. (a -> b) -> a -> b
$ \Context e
ctx -> case Eff e b -> Context e -> Ctl e b
forall e a. Eff e a -> Context e -> Ctl e a
unEff (a -> Eff e b
f a
x) Context e
ctx of
        Pure b
x -> b -> Ctl e c
g b
x
        Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e b
cont -> Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e c) -> Ctl e c
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op (b -> Ctl e c
g (b -> Ctl e c) -> (b -> Eff e b) -> b -> Eff e c
forall b e c a. (b -> Ctl e c) -> (a -> Eff e b) -> a -> Eff e c
`kcompose2` b -> Eff e b
cont)


-- use a prompt with a unique marker (and handle yields to it)
{-# INLINE prompt #-}
prompt :: Marker h e ans -> h e ans -> Eff (h :* e) ans -> Eff e ans
prompt :: Marker h e ans -> h e ans -> Eff (h :* e) ans -> Eff e ans
prompt Marker h e ans
m h e ans
h (Eff Context (h :* e) -> Ctl (h :* e) ans
eff) = (Context e -> Ctl e ans) -> Eff e ans
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff ((Context e -> Ctl e ans) -> Eff e ans)
-> (Context e -> Ctl e ans) -> Eff e ans
forall a b. (a -> b) -> a -> b
$ \Context e
ctx ->
  case (Context (h :* e) -> Ctl (h :* e) ans
eff (Marker h e ans
-> h e ans -> ContextT e e -> Context e -> Context (h :* e)
forall (h :: * -> * -> *) e' ans e.
Marker h e' ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker h e ans
m h e ans
h ContextT e e
forall e. ContextT e e
CTId Context e
ctx)) of                    -- add handler to the context
    Pure ans
x -> ans -> Ctl e ans
forall e a. a -> Ctl e a
Pure ans
x
    Control Marker h e' ans
n (b -> Eff e' ans) -> Eff e' ans
op b -> Eff (h :* e) ans
cont ->
        let cont' :: b -> Eff e ans
cont' b
x = Marker h e ans -> h e ans -> Eff (h :* e) ans -> Eff e ans
forall (h :: * -> * -> *) e ans.
Marker h e ans -> h e ans -> Eff (h :* e) ans -> Eff e ans
prompt Marker h e ans
m h e ans
h (b -> Eff (h :* e) ans
cont b
x) in      -- extend the continuation with our own prompt
        case Marker h e ans
-> Marker h e' ans
-> Maybe ((h e ans, ans, e) :~: (h e' ans, ans, e'))
forall (h :: * -> * -> *) e a (h' :: * -> * -> *) e' b.
Marker h e a
-> Marker h' e' b -> Maybe ((h e a, a, e) :~: (h' e' b, b, e'))
mmatch Marker h e ans
m Marker h e' ans
n of
          Maybe ((h e ans, ans, e) :~: (h e' ans, ans, e'))
Nothing   -> Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans)
-> (b -> Eff e ans)
-> Ctl e ans
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
n (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e ans
cont'          -- keep yielding (but with the extended continuation)
          Just (h e ans, ans, e) :~: (h e' ans, ans, e')
Refl -> Eff e' ans -> Context e' -> Ctl e' ans
forall e a. Eff e a -> Context e -> Ctl e a
unEff ((b -> Eff e' ans) -> Eff e' ans
op b -> Eff e ans
b -> Eff e' ans
cont') Context e
Context e'
ctx   -- found our prompt, invoke `op` (under the context `ctx`).
                              -- Note: `Refl` proves `a ~ ans` and `e ~ e'` (the existential `ans,e'` in Control)

{-# INLINE handler #-}
handler :: h e ans -> Eff (h :* e) ans -> Eff e ans
handler :: h e ans -> Eff (h :* e) ans -> Eff e ans
handler h e ans
h Eff (h :* e) ans
action
  = (Marker h e ans -> Eff e ans) -> Eff e ans
forall (h :: * -> * -> *) e a. (Marker h e a -> Eff e a) -> Eff e a
freshMarker ((Marker h e ans -> Eff e ans) -> Eff e ans)
-> (Marker h e ans -> Eff e ans) -> Eff e ans
forall a b. (a -> b) -> a -> b
$ \Marker h e ans
m -> Marker h e ans -> h e ans -> Eff (h :* e) ans -> Eff e ans
forall (h :: * -> * -> *) e ans.
Marker h e ans -> h e ans -> Eff (h :* e) ans -> Eff e ans
prompt Marker h e ans
m h e ans
h Eff (h :* e) ans
action

-- Run a control monad
runEff :: Eff () a -> a
runEff :: Eff () a -> a
runEff (Eff Context () -> Ctl () a
eff) = case Context () -> Ctl () a
eff Context ()
CNil of
                   Pure a
x -> a
x
                   Control Marker h e' ans
_ (b -> Eff e' ans) -> Eff e' ans
_ b -> Eff () a
_ -> String -> a
forall a. HasCallStack => String -> a
error String
"Unhandled operation"  -- can never happen

{-# INLINE handlerRet #-}
handlerRet :: (ans -> a) -> h e a -> Eff (h :* e) ans -> Eff e a
handlerRet :: (ans -> a) -> h e a -> Eff (h :* e) ans -> Eff e a
handlerRet ans -> a
ret h e a
h Eff (h :* e) ans
action
  = h e a -> Eff (h :* e) a -> Eff e a
forall (h :: * -> * -> *) e ans.
h e ans -> Eff (h :* e) ans -> Eff e ans
handler h e a
h (do ans
x <- Eff (h :* e) ans
action; a -> Eff (h :* e) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ans -> a
ret ans
x))

{-# INLINE handlerHide #-}
handlerHide :: h (h' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* e) ans
handlerHide :: h (h' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* e) ans
handlerHide h (h' :* e) ans
h Eff (h :* e) ans
action
  = h (h' :* e) ans -> Eff (h :* (h' :* e)) ans -> Eff (h' :* e) ans
forall (h :: * -> * -> *) e ans.
h e ans -> Eff (h :* e) ans -> Eff e ans
handler h (h' :* e) ans
h (Eff (h :* e) ans -> Eff (h :* (h' :* e)) ans
forall (h :: * -> * -> *) e a (h' :: * -> * -> *).
Eff (h :* e) a -> Eff (h :* (h' :* e)) a
hideSecond Eff (h :* e) ans
action)

{-# INLINE handlerHideRetEff #-}
handlerHideRetEff :: (ans -> Eff (h' :* e) b) -> h (h' :* e) b -> Eff (h :* e) ans -> Eff (h' :* e) b
handlerHideRetEff :: (ans -> Eff (h' :* e) b)
-> h (h' :* e) b -> Eff (h :* e) ans -> Eff (h' :* e) b
handlerHideRetEff ans -> Eff (h' :* e) b
ret h (h' :* e) b
h Eff (h :* e) ans
action
  = h (h' :* e) b -> Eff (h :* (h' :* e)) b -> Eff (h' :* e) b
forall (h :: * -> * -> *) e ans.
h e ans -> Eff (h :* e) ans -> Eff e ans
handler h (h' :* e) b
h (do ans
x <- Eff (h :* e) ans -> Eff (h :* (h' :* e)) ans
forall (h :: * -> * -> *) e a (h' :: * -> * -> *).
Eff (h :* e) a -> Eff (h :* (h' :* e)) a
hideSecond Eff (h :* e) ans
action; Eff (h' :* e) b -> Eff (h :* (h' :* e)) b
forall e ans (h :: * -> * -> *). Eff e ans -> Eff (h :* e) ans
mask (ans -> Eff (h' :* e) b
ret ans
x))

-- | Mask the top effect handler in the give action (i.e. if a operation is performed
-- on an @h@ effect inside @e@ the top handler is ignored).
mask :: Eff e ans -> Eff (h :* e) ans
mask :: Eff e ans -> Eff (h :* e) ans
mask Eff e ans
eff = (Context (h :* e) -> Context e) -> Eff e ans -> Eff (h :* e) ans
forall e' e a. (Context e' -> Context e) -> Eff e a -> Eff e' a
ctxMap Context (h :* e) -> Context e
forall (h :: * -> * -> *) e. Context (h :* e) -> Context e
ctail Eff e ans
eff


---------------------------------------------------------
--
---------------------------------------------------------

type h :? e = In h e

data SubContext h = forall e. SubContext !(Context (h:* e))

class In h e where
  subContext :: Context e -> SubContext h

instance (InEq (HEqual h h') h h' ctx) => In h (h' :* ctx)  where
  subContext :: Context (h' :* ctx) -> SubContext h
subContext = Context (h' :* ctx) -> SubContext h
forall (iseq :: Bool) (h :: * -> * -> *) (h' :: * -> * -> *) e.
InEq iseq h h' e =>
Context (h' :* e) -> SubContext h
subContextEq

type family HEqual (h :: * -> * -> *) (h' :: * -> * -> *) :: Bool where
  HEqual h h  = 'True
  HEqual h h' = 'False

class (iseq ~ HEqual h h') => InEq iseq h h' e  where
  subContextEq :: Context (h' :* e) -> SubContext h

instance (h ~ h') => InEq 'True h h' e where
  subContextEq :: Context (h' :* e) -> SubContext h
subContextEq Context (h' :* e)
ctx = Context (h' :* e) -> SubContext h'
forall (h :: * -> * -> *) e. Context (h :* e) -> SubContext h
SubContext Context (h' :* e)
ctx

instance ('False ~ HEqual h h', In h e) => InEq 'False h h' e where
  subContextEq :: Context (h' :* e) -> SubContext h
subContextEq Context (h' :* e)
ctx = Context e -> SubContext h
forall (h :: * -> * -> *) e. In h e => Context e -> SubContext h
subContext (Context (h' :* e) -> Context e
forall (h :: * -> * -> *) e. Context (h :* e) -> Context e
ctail Context (h' :* e)
ctx)


{-# INLINE withSubContext #-}
withSubContext :: (h :? e) => (SubContext h -> Eff e a) -> Eff e a
withSubContext :: (SubContext h -> Eff e a) -> Eff e a
withSubContext SubContext h -> Eff e a
action
  = do Context e
ctx <- (Context e -> Ctl e (Context e)) -> Eff e (Context e)
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff Context e -> Ctl e (Context e)
forall e a. a -> Ctl e a
Pure
       SubContext h -> Eff e a
action (Context e -> SubContext h
forall (h :: * -> * -> *) e. In h e => Context e -> SubContext h
subContext Context e
ctx)


------------------------------------
-- Operations
-------------------------------------

-- | The abstract type of operations of type @a@ to @b@, for a handler
-- defined in an effect context @e@ and answer type @ans@.
data Op a b e ans = Op { Op a b e ans
-> forall (h :: * -> * -> *) e'.
   In h e' =>
   Marker h e ans -> Context e -> a -> Eff e' b
applyOp:: !(forall h e'. In h e' => Marker h e ans -> Context e -> a -> Eff e' b) }


-- Given evidence and an operation selector, perform the operation
{-# INLINE perform #-}
perform :: In h e => (forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
perform :: (forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
perform forall e' ans. h e' ans -> Op a b e' ans
selectOp a
x
  = (SubContext h -> Eff e b) -> Eff e b
forall (h :: * -> * -> *) e a.
(h :? e) =>
(SubContext h -> Eff e a) -> Eff e a
withSubContext ((SubContext h -> Eff e b) -> Eff e b)
-> (SubContext h -> Eff e b) -> Eff e b
forall a b. (a -> b) -> a -> b
$ \(SubContext (CCons Marker h e' ans
m h e' ans
h ContextT e e'
g Context e
ctx)) ->
      Op a b e' ans -> Marker h e' ans -> Context e' -> a -> Eff e b
forall a b e ans.
Op a b e ans
-> forall (h :: * -> * -> *) e'.
   In h e' =>
   Marker h e ans -> Context e -> a -> Eff e' b
applyOp (h e' ans -> Op a b e' ans
forall e' ans. h e' ans -> Op a b e' ans
selectOp h e' ans
h e' ans
h) Marker h e' ans
m (ContextT e e' -> Context e -> Context e'
forall e e'. ContextT e e' -> Context e -> Context e'
applyT ContextT e e'
g Context e
ctx) a
x

-- | Create an operation that always resumes with a constant value (of type @a@).
-- (see also the `perform` example).
value :: a -> Op () a e ans
value :: a -> Op () a e ans
value a
x = (() -> Eff e a) -> Op () a e ans
forall a e b ans. (a -> Eff e b) -> Op a b e ans
function (\() -> a -> Eff e a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x)

-- | Create an operation that takes an argument of type @a@ and always resumes with a result of type @b@.
-- These are called /tail-resumptive/ operations and are implemented more efficient than
-- general operations as they can execute /in-place/ (instead of yielding to the handler).
-- Most operations are tail-resumptive. (See also the `handlerLocal` example).
function :: (a -> Eff e b) -> Op a b e ans
function :: (a -> Eff e b) -> Op a b e ans
function a -> Eff e b
f = (forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
forall a b e ans.
(forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
Op (\Marker h e ans
m Context e
ctx a
x -> Marker h e ans -> Context e -> Eff e b -> Eff e' b
forall (h :: * -> * -> *) e e' ans b.
In h e =>
Marker h e' ans -> Context e' -> Eff e' b -> Eff e b
under Marker h e ans
m Context e
ctx (a -> Eff e b
f a
x))

-- | Create an fully general operation from type @a@ to @b@.
-- the function @f@ takes the argument, and a /resumption/ function of type @b -> `Eff` e ans@
-- that can be called to resume from the original call site. For example:
--
-- @
-- data Amb e ans = Amb { flip :: forall b. `Op` () Bool e ans }
--
-- xor :: (Amb `:?` e) => `Eff` e Bool
-- xor = do x <- `perform` flip ()
--          y <- `perform` flip ()
--          return ((x && not y) || (not x && y))
--
-- solutions :: `Eff` (Amb `:*` e) a -> `Eff` e [a]
-- solutions = `handlerRet` (\\x -> [x]) $
--             Amb{ flip = `operation` (\\() k -> do{ xs <- k True; ys <- k False; return (xs ++ ys)) }) }
-- @
operation :: (a -> (b -> Eff e ans) -> Eff e ans) -> Op a b e ans
operation :: (a -> (b -> Eff e ans) -> Eff e ans) -> Op a b e ans
operation a -> (b -> Eff e ans) -> Eff e ans
f = (forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
forall a b e ans.
(forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
Op (\Marker h e ans
m Context e
ctx a
x -> Marker h e ans -> ((b -> Eff e ans) -> Eff e ans) -> Eff e' b
forall (h :: * -> * -> *) e ans b e'.
Marker h e ans -> ((b -> Eff e ans) -> Eff e ans) -> Eff e' b
yield Marker h e ans
m (\b -> Eff e ans
ctlk -> a -> (b -> Eff e ans) -> Eff e ans
f a
x b -> Eff e ans
ctlk))


-- | Create an operation that never resumes (an exception).
-- (See `handlerRet` for an example).
except :: (a -> Eff e ans) -> Op a b e ans
except :: (a -> Eff e ans) -> Op a b e ans
except a -> Eff e ans
f = (forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
forall a b e ans.
(forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
Op (\Marker h e ans
m Context e
ctx a
x -> Marker h e ans -> ((b -> Eff e ans) -> Eff e ans) -> Eff e' b
forall (h :: * -> * -> *) e ans b e'.
Marker h e ans -> ((b -> Eff e ans) -> Eff e ans) -> Eff e' b
yield Marker h e ans
m (\b -> Eff e ans
ctlk -> a -> Eff e ans
f a
x))

--------------------------------------------------------------------------------
-- Efficient (and safe) Local state handler
--------------------------------------------------------------------------------
-- | The type of the built-in state effect.
-- (This state is generally more efficient than rolling your own and usually
-- used in combination with `handlerLocal` to provide local isolated state)
newtype Local a e ans = Local (IORef a)

-- | Unsafe `IO` in the `Eff` monad.
{-# INLINE unsafeIO #-}
unsafeIO :: IO a -> Eff e a
unsafeIO :: IO a -> Eff e a
unsafeIO IO a
io = let x :: a
x = IO a -> a
forall (m :: * -> *) a. PrimBase m => m a -> a
unsafeInlinePrim IO a
io in a -> Eff e a -> Eff e a
seq a
x ((Context e -> Ctl e a) -> Eff e a
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff ((Context e -> Ctl e a) -> Eff e a)
-> (Context e -> Ctl e a) -> Eff e a
forall a b. (a -> b) -> a -> b
$ \Context e
_ -> a -> Ctl e a
forall e a. a -> Ctl e a
Pure a
x)

-- | Get the value of the local state.
{-# INLINE lget #-}
lget :: Local a e ans -> Op () a e ans
lget :: Local a e ans -> Op () a e ans
lget (Local IORef a
r) = (forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> () -> Eff e' a)
-> Op () a e ans
forall a b e ans.
(forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
Op (\Marker h e ans
m Context e
ctx ()
x -> IO a -> Eff e' a
forall a e. IO a -> Eff e a
unsafeIO (() -> IO a -> IO a
seq ()
x (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r))

-- | Set the value of the local state.
{-# INLINE lput #-}
lput :: Local a e ans -> Op a () e ans
lput :: Local a e ans -> Op a () e ans
lput (Local IORef a
r) = (forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' ())
-> Op a () e ans
forall a b e ans.
(forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
Op (\Marker h e ans
m Context e
ctx a
x -> IO () -> Eff e' ()
forall a e. IO a -> Eff e a
unsafeIO (IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
r a
x))

-- | Update the value of the local state.
{-# INLINE lmodify #-}
lmodify :: Local a e ans -> Op (a -> a) () e ans
lmodify :: Local a e ans -> Op (a -> a) () e ans
lmodify (Local IORef a
r) = (forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> (a -> a) -> Eff e' ())
-> Op (a -> a) () e ans
forall a b e ans.
(forall (h :: * -> * -> *) e'.
 In h e' =>
 Marker h e ans -> Context e -> a -> Eff e' b)
-> Op a b e ans
Op (\Marker h e ans
m Context e
ctx a -> a
f -> IO () -> Eff e' ()
forall a e. IO a -> Eff e a
unsafeIO (do{ a
x <- IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r; IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
r (a -> IO ()) -> a -> IO ()
forall a b. (a -> b) -> a -> b
$! (a -> a
f a
x) }))

-- | Get the value of the local state if it is the top handler.
localGet :: Eff (Local a :* e) a
localGet :: Eff (Local a :* e) a
localGet = (forall e' ans. Local a e' ans -> Op () a e' ans)
-> () -> Eff (Local a :* e) a
forall (h :: * -> * -> *) e a b.
In h e =>
(forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
perform forall e' ans. Local a e' ans -> Op () a e' ans
forall a e ans. Local a e ans -> Op () a e ans
lget ()

-- | Set the value of the local state if it is the top handler.
localPut :: a -> Eff (Local a :* e) ()
localPut :: a -> Eff (Local a :* e) ()
localPut a
x = (forall e' ans. Local a e' ans -> Op a () e' ans)
-> a -> Eff (Local a :* e) ()
forall (h :: * -> * -> *) e a b.
In h e =>
(forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
perform forall e' ans. Local a e' ans -> Op a () e' ans
forall a e ans. Local a e ans -> Op a () e ans
lput a
x

-- | Update the value of the local state if it is the top handler.
localModify :: (a -> a) -> Eff (Local a :* e) ()
localModify :: (a -> a) -> Eff (Local a :* e) ()
localModify a -> a
f = (forall e' ans. Local a e' ans -> Op (a -> a) () e' ans)
-> (a -> a) -> Eff (Local a :* e) ()
forall (h :: * -> * -> *) e a b.
In h e =>
(forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
perform forall e' ans. Local a e' ans -> Op (a -> a) () e' ans
forall a e ans. Local a e ans -> Op (a -> a) () e ans
lmodify a -> a
f

-- A special prompt that saves and restores state per resumption
mpromptIORef :: IORef a -> Eff e b -> Eff e b
mpromptIORef :: IORef a -> Eff e b -> Eff e b
mpromptIORef IORef a
r Eff e b
action
  = (Context e -> Ctl e b) -> Eff e b
forall e a. (Context e -> Ctl e a) -> Eff e a
Eff ((Context e -> Ctl e b) -> Eff e b)
-> (Context e -> Ctl e b) -> Eff e b
forall a b. (a -> b) -> a -> b
$ \Context e
ctx -> case (Eff e b -> Context e -> Ctl e b
forall e a. Eff e a -> Context e -> Ctl e a
unEff Eff e b
action Context e
ctx) of
      p :: Ctl e b
p@(Pure b
_) -> Ctl e b
p
      Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e b
cont
        -> do a
val <- Eff e a -> Context e -> Ctl e a
forall e a. Eff e a -> Context e -> Ctl e a
unEff (IO a -> Eff e a
forall a e. IO a -> Eff e a
unsafeIO (IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r)) Context e
ctx                     -- save current value on yielding
              let cont' :: b -> Eff e b
cont' b
x = do IO () -> Eff e ()
forall a e. IO a -> Eff e a
unsafeIO (IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
r a
val)  -- restore saved value on resume
                               IORef a -> Eff e b -> Eff e b
forall a e b. IORef a -> Eff e b -> Eff e b
mpromptIORef IORef a
r (b -> Eff e b
cont b
x)
              Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e b) -> Ctl e b
forall e a (h :: * -> * -> *) b e' ans.
Marker h e' ans
-> ((b -> Eff e' ans) -> Eff e' ans) -> (b -> Eff e a) -> Ctl e a
Control Marker h e' ans
m (b -> Eff e' ans) -> Eff e' ans
op b -> Eff e b
cont'

-- | Create an `IORef` connected to a prompt. The value of
-- the `IORef` is saved and restored through resumptions.
unsafePromptIORef :: a -> (Marker h e b -> IORef a -> Eff e b) -> Eff e b
unsafePromptIORef :: a -> (Marker h e b -> IORef a -> Eff e b) -> Eff e b
unsafePromptIORef a
init Marker h e b -> IORef a -> Eff e b
action
  = (Marker h e b -> Eff e b) -> Eff e b
forall (h :: * -> * -> *) e a. (Marker h e a -> Eff e a) -> Eff e a
freshMarker ((Marker h e b -> Eff e b) -> Eff e b)
-> (Marker h e b -> Eff e b) -> Eff e b
forall a b. (a -> b) -> a -> b
$ \Marker h e b
m ->
    do IORef a
r <- IO (IORef a) -> Eff e (IORef a)
forall a e. IO a -> Eff e a
unsafeIO (a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef a
init)
       IORef a -> Eff e b -> Eff e b
forall a e b. IORef a -> Eff e b -> Eff e b
mpromptIORef IORef a
r (Marker h e b -> IORef a -> Eff e b
action Marker h e b
m IORef a
r)

-- | Create a local state handler with an initial state of type @a@,
-- with a return function to combine the final result with the final state to a value of type @b@.
{-# INLINE localRet #-}
localRet :: a -> (ans -> a -> b) -> Eff (Local a :* e) ans -> Eff e b
localRet :: a -> (ans -> a -> b) -> Eff (Local a :* e) ans -> Eff e b
localRet a
init ans -> a -> b
ret Eff (Local a :* e) ans
action
  = a -> (Marker (Local a) e b -> IORef a -> Eff e b) -> Eff e b
forall a (h :: * -> * -> *) e b.
a -> (Marker h e b -> IORef a -> Eff e b) -> Eff e b
unsafePromptIORef a
init ((Marker (Local a) e b -> IORef a -> Eff e b) -> Eff e b)
-> (Marker (Local a) e b -> IORef a -> Eff e b) -> Eff e b
forall a b. (a -> b) -> a -> b
$ \Marker (Local a) e b
m IORef a
r ->  -- set a fresh prompt with marker `m`
        do ans
x <- (Context e -> Context (Local a :* e))
-> Eff (Local a :* e) ans -> Eff e ans
forall e' e a. (Context e' -> Context e) -> Eff e a -> Eff e' a
ctxMap (\Context e
ctx -> Marker (Local a) e b
-> Local a e b
-> ContextT e e
-> Context e
-> Context (Local a :* e)
forall (h :: * -> * -> *) e' ans e.
Marker h e' ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker (Local a) e b
m (IORef a -> Local a e b
forall a e ans. IORef a -> Local a e ans
Local IORef a
r) ContextT e e
forall e. ContextT e e
CTId Context e
ctx) Eff (Local a :* e) ans
action -- and call action with the extra evidence
           a
y <- IO a -> Eff e a
forall a e. IO a -> Eff e a
unsafeIO (IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r)
           b -> Eff e b
forall (m :: * -> *) a. Monad m => a -> m a
return (ans -> a -> b
ret ans
x a
y)

-- | Create a local state handler with an initial state of type @a@.
{-# INLINE local #-}
local :: a -> Eff (Local a :* e) ans -> Eff e ans
local :: a -> Eff (Local a :* e) ans -> Eff e ans
local a
init Eff (Local a :* e) ans
action
  = a -> (ans -> a -> ans) -> Eff (Local a :* e) ans -> Eff e ans
forall a ans b e.
a -> (ans -> a -> b) -> Eff (Local a :* e) ans -> Eff e b
localRet a
init ans -> a -> ans
forall a b. a -> b -> a
const Eff (Local a :* e) ans
action

-- | Create a new handler for @h@ which can access the /locally isolated state/ @`Local` a@.
-- This is fully local to the handler @h@ only and not visible in the @action@ as
-- apparent from its effect context (which does /not/ contain @`Local` a@). The
-- @ret@ argument can be used to transform the final result combined with the final state.
{-# INLINE handlerLocalRet #-}
handlerLocalRet :: a -> (ans -> a -> b) -> (h (Local a :* e) b) -> Eff (h :* e) ans -> Eff e b
handlerLocalRet :: a
-> (ans -> a -> b)
-> h (Local a :* e) b
-> Eff (h :* e) ans
-> Eff e b
handlerLocalRet a
init ans -> a -> b
ret h (Local a :* e) b
h Eff (h :* e) ans
action
  = a -> Eff (Local a :* e) b -> Eff e b
forall a e ans. a -> Eff (Local a :* e) ans -> Eff e ans
local a
init (Eff (Local a :* e) b -> Eff e b)
-> Eff (Local a :* e) b -> Eff e b
forall a b. (a -> b) -> a -> b
$ (ans -> Eff (Local a :* e) b)
-> h (Local a :* e) b -> Eff (h :* e) ans -> Eff (Local a :* e) b
forall ans (h' :: * -> * -> *) e b (h :: * -> * -> *).
(ans -> Eff (h' :* e) b)
-> h (h' :* e) b -> Eff (h :* e) ans -> Eff (h' :* e) b
handlerHideRetEff (\ans
x -> do{ a
y <- Eff (Local a :* e) a
forall a e. Eff (Local a :* e) a
localGet; b -> Eff (Local a :* e) b
forall (m :: * -> *) a. Monad m => a -> m a
return (ans -> a -> b
ret ans
x a
y)}) h (Local a :* e) b
h Eff (h :* e) ans
action

-- | Create a new handler for @h@ which can access the /locally isolated state/ @`Local` a@.
-- This is fully local to the handler @h@ only and not visible in the @action@ as
-- apparent from its effect context (which does /not/ contain @`Local` a@).
--
-- @
-- data State a e ans = State { get :: `Op` () a e ans, put :: `Op` a () e ans  }
--
-- state :: a -> `Eff` (State a `:*` e) ans -> `Eff` e ans
-- state init = `handlerLocal` init (State{ get = `function` (\\_ -> `perform` `lget` ()),
--                                        put = `function` (\\x -> `perform` `lput` x) })
--
-- test = `runEff` $
--        state (41::Int) $
--        inc                -- see `:?`
-- @
{-# INLINE handlerLocal #-}
handlerLocal :: a -> (h (Local a :* e) ans) -> Eff (h :* e) ans -> Eff e ans
handlerLocal :: a -> h (Local a :* e) ans -> Eff (h :* e) ans -> Eff e ans
handlerLocal a
init h (Local a :* e) ans
h Eff (h :* e) ans
action
  = a -> Eff (Local a :* e) ans -> Eff e ans
forall a e ans. a -> Eff (Local a :* e) ans -> Eff e ans
local a
init (h (Local a :* e) ans -> Eff (h :* e) ans -> Eff (Local a :* e) ans
forall (h :: * -> * -> *) (h' :: * -> * -> *) e ans.
h (h' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* e) ans
handlerHide h (Local a :* e) ans
h Eff (h :* e) ans
action)