@@ -10,7 +10,7 @@ import Effect.Default
1010%access public
1111-- ----------------------------------------------------------------- [ Effects ]
1212||| The Effect type describes effectful computations.
13−|||
13+|||
1414||| This type is parameterised by:
1515||| + The input resource.
1616||| + The return type of the computation.
@@ -28,11 +28,11 @@ data EFFECT : Type where
2828||| underlying computation context `m` for execution.
2929class Handler (e : Effect) (m : Type -> Type) where
3030 ||| How to handle the effect.
31− |||
31+ |||
3232 ||| @ r The resource being handled.
3333 ||| @ eff The effect to be applied.
3434 ||| @ k The continuation to pass the result of the effect
35− covering handle : (r : res) -> (eff : e t res resk) ->
35+ covering handle : (r : res) -> (eff : e t res resk) ->
3636 (k : ((x : t) -> resk x -> m a)) -> m a
3737
3838||| Get the resource type (handy at the REPL to find out about an effect)
@@ -48,7 +48,7 @@ resourceType (MkEff t e) = t
4848syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
4949
5050-- The state transition is dependent on a result `b`, a bound variable.
51−syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
51+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
5252 = eff inst (\b => outst)
5353
5454--- A simple state transition
@@ -68,7 +68,7 @@ namespace Env
6868 data Env : (m : Type -> Type) -> List EFFECT -> Type where
6969 Nil : Env m Nil
7070 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
71−
71+
7272data EffElem : Effect -> Type ->
7373 List EFFECT -> Type where
7474 Here : EffElem x a (MkEff a x :: xs)
@@ -129,7 +129,7 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
129129
130130-- ------------------------------------------------- [ The Language of Effects ]
131131||| Definition of a language of effectful programs.
132−|||
132+|||
133133||| @ x The return type of the result.
134134||| @ es The list of allowed side-effects.
135135||| @ ce Function to compute a new list of allowed side-effects.
@@ -139,7 +139,7 @@ data Eff : (x : Type)
139139 value : a -> Eff a xs (\v => xs)
140140 with_val : (val : a) -> Eff () xs (\v => xs' val) ->
141141 Eff a xs xs'
142− ebind : Eff a xs xs' ->
142+ ebind : Eff a xs xs' ->
143143 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
144144 callP : (prf : EffElem e a xs) ->
145145 (eff : e t a b) ->
@@ -148,18 +148,18 @@ data Eff : (x : Type)
148148 liftP : (prf : SubList ys xs) ->
149149 Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
150150
151− (:-) : (l : ty) ->
152− Eff t [x] xs' -> -- [x] (\v => xs) ->
151+ (:-) : (l : ty) ->
152+ Eff t [x] xs' -> -- [x] (\v => xs) ->
153153 Eff t [l ::: x] (\v => map (l :::) (xs' v))
154154
155−(>>=) : Eff a xs xs' ->
155+(>>=) : Eff a xs xs' ->
156156 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
157−(>>=) = ebind
157+(>>=) = ebind
158158
159159-- namespace SimpleBind
160−-- (>>=) : Eff m a xs (\v => xs) ->
160+-- (>>=) : Eff m a xs (\v => xs) ->
161161-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
162−-- (>>=) = ebind
162+-- (>>=) = ebind
163163
164164||| Run a subprogram which results in an effect state the same as the input.
165165staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
@@ -182,7 +182,7 @@ pure = value
182182
183183syntax pureM [val] = with_val val (pure ())
184184
185−(<$>) : Eff (a -> b) xs (\v => xs) ->
185+(<$>) : Eff (a -> b) xs (\v => xs) ->
186186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
187187(<$>) prog v = do fn <- prog
188188 arg <- v
@@ -205,7 +205,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
205205
206206eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
207207eff env (value x) k = k x env
208−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
208+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
209209eff env (prog `ebind` c) k
210210 = eff env prog (\p', env' => eff env' (c p') k)
211211eff env (callP prf effP) k = execEff env prf effP k
@@ -248,24 +248,48 @@ lift e {prf} = liftP prf e
248248
249249
250250-- --------------------------------------------------------- [ Running Effects ]
251−
252−||| Run an effectful program
253−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff a xs xs' -> m a
251+||| Run an effectful program.
252+|||
253+||| The content (`m`) in which to run the program is taken from the
254+||| environment in which the program is called. The `env` argument is
255+||| implicit and initialised automatically.
256+|||
257+||| @prog The effectful program to run.
258+run : Applicative m => {default MkDefaultEnv env : Env m xs}
259+ -> (prog : Eff a xs xs') -> m a
254260run {env} prog = eff env prog (\r, env => pure r)
255261
256−runPure : {default MkDefaultEnv env : Env id xs} -> Eff a xs xs' -> a
262+||| Run an effectful program in the identity context.
263+|||
264+||| A helper function useful for when the given context is 'pure'.
265+||| The `env` argument is implicit and initialised automatically.
266+|||
267+||| @prog The effectful program to run.
268+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a
257269runPure {env} prog = eff env prog (\r, env => r)
258270
259−runInit : Applicative m => Env m xs -> Eff a xs xs' -> m a
271+||| Run an effectful program in a given context `m` with a default value for the environment.
272+|||
273+||| This is useful for when there is no default environment for the given context.
274+|||
275+||| @env The environment to use.
276+||| @prog The effectful program to run.
277+runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a
260278runInit env prog = eff env prog (\r, env => pure r)
261279
262−runPureInit : Env id xs -> Eff a xs xs' -> a
280+||| Run an effectful program with a given default value for the environment.
281+|||
282+||| A helper function useful for when the given context is 'pure' and there is no default environment.
283+|||
284+||| @env The environment to use.
285+||| @prog The effectful program to run.
286+runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a
263287runPureInit env prog = eff env prog (\r, env => r)
264288
265289runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
266290runWith inj env prog = eff env prog (\r, env => inj r)
267291
268−runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
292+runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
269293 m (x : a ** Env m (xs' x))
270294runEnv env prog = eff env prog (\r, env => pure (r ** env))
271295