@@ -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
@@ -69,7 +69,7 @@ namespace Env
6969 data Env : (m : Type -> Type) -> List EFFECT -> Type where
7070 Nil : Env m Nil
7171 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
72−
72+
7373data EffElem : Effect -> Type ->
7474 List EFFECT -> Type where
7575 Here : EffElem x a (MkEff a x :: xs)
@@ -130,7 +130,7 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
130130
131131-- ------------------------------------------------- [ The Language of Effects ]
132132||| Definition of an Effect.
133−|||
133+|||
134134||| @ m The computation context
135135||| @ x The return type of the result.
136136||| @ es The list of allowed side-effects.
@@ -142,7 +142,7 @@ data Eff : (m : Type -> Type)
142142 value : a -> Eff m a xs (\v => xs)
143143 with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
144144 Eff m a xs xs'
145− ebind : Eff m a xs xs' ->
145+ ebind : Eff m a xs xs' ->
146146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
147147 callP : (prf : EffElem e a xs) ->
148148 (eff : e t a b) ->
@@ -151,25 +151,25 @@ data Eff : (m : Type -> Type)
151151 liftP : (prf : SubList ys xs) ->
152152 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
153153 newInit : Handler e m =>
154− res ->
154+ res ->
155155 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
156156 Eff m a xs (\v => xs')
157157 catch : Catchable m err =>
158158 Eff m a xs xs' -> (err -> Eff m a xs xs') ->
159159 Eff m a xs xs'
160160
161− (:-) : (l : ty) ->
162− Eff m t [x] xs' -> -- [x] (\v => xs) ->
161+ (:-) : (l : ty) ->
162+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
163163 Eff m t [l ::: x] (\v => map (l :::) (xs' v))
164164
165−(>>=) : Eff m a xs xs' ->
165+(>>=) : Eff m a xs xs' ->
166166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
167−(>>=) = ebind
167+(>>=) = ebind
168168
169169-- namespace SimpleBind
170−-- (>>=) : Eff m a xs (\v => xs) ->
170+-- (>>=) : Eff m a xs (\v => xs) ->
171171-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
172−-- (>>=) = ebind
172+-- (>>=) = ebind
173173
174174||| Run a subprogram which results in an effect state the same as the input.
175175staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)
@@ -192,7 +192,7 @@ pure = value
192192
193193syntax pureM [val] = with_val val (pure ())
194194
195−(<$>) : Eff m (a -> b) xs (\v => xs) ->
195+(<$>) : Eff m (a -> b) xs (\v => xs) ->
196196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
197197(<$>) prog v = do fn <- prog
198198 arg <- v
@@ -215,7 +215,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
215215
216216eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
217217eff env (value x) k = k x env
218−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
218+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
219219eff env (prog `ebind` c) k
220220 = eff env prog (\p', env' => eff env' (c p') k)
221221eff env (callP prf effP) k = execEff env prf effP k
@@ -263,30 +263,53 @@ lift e {prf} = liftP prf e
263263
264264
265265new : Handler e m =>
266− {default default r : res} ->
266+ {default default r : res} ->
267267 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
268268 Eff m a xs (\v => xs')
269269new {r} e = newInit r e
270270
271271-- --------------------------------------------------------- [ Running Effects ]
272272
273−||| Run an effectful program
274−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
273+||| Run an effectful program.
274+|||
275+||| The content (`m`) in which to run the program is taken from the environment in which the program is called.
276+||| The `env` argument is implicit and initialised automatically.
277+|||
278+||| @prog The effectful program to run.
279+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> (prog : Eff m a xs xs') -> m a
275280run {env} prog = eff env prog (\r, env => pure r)
276281
277−runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a
282+||| Run an effectful program in the identity context `id`.
283+|||
284+||| A helper function useful for when the given context is 'pure'.
285+||| The `env` argument is implicit and initialised automatically.
286+|||
287+||| @prog The effectful program to run.
288+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff id a xs xs') -> a
278289runPure {env} prog = eff env prog (\r, env => r)
279290
280−runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a
291+||| Run an effectful program with a default value for the environment context.
292+|||
293+||| This is useful for when no default value exists for a given resource type.
294+|||
295+||| @val The default value for the resource type.
296+||| @prog The effectful program to run.
297+runInit : Applicative m => (val : Env m xs) -> (prog : Eff m a xs xs') -> m a
281298runInit env prog = eff env prog (\r, env => pure r)
282299
283−runPureInit : Env id xs -> Eff id a xs xs' -> a
300+||| Run an effectful program in the identity context `id` with a given default value for the environment context.
301+|||
302+||| A helper function useful for when the given context is 'pure'.
303+|||
304+||| @val The default value for the resource type.
305+||| @prog The effectful program to run.
306+runPureInit : (val : Env id xs) -> (prog : Eff id a xs xs') -> a
284307runPureInit env prog = eff env prog (\r, env => r)
285308
286309runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
287310runWith inj env prog = eff env prog (\r, env => inj r)
288311
289−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
312+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
290313 m (x : a ** Env m (xs' x))
291314runEnv env prog = eff env prog (\r, env => pure (r ** env))
292315
@@ -297,9 +320,9 @@ mapE f [] = pure []
297320mapE f (x :: xs) = [| f x :: mapE f xs |]
298321
299322
300−mapVE : Applicative m =>
301− (a -> {xs} Eff m b) ->
302− Vect n a ->
323+mapVE : Applicative m =>
324+ (a -> {xs} Eff m b) ->
325+ Vect n a ->
303326 {xs} Eff m (Vect n b)
304327mapVE f [] = pure []
305328mapVE f (x :: xs) = [| f x :: mapVE f xs |]