@@ -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,28 +48,27 @@ 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
5555syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
5656
5757-- --------------------------------------- [ Properties and Proof Construction ]
58−using (xs : List a, ys : List a)
59− data SubList : List a -> List a -> Type where
60− SubNil : SubList {a} [] []
61− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
62− Drop : SubList xs ys -> SubList xs (x :: ys)
58+data SubList : List a -> List a -> Type where
59+ SubNil : SubList [] []
60+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
61+ Drop : SubList xs ys -> SubList xs (x :: ys)
6362
64− subListId : SubList xs xs
65− subListId {xs = Nil} = SubNil
66− subListId {xs = x :: xs} = Keep subListId
63+subListId : SubList xs xs
64+subListId {xs = Nil} = SubNil
65+subListId {xs = x :: xs} = Keep subListId
6766
6867namespace Env
6968 data Env : (m : Type -> Type) -> List EFFECT -> Type where
7069 Nil : Env m Nil
7170 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
72−
71+
7372data EffElem : Effect -> Type ->
7473 List EFFECT -> Type where
7574 Here : EffElem x a (MkEff a x :: xs)
@@ -129,71 +128,62 @@ relabel {xs = []} l [] = []
129128relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
130129
131130-- ------------------------------------------------- [ The Language of Effects ]
132−||| Definition of an Effect.
133−|||
134−||| @ m The computation context
131+||| Definition of a language of effectful programs.
132+|||
135133||| @ x The return type of the result.
136134||| @ es The list of allowed side-effects.
137135||| @ ce Function to compute a new list of allowed side-effects.
138−data Eff : (m : Type -> Type)
139− -> (x : Type)
136+data Eff : (x : Type)
140137 -> (es : List EFFECT)
141138 -> (ce : x -> List EFFECT) -> Type where
142− value : a -> Eff m a xs (\v => xs)
143− with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
144− Eff m a xs xs'
145− ebind : Eff m a xs xs' ->
146− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
139+ value : a -> Eff a xs (\v => xs)
140+ with_val : (val : a) -> Eff () xs (\v => xs' val) ->
141+ Eff a xs xs'
142+ ebind : Eff a xs xs' ->
143+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
147144 callP : (prf : EffElem e a xs) ->
148145 (eff : e t a b) ->
149− Eff m t xs (\v => updateResTy v xs prf eff)
146+ Eff t xs (\v => updateResTy v xs prf eff)
150147
151148 liftP : (prf : SubList ys xs) ->
152− Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
153− newInit : Handler e m =>
154− res ->
155− Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
156− Eff m a xs (\v => xs')
157− catch : Catchable m err =>
158− Eff m a xs xs' -> (err -> Eff m a xs xs') ->
159− Eff m a xs xs'
160−
161− (:-) : (l : ty) ->
162− Eff m t [x] xs' -> -- [x] (\v => xs) ->
163− Eff m t [l ::: x] (\v => map (l :::) (xs' v))
164−
165−(>>=) : Eff m a xs xs' ->
166− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
167−(>>=) = ebind
149+ Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
150+
151+ (:-) : (l : ty) ->
152+ Eff t [x] xs' -> -- [x] (\v => xs) ->
153+ Eff t [l ::: x] (\v => map (l :::) (xs' v))
154+
155+(>>=) : Eff a xs xs' ->
156+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
157+(>>=) = ebind
168158
169159-- namespace SimpleBind
170−-- (>>=) : Eff m a xs (\v => xs) ->
160+-- (>>=) : Eff m a xs (\v => xs) ->
171161-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
172−-- (>>=) = ebind
162+-- (>>=) = ebind
173163
174164||| Run a subprogram which results in an effect state the same as the input.
175−staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)
165+staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
176166staticEff = id
177167
178168||| Explicitly give the expected set of result effects for an effectful
179169||| operation.
180−toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')
170+toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
181171toEff xs' = id
182172
183−return : a -> Eff m a xs (\v => xs)
173+return : a -> Eff a xs (\v => xs)
184174return x = value x
185175
186176-- ------------------------------------------------------ [ for idiom brackets ]
187177
188178infixl 2 <$>
189179
190−pure : a -> Eff m a xs (\v => xs)
180+pure : a -> Eff a xs (\v => xs)
191181pure = value
192182
193183syntax pureM [val] = with_val val (pure ())
194184
195−(<$>) : Eff m (a -> b) xs (\v => xs) ->
196− Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
185+(<$>) : Eff (a -> b) xs (\v => xs) ->
186+ Eff a xs (\v => xs) -> Eff b xs (\v => xs)
197187(<$>) prog v = do fn <- prog
198188 arg <- v
199189 return (fn arg)
@@ -213,20 +203,15 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
213203-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
214204-- updates can be propagated even through failing computations?
215205
216−eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
206+eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
217207eff env (value x) k = k x env
218−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')
219209eff env (prog `ebind` c) k
220210 = eff env prog (\p', env' => eff env' (c p') k)
221211eff env (callP prf effP) k = execEff env prf effP k
222212eff env (liftP prf effP) k
223213 = let env' = dropEnv env prf in
224214 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
225−eff env (newInit r prog) k
226− = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)
227−eff env (catch prog handler) k
228− = catch (eff env prog k)
229− (\e => eff env (handler e) k)
230215-- FIXME:
231216-- xs is needed explicitly because otherwise the pattern binding for
232217-- 'l' appears too late. Solution seems to be to reorder patterns at the
@@ -249,84 +234,56 @@ syntax MkDefaultEnv = with Env
249234
250235call : {a, b: _} -> {e : Effect} ->
251236 (eff : e t a b) ->
252− {auto prf : EffElem e a xs} ->
253− Eff m t xs (\v => updateResTy v xs prf eff)
237+ {default tactics { search 100; }
238+ prf : EffElem e a xs} ->
239+ Eff t xs (\v => updateResTy v xs prf eff)
254240call e {prf} = callP prf e
255241
256242implicit
257−lift : Eff m t ys ys' ->
258− {auto prf : SubList ys xs} ->
259− Eff m t xs (\v => updateWith (ys' v) xs prf)
243+lift : Eff t ys ys' ->
244+ {default tactics { search 100; }
245+ prf : SubList ys xs} ->
246+ Eff t xs (\v => updateWith (ys' v) xs prf)
260247lift e {prf} = liftP prf e
261248
262249
263−new : Handler e m =>
264− {default default r : res} ->
265− Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
266− Eff m a xs (\v => xs')
267−new {r} e = newInit r e
268−
269250-- --------------------------------------------------------- [ Running Effects ]
270251
271−||| Run an effectful program.
272−|||
273−||| The content (`m`) in which to run the program is taken from the environment in which the program is called.
274−||| The `env` argument is implicit and initialised automatically.
275−|||
276−||| @prog The effectful program to run.
277−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> (prog : Eff m a xs xs') -> m a
252+||| Run an effectful program
253+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff a xs xs' -> m a
278254run {env} prog = eff env prog (\r, env => pure r)
279255
280−||| Run an effectful program in the identity context `id`.
281−|||
282−||| A helper function useful for when the given context is 'pure'.
283−||| The `env` argument is implicit and initialised automatically.
284−|||
285−||| @prog The effectful program to run.
286−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff id a xs xs') -> a
256+runPure : {default MkDefaultEnv env : Env id xs} -> Eff a xs xs' -> a
287257runPure {env} prog = eff env prog (\r, env => r)
288258
289−||| Run an effectful program with a default value for the environment context.
290−|||
291−||| This is useful for when no default value exists for a given resource type.
292−|||
293−||| @val The default value for the resource type.
294−||| @prog The effectful program to run.
295−runInit : Applicative m => (val : Env m xs) -> (prog : Eff m a xs xs') -> m a
259+runInit : Applicative m => Env m xs -> Eff a xs xs' -> m a
296260runInit env prog = eff env prog (\r, env => pure r)
297261
298−||| Run an effectful program in the identity context `id` with a given default value for the environment context.
299−|||
300−||| A helper function useful for when the given context is 'pure'.
301−|||
302−||| @val The default value for the resource type.
303−||| @prog The effectful program to run.
304−runPureInit : (val : Env id xs) -> (prog : Eff id a xs xs') -> a
262+runPureInit : Env id xs -> Eff a xs xs' -> a
305263runPureInit env prog = eff env prog (\r, env => r)
306264
307−runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
265+runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
308266runWith inj env prog = eff env prog (\r, env => inj r)
309267
310−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
268+runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
311269 m (x : a ** Env m (xs' x))
312270runEnv env prog = eff env prog (\r, env => pure (r ** env))
313271
314272-- ----------------------------------------------- [ some higher order things ]
315273
316−mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
274+mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
317275mapE f [] = pure []
318276mapE f (x :: xs) = [| f x :: mapE f xs |]
319277
320278
321−mapVE : Applicative m =>
322− (a -> {xs} Eff m b) ->
323− Vect n a ->
324− {xs} Eff m (Vect n b)
279+mapVE : (a -> {xs} Eff b) ->
280+ Vect n a ->
281+ {xs} Eff (Vect n b)
325282mapVE f [] = pure []
326283mapVE f (x :: xs) = [| f x :: mapVE f xs |]
327284
328285
329−when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()
286+when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
330287when True e = Force e
331288when False e = pure ()
332289