@@ -24,6 +24,27 @@ Effect = (x : Type) -> Type -> (x -> Type) -> Type
2424data EFFECT : Type where
2525 MkEff : Type -> Effect -> EFFECT
2626
27+-- 'sig' gives the signature for an effect. There are three versions
28+-- depending on whether there is no state change, a non-dependent change,
29+-- or a dependent change. These are easily disambiguated by type.
30+
31+namespace NoResourceEffect
32+ sig : Effect -> Type -> Type
33+ sig e r = e r () (\v => ())
34+
35+namespace NoUpdateEffect
36+ sig : Effect -> (ret : Type) -> (resource : Type) -> Type
37+ sig e r e_in = e r e_in (\v => e_in)
38+
39+namespace UpdateEffect
40+ sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type
41+ sig e r e_in e_out = e r e_in (\v => e_out)
42+
43+namespace DepUpdateEffect
44+ sig : Effect ->
45+ (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
46+ sig e r e_in e_out = e r e_in e_out
47+
2748||| Handler classes describe how an effect `e` is translated to the
2849||| underlying computation context `m` for execution.
2950class Handler (e : Effect) (m : Type -> Type) where
@@ -60,6 +81,7 @@ data SubList : List a -> List a -> Type where
6081 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
6182 Drop : SubList xs ys -> SubList xs (x :: ys)
6283
84+%hint
6385subListId : SubList xs xs
6486subListId {xs = Nil} = SubNil
6587subListId {xs = x :: xs} = Keep subListId
@@ -133,26 +155,56 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
133155||| @ x The return type of the result.
134156||| @ es The list of allowed side-effects.
135157||| @ ce Function to compute a new list of allowed side-effects.
136−data Eff : (x : Type)
137− -> (es : List EFFECT)
138− -> (ce : x -> List EFFECT) -> Type where
139− value : (val : a) -> Eff a (xs val) xs
140− ebind : Eff a xs xs' ->
141− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
158+data EffM : (m : Type -> Type) -> (x : Type)
159+ -> (es : List EFFECT)
160+ -> (ce : x -> List EFFECT) -> Type where
161+ value : (val : a) -> EffM m a (xs val) xs
162+ ebind : EffM m a xs xs' ->
163+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
142164 callP : (prf : EffElem e a xs) ->
143165 (eff : e t a b) ->
144− Eff t xs (\v => updateResTy v xs prf eff)
166+ EffM m t xs (\v => updateResTy v xs prf eff)
145167
146168 liftP : (prf : SubList ys xs) ->
147− Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
169+ EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
148170
149171 (:-) : (l : ty) ->
150− Eff t [x] xs' -> -- [x] (\v => xs) ->
151− Eff t [l ::: x] (\v => map (l :::) (xs' v))
172+ EffM m t [x] xs' -> -- [x] (\v => xs) ->
173+ EffM m t [l ::: x] (\v => map (l :::) (xs' v))
174+
175+-- Some type synonyms, so we don't always have to write EffM in full
176+
177+namespace SimpleEff
178+ -- Simple effects, no updates
179+ Eff : (x : Type) -> (es : List EFFECT) -> Type
180+ Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
181+
182+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type
183+ EffT m x es = EffM m x es (\v => es)
184+
185+namespace TransEff
186+ -- Dependent effects, updates not dependent on result
187+ Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
188+ Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
189+
190+ EffT : (m : Type -> Type) ->
191+ (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
192+ EffT m x es ce = EffM m x es (\_ => ce)
193+
194+namespace DepEff
195+ -- Dependent effects, updates dependent on result
196+ Eff : (x : Type) -> (es : List EFFECT)
197+ -> (ce : x -> List EFFECT) -> Type
198+ Eff x es ce = {m : Type -> Type} -> EffM m x es ce
199+
200+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
201+ -> (ce : x -> List EFFECT) -> Type
202+ EffT m x es ce = EffM m x es ce
203+
152204
153205%no_implicit
154−(>>=) : Eff a xs xs' ->
155− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
206+(>>=) : EffM m a xs xs' ->
207+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
156208(>>=) = ebind
157209
158210-- namespace SimpleBind
@@ -161,29 +213,29 @@ data Eff : (x : Type)
161213-- (>>=) = ebind
162214
163215||| Run a subprogram which results in an effect state the same as the input.
164−staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
216+staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)
165217staticEff = id
166218
167219||| Explicitly give the expected set of result effects for an effectful
168220||| operation.
169−toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
221+toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
170222toEff xs' = id
171223
172−return : a -> Eff a xs (\v => xs)
224+return : a -> EffM m a xs (\v => xs)
173225return x = value x
174226
175227-- ------------------------------------------------------ [ for idiom brackets ]
176228
177229infixl 2 <*>
178230
179−pure : a -> Eff a xs (\v => xs)
231+pure : a -> EffM m a xs (\v => xs)
180232pure = value
181233
182−pureM : (val : a) -> Eff a (xs val) xs
234+pureM : (val : a) -> EffM m a (xs val) xs
183235pureM = value
184236
185−(<*>) : Eff (a -> b) xs (\v => xs) ->
186− Eff a xs (\v => xs) -> Eff b xs (\v => xs)
237+(<*>) : EffM m (a -> b) xs (\v => xs) ->
238+ EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
187239(<*>) prog v = do fn <- prog
188240 arg <- v
189241 return (fn arg)
@@ -203,7 +255,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
203255-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
204256-- updates can be propagated even through failing computations?
205257
206−eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
258+eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
207259eff env (value x) k = k x env
208260eff env (prog `ebind` c) k
209261 = eff env prog (\p', env' => eff env' (c p') k)
@@ -235,14 +287,14 @@ call : {a, b: _} -> {e : Effect} ->
235287 (eff : e t a b) ->
236288 {default tactics { search 100; }
237289 prf : EffElem e a xs} ->
238− Eff t xs (\v => updateResTy v xs prf eff)
290+ EffM m t xs (\v => updateResTy v xs prf eff)
239291call e {prf} = callP prf e
240292
241293implicit
242−lift : Eff t ys ys' ->
294+lift : EffM m t ys ys' ->
243295 {default tactics { search 100; }
244296 prf : SubList ys xs} ->
245− Eff t xs (\v => updateWith (ys' v) xs prf)
297+ EffM m t xs (\v => updateWith (ys' v) xs prf)
246298lift e {prf} = liftP prf e
247299
248300
@@ -255,7 +307,7 @@ lift e {prf} = liftP prf e
255307|||
256308||| @prog The effectful program to run.
257309run : Applicative m => {default MkDefaultEnv env : Env m xs}
258− -> (prog : Eff a xs xs') -> m a
310+ -> (prog : EffM m a xs xs') -> m a
259311run {env} prog = eff env prog (\r, env => pure r)
260312
261313||| Run an effectful program in the identity context.
@@ -264,7 +316,7 @@ run {env} prog = eff env prog (\r, env => pure r)
264316||| The `env` argument is implicit and initialised automatically.
265317|||
266318||| @prog The effectful program to run.
267−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a
319+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : EffM id a xs xs') -> a
268320runPure {env} prog = eff env prog (\r, env => r)
269321
270322||| Run an effectful program in a given context `m` with a default value for the environment.
@@ -273,7 +325,7 @@ runPure {env} prog = eff env prog (\r, env => r)
273325|||
274326||| @env The environment to use.
275327||| @prog The effectful program to run.
276−runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a
328+runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a
277329runInit env prog = eff env prog (\r, env => pure r)
278330
279331||| Run an effectful program with a given default value for the environment.
@@ -282,31 +334,31 @@ runInit env prog = eff env prog (\r, env => pure r)
282334|||
283335||| @env The environment to use.
284336||| @prog The effectful program to run.
285−runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a
337+runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a
286338runPureInit env prog = eff env prog (\r, env => r)
287339
288−runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
340+runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
289341runWith inj env prog = eff env prog (\r, env => inj r)
290342
291−runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
343+runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
292344 m (x : a ** Env m (xs' x))
293345runEnv env prog = eff env prog (\r, env => pure (r ** env))
294346
295347-- ----------------------------------------------- [ some higher order things ]
296348
297−mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
349+mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)
298350mapE f [] = pure []
299351mapE f (x :: xs) = [| f x :: mapE f xs |]
300352
301353
302−mapVE : (a -> {xs} Eff b) ->
354+mapVE : (a -> {xs} EffM m b) ->
303355 Vect n a ->
304− {xs} Eff (Vect n b)
356+ {xs} EffM m (Vect n b)
305357mapVE f [] = pure []
306358mapVE f (x :: xs) = [| f x :: mapVE f xs |]
307359
308360
309−when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
361+when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()
310362when True e = Force e
311363when False e = pure ()
312364