Prog

An encoding for algebraic effects, based on the freer monad.

Effectful program

data Prog es a where

A program that returns a value of type a and can call operations that belong to some effect e in signature es; this represents a syntax tree whose nodes are operations and leaves are pure values.

Constructors

Val

Fields

• :: a

  pure value

• -> Prog es a

Op

Fields

• :: EffectSum es x

  operation belonging to some effect in es

• -> (x -> Prog es a)

  continuation from the result of the operation

• -> Prog es a

Instances

Monad (Prog es)

Defined in Prog

Methods

(>>=) :: Prog es a -> (a -> Prog es b) -> Prog es b

(>>) :: Prog es a -> Prog es b -> Prog es b

return :: a -> Prog es a

Functor (Prog es)

Defined in Prog

Methods

fmap :: (a -> b) -> Prog es a -> Prog es b

(<$) :: a -> Prog es b -> Prog es a

Applicative (Prog es)

Defined in Prog

Methods

pure :: a -> Prog es a

(<*>) :: Prog es (a -> b) -> Prog es a -> Prog es b

liftA2 :: (a -> b -> c) -> Prog es a -> Prog es b -> Prog es c

(*>) :: Prog es a -> Prog es b -> Prog es b

(<*) :: Prog es a -> Prog es b -> Prog es a

data EffectSum (es :: [* -> *]) (x :: *) :: *

An open sum for an effect signature es, containing an operation e x where e is in es

class FindElem e es => Member (e :: * -> *) (es :: [* -> *]) where

Membership of an effect e in es

Methods

inj :: e x -> EffectSum es x

Inject an operation of type e x into an effect sum

prj :: EffectSum es x -> Maybe (e x)

Attempt to project an operation of type e x out from an effect sum

Instances

FindElem e es => Member e es

Defined in Prog

Methods

inj :: e x -> EffectSum es x

prj :: EffectSum es x -> Maybe (e x)

e ~ e' => Member e '[e']

Defined in Prog

Methods

inj :: e x -> EffectSum '[e'] x

prj :: EffectSum '[e'] x -> Maybe (e x)

Auxiliary functions

run :: Prog '[] a -> a

Run a pure computation

call :: Member e es => e x -> Prog es x

Call an operation of type e x in a computation

discharge :: EffectSum (e ': es) x -> Either (EffectSum es x) (e x)

Discharges an effect e from the front of an effect signature es