{-# 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)
              GADTs,
              MultiParamTypeClasses,
              FunctionalDependencies,
              Rank2Types
#-}
{-|
Description : Efficient effect handlers based on Evidence translation
Copyright   : (c) 2020, Microsoft Research; Daan Leijen; Ningning Xie
License     : MIT
Maintainer  : xnning@hku.hk; daan@microsoft.com
Stability   : Experimental

Efficient effect handlers based on Evidence translation. The implementation
is based on /"Effect Handlers, Evidently"/, Ningning Xie /et al./, ICFP 2020 [(pdf)](https://www.microsoft.com/en-us/research/publication/effect-handlers-evidently),
and the interface and design is 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).

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

@
\{\-\# LANGUAGE  TypeOperators, FlexibleContexts, Rank2Types  \#\-\}
import Control.Ev.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,

Daan Leijen and Ningning Xie,  May 2020.

-}
module Control.Ev.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.Ev.Ctl hiding (Local)
import Data.IORef

-- import Unsafe.Coerce     (unsafeCoerce)

infixr 5 :*

-------------------------------------------------------
-- The handler context
-------------------------------------------------------

-- | An effect context is a type-level list of effects.
-- A concrete effect context has the form @(h1 :* h2 :* ... :* hn :* ())@.
-- An effect context can also be polymorpic, as @(h :* e)@, denoting a top handler
-- @h@ with a tail @e@. For example the type of `handler` reflects that in
-- an expression @(`handler` hnd action)@ that
-- the @action@ can perform operations in @h@ as that is now the top handler in the
-- effect context for @action@:
--
-- @
-- `handler` :: h e ans -> `Eff` (h `:*` e) ans -> `Eff` e ans
-- @
--
-- (Note: The effects in a context are partially applied types -- an effect @h e ans@
-- denotes a full effect handler (as a value) defined in an effect context @e@ and
-- with answer type @ans@. In the effect context type though, these types are abstract
-- and we use the partial type @h@ do denote the effect)
data (h :: * -> * -> *) :* e

-- | A runtime context @Context e@ corresponds always to the effect context @e@.
data Context e where
  CCons :: !(Marker ans) -> !(h e' ans) -> !(ContextT e e') -> !(Context e) -> Context (h :* e)
  CNil  :: Context ()

-- A context transformer: this could be defined as a regular function as
-- >  type ContextT e e' = Context e -> Context e'
-- but we use an explicit representation as a GADT for the identity and
-- `CCons` versions of the function as that allows the compiler to optimize
-- much better for the cases where the function is known.
data ContextT e e' where
  CTCons :: !(Marker ans) -> !(h e' ans) -> !(ContextT e e') -> ContextT e (h :* e)
  CTId   :: 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 ans
m h e' ans
h ContextT e e'
g) Context e
ctx = Marker ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker 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 (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 ans
_ h e' ans
_ ContextT e e'
_ Context e
ctx)   = Context e
Context e
ctx


-------------------------------------------------------
-- The Effect monad
-------------------------------------------------------

-- | The effect monad in an effect context @e@ with result @a@
newtype Eff e a = Eff (Context e -> Ctl a)

lift :: Ctl a -> Eff e a
lift :: Ctl a -> Eff e a
lift Ctl a
ctl = (Context e -> Ctl a) -> Eff e a
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
_ -> Ctl a
ctl)

under :: Context e -> Eff e a -> Ctl a
under :: Context e -> Eff e a -> Ctl a
under Context e
ctx (Eff Context e -> Ctl a
eff)  = Context e -> Ctl a
eff Context e
ctx


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 a) -> Eff e a
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
ctx -> a -> Ctl a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x)
  (Eff Context e -> Ctl a
eff) >>= :: Eff e a -> (a -> Eff e b) -> Eff e b
>>= a -> Eff e b
f   = (Context e -> Ctl b) -> Eff e b
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
ctx -> do a
x <- Context e -> Ctl a
eff Context e
ctx
                                      Context e -> Eff e b -> Ctl b
forall e a. Context e -> Eff e a -> Ctl a
under Context e
ctx (a -> Eff e b
f a
x))

-- | Use @handler hnd action@ to handle effect @h@ with
-- handler @hnd@ in @action@ (which has @h@ in its effect context now as @h :* e@).
-- For example:
--
-- @
-- data Reader a e ans = Reader { ask :: `Op` () a e ans }
--
-- reader :: a -> `Eff` (Reader a `:*` e) ans -> `Eff` e ans
-- reader x = `handler` (Reader{ ask = `value` x })
-- @
{-# 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
  = (Context e -> Ctl ans) -> Eff e ans
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
ctx -> (Marker ans -> Ctl ans) -> Ctl ans
forall a. (Marker a -> Ctl a) -> Ctl a
prompt ((Marker ans -> Ctl ans) -> Ctl ans)
-> (Marker ans -> Ctl ans) -> Ctl ans
forall a b. (a -> b) -> a -> b
$ \Marker ans
m ->                      -- set a fresh prompt with marker `m`
                 do Context (h :* e) -> Eff (h :* e) ans -> Ctl ans
forall e a. Context e -> Eff e a -> Ctl a
under (Marker ans
-> h e ans -> ContextT e e -> Context e -> Context (h :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker ans
m h e ans
h ContextT e e
forall e. ContextT e e
CTId Context e
ctx) Eff (h :* e) ans
action) -- and call action with the extra evidence

-- | Run an effect monad in an empty context (as all effects need to be handled)
runEff :: Eff () a -> a
runEff :: Eff () a -> a
runEff (Eff Context () -> Ctl a
eff)  = Ctl a -> a
forall a. Ctl a -> a
runCtl (Context () -> Ctl a
eff Context ()
CNil)


-- | Handle an effect @h@ over @action@ and tranform the final result with
-- the /return/ function @ret@. For example:
--
-- @
-- data Except a e ans = Except { throwError :: forall b. `Op` a b e ans }
--
-- exceptMaybe :: `Eff` (Except a `:*` e) ans -> `Eff` e (Maybe ans)
-- exceptMaybe = `handlerRet` Just (Except{ throwError = except (\\_ -> return Nothing) })
-- @
{-# 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))


-- | Define a handler @h@ that hides the top handler @h'@ from its @action@,
-- while keeping @h'@ is still visible in the operation definitions of @h@.
-- This is used to implement locally isolated state for `handlerLocal` using
-- the regular `local` state. In particular, `handlerLocal` is implemented as:
--
-- @
-- `handlerLocal` :: a -> (h (`Local` a `:*` e) ans) -> `Eff` (h `:*` e) ans -> `Eff` e ans
-- `handlerLocal` init h action = `local` init (`handlerHide` h action)
-- @
{-# 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
  = (Context (h' :* e) -> Ctl ans) -> Eff (h' :* e) ans
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\(CCons Marker ans
m' h e' ans
h' ContextT e e'
g' Context e
ctx') -> (Marker ans -> Ctl ans) -> Ctl ans
forall a. (Marker a -> Ctl a) -> Ctl a
prompt (\Marker ans
m -> Context (h :* e) -> Eff (h :* e) ans -> Ctl ans
forall e a. Context e -> Eff e a -> Ctl a
under (Marker ans
-> h (h' :* e) ans
-> ContextT e (h' :* e)
-> Context e
-> Context (h :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker ans
m h (h' :* e) ans
h (Marker ans -> h e' ans -> ContextT e e' -> ContextT e (h :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans -> h e' ans -> ContextT e e' -> ContextT e (h :* e)
CTCons Marker ans
m' h e' ans
h' ContextT e e'
g') Context e
ctx') Eff (h :* e) ans
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
  = (Context (h' :* e) -> Ctl b) -> Eff (h' :* e) b
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\ctx :: Context (h' :* e)
ctx@(CCons Marker ans
m' h e' ans
h' ContextT e e'
g' Context e
ctx') -> do (Marker b -> Ctl b) -> Ctl b
forall a. (Marker a -> Ctl a) -> Ctl a
prompt (\Marker b
m -> do ans
x <- Context (h :* e) -> Eff (h :* e) ans -> Ctl ans
forall e a. Context e -> Eff e a -> Ctl a
under (Marker b
-> h (h' :* e) b
-> ContextT e (h' :* e)
-> Context e
-> Context (h :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker b
m h (h' :* e) b
h (Marker ans -> h e' ans -> ContextT e e' -> ContextT e (h :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans -> h e' ans -> ContextT e e' -> ContextT e (h :* e)
CTCons Marker ans
m' h e' ans
h' ContextT e e'
g') Context e
ctx') Eff (h :* e) ans
Eff (h :* e) ans
action
                                                           Context (h' :* e) -> Eff (h' :* e) b -> Ctl b
forall e a. Context e -> Eff e a -> Ctl a
under Context (h' :* e)
ctx (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 Context e -> Ctl ans
f) = (Context (h :* e) -> Ctl ans) -> Eff (h :* e) ans
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context (h :* e)
ctx -> Context e -> Ctl ans
f (Context (h :* e) -> Context e
forall (h :: * -> * -> *) e. Context (h :* e) -> Context e
ctail Context (h :* e)
ctx))


---------------------------------------------------------
-- Select a sub context
---------------------------------------------------------

{-| An effect membership constraint: @h :? e@ ensures that the effect handler
@h@ is in the effect context @e@. For example:

@
inc :: (State Int `:?` e) => `Eff` e ()
inc = do i <- `perform` get ()
         `perform` put (i+1) }
@

-}
type h :? e = In h e   -- is `h` in the effect context `e` ?

data SubContext h  = forall e. SubContext !(Context (h :* e))  -- make `e` existential

-- | The @In@ constraint is an alias for `:?`
class In h e where
  subContext :: Context e -> SubContext h  -- ^ Internal method to select a sub context

instance (InEq (HEqual h h') h h' w) => In h (h' :* w) where
  subContext :: Context (h' :* w) -> SubContext h
subContext = Context (h' :* w) -> 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

-- | Internal class used by `:?`.
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 :: (In h e) => (SubContext h -> Ctl a) -> Eff e a
withSubContext :: (SubContext h -> Ctl a) -> Eff e a
withSubContext SubContext h -> Ctl a
f
  = (Context e -> Ctl a) -> Eff e a
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
ctx -> SubContext h -> Ctl a
f (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 -> Marker ans -> Context e -> a -> Ctl b
applyOp :: !(Marker ans -> Context e -> a -> Ctl b) }

{-| Given an operation selector, perform the operation. The type of the selector
function is a bit intimidating, but it just selects the right operation `Op` from the
handler @h@ regardless of the effect context @e'@ and answer type @ans@ where the
handler is defined.

Usually the operation selector is a field in the data type for the effect handler.
For example:

@
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 = `runEff` $
       `handler` (Reader{ ask = `value` "world" }) $
       greet
@

-}
{-# INLINE perform #-}
perform :: (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 -> Ctl b) -> Eff e b
forall (h :: * -> * -> *) e a.
In h e =>
(SubContext h -> Ctl a) -> Eff e a
withSubContext (\(SubContext (CCons Marker ans
m h e' ans
h ContextT e e'
g Context e
ctx)) -> Op a b e' ans -> Marker ans -> Context e' -> a -> Ctl b
forall a b e ans.
Op a b e ans -> Marker ans -> Context e -> a -> Ctl 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 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 = (Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
forall a b e ans.
(Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
Op (\Marker ans
_ Context e
ctx a
x -> Context e -> Eff e b -> Ctl b
forall e a. Context e -> Eff e a -> Ctl a
under 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 = (Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
forall a b e ans.
(Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
Op (\Marker ans
m Context e
ctx a
x -> Marker ans -> ((b -> Ctl ans) -> Ctl ans) -> Ctl b
forall ans b. Marker ans -> ((b -> Ctl ans) -> Ctl ans) -> Ctl b
yield Marker ans
m (((b -> Ctl ans) -> Ctl ans) -> Ctl b)
-> ((b -> Ctl ans) -> Ctl ans) -> Ctl b
forall a b. (a -> b) -> a -> b
$ \b -> Ctl ans
ctlk ->
                              let k :: b -> Eff e ans
k b
y = (Context e -> Ctl ans) -> Eff e ans
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
ctx' -> Context e -> Context e -> (b -> Ctl ans) -> b -> Ctl ans
forall e b a. Context e -> Context e -> (b -> Ctl a) -> b -> Ctl a
guard Context e
ctx Context e
ctx' b -> Ctl ans
ctlk b
y)
                              in Context e -> Eff e ans -> Ctl ans
forall e a. Context e -> Eff e a -> Ctl a
under Context e
ctx (a -> (b -> Eff e ans) -> Eff e ans
f a
x b -> Eff e ans
k))


-- | 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 = (Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
forall a b e ans.
(Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
Op (\Marker ans
m Context e
ctx a
x -> Marker ans -> ((b -> Ctl ans) -> Ctl ans) -> Ctl b
forall ans b. Marker ans -> ((b -> Ctl ans) -> Ctl ans) -> Ctl b
yield Marker ans
m (((b -> Ctl ans) -> Ctl ans) -> Ctl b)
-> ((b -> Ctl ans) -> Ctl ans) -> Ctl b
forall a b. (a -> b) -> a -> b
$ \b -> Ctl ans
ctlk -> Context e -> Eff e ans -> Ctl ans
forall e a. Context e -> Eff e a -> Ctl a
under Context e
ctx (a -> Eff e ans
f a
x))


guard :: Context e -> Context e -> (b -> Ctl a) -> b -> Ctl a
guard :: Context e -> Context e -> (b -> Ctl a) -> b -> Ctl a
guard Context e
ctx1 Context e
ctx2 b -> Ctl a
k b
x = if (Context e
ctx1 Context e -> Context e -> Bool
forall a. Eq a => a -> a -> Bool
== Context e
ctx2) then b -> Ctl a
k b
x else [Char] -> Ctl a
forall a. HasCallStack => [Char] -> a
error [Char]
"Control.Ev.Eff.guard: unscoped resumption under a different handler context"

instance Eq (Context e) where
  (CCons Marker ans
m1 h e' ans
_ ContextT e e'
_ Context e
ctx1)  == :: Context e -> Context e -> Bool
== (CCons Marker ans
m2 h e' ans
_ ContextT e e'
_ Context e
ctx2)   = (Marker ans -> Marker ans -> Bool
forall a b. Marker a -> Marker b -> Bool
markerEq Marker ans
m1 Marker ans
m2) Bool -> Bool -> Bool
&& (Context e
ctx1 Context e -> Context e -> Bool
forall a. Eq a => a -> a -> Bool
== Context e
Context e
ctx2)
  Context e
CNil                 == Context e
CNil                  = Bool
True


--------------------------------------------------------------------------------
-- 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)

-- | 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) = (Marker ans -> Context e -> () -> Ctl a) -> Op () a e ans
forall a b e ans.
(Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
Op (\Marker ans
m Context e
ctx ()
x -> IO a -> Ctl a
forall a. IO a -> Ctl 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) = (Marker ans -> Context e -> a -> Ctl ()) -> Op a () e ans
forall a b e ans.
(Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
Op (\Marker ans
m Context e
ctx a
x -> IO () -> Ctl ()
forall a. IO a -> Ctl 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) = (Marker ans -> Context e -> (a -> a) -> Ctl ())
-> Op (a -> a) () e ans
forall a b e ans.
(Marker ans -> Context e -> a -> Ctl b) -> Op a b e ans
Op (\Marker ans
m Context e
ctx a -> a
f -> IO () -> Ctl ()
forall a. IO a -> Ctl 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.
(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.
(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.
(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

-- | 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
  = (Context e -> Ctl b) -> Eff e b
forall e a. (Context e -> Ctl a) -> Eff e a
Eff (\Context e
ctx -> a -> (Marker b -> IORef a -> Ctl b) -> Ctl b
forall a b. a -> (Marker b -> IORef a -> Ctl b) -> Ctl b
unsafePromptIORef a
init ((Marker b -> IORef a -> Ctl b) -> Ctl b)
-> (Marker b -> IORef a -> Ctl b) -> Ctl b
forall a b. (a -> b) -> a -> b
$ \Marker b
m IORef a
r ->  -- set a fresh prompt with marker `m`
                 do ans
x <- Context (Local a :* e) -> Eff (Local a :* e) ans -> Ctl ans
forall e a. Context e -> Eff e a -> Ctl a
under (Marker b
-> Local a e b
-> ContextT e e
-> Context e
-> Context (Local a :* e)
forall ans (h :: * -> * -> *) e' e.
Marker ans
-> h e' ans -> ContextT e e' -> Context e -> Context (h :* e)
CCons Marker 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 -> Ctl a
forall a. IO a -> Ctl a
unsafeIO (IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r)
                    b -> Ctl 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)