@@ -24,6 +24,28 @@ 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 four versions
28+-- depending on whether there is no resource needed,
29+-- no state change, a non-dependent change,
30+-- or a dependent change. These are easily disambiguated by type.
31+
32+namespace NoResourceEffect
33+ sig : Effect -> Type -> Type
34+ sig e r = e r () (\v => ())
35+
36+namespace NoUpdateEffect
37+ sig : Effect -> (ret : Type) -> (resource : Type) -> Type
38+ sig e r e_in = e r e_in (\v => e_in)
39+
40+namespace UpdateEffect
41+ sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type
42+ sig e r e_in e_out = e r e_in (\v => e_out)
43+
44+namespace DepUpdateEffect
45+ sig : Effect ->
46+ (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
47+ sig e r e_in e_out = e r e_in e_out
48+
2749||| Handler classes describe how an effect `e` is translated to the
2850||| underlying computation context `m` for execution.
2951class Handler (e : Effect) (m : Type -> Type) where
@@ -60,6 +82,7 @@ data SubList : List a -> List a -> Type where
6082 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
6183 Drop : SubList xs ys -> SubList xs (x :: ys)
6284
85+%hint
6386subListId : SubList xs xs
6487subListId {xs = Nil} = SubNil
6588subListId {xs = x :: xs} = Keep subListId
@@ -133,26 +156,61 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
133156||| @ x The return type of the result.
134157||| @ es The list of allowed side-effects.
135158||| @ 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''
159+data EffM : (m : Type -> Type) -> (x : Type)
160+ -> (es : List EFFECT)
161+ -> (ce : x -> List EFFECT) -> Type where
162+ value : (val : a) -> EffM m a (xs val) xs
163+ ebind : EffM m a xs xs' ->
164+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
142165 callP : (prf : EffElem e a xs) ->
143166 (eff : e t a b) ->
144− Eff t xs (\v => updateResTy v xs prf eff)
167+ EffM m t xs (\v => updateResTy v xs prf eff)
145168
146169 liftP : (prf : SubList ys xs) ->
147− Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
170+ EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
171+
172+ new : Handler e' m => (e : EFFECT) -> resTy ->
173+ {auto prf : e = MkEff resTy e'} ->
174+ EffM m t (e :: es) (\v => e :: es) ->
175+ EffM m t es (\v => es)
148176
149177 (:-) : (l : ty) ->
150− Eff t [x] xs' -> -- [x] (\v => xs) ->
151− Eff t [l ::: x] (\v => map (l :::) (xs' v))
178+ EffM m t [x] xs' -> -- [x] (\v => xs) ->
179+ EffM m t [l ::: x] (\v => map (l :::) (xs' v))
180+
181+-- Some type synonyms, so we don't always have to write EffM in full
182+
183+namespace SimpleEff
184+ -- Simple effects, no updates
185+ Eff : (x : Type) -> (es : List EFFECT) -> Type
186+ Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
187+
188+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type
189+ EffT m x es = EffM m x es (\v => es)
190+
191+namespace TransEff
192+ -- Dependent effects, updates not dependent on result
193+ Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
194+ Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
195+
196+ EffT : (m : Type -> Type) ->
197+ (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
198+ EffT m x es ce = EffM m x es (\_ => ce)
199+
200+namespace DepEff
201+ -- Dependent effects, updates dependent on result
202+ Eff : (x : Type) -> (es : List EFFECT)
203+ -> (ce : x -> List EFFECT) -> Type
204+ Eff x es ce = {m : Type -> Type} -> EffM m x es ce
205+
206+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
207+ -> (ce : x -> List EFFECT) -> Type
208+ EffT m x es ce = EffM m x es ce
209+
152210
153211%no_implicit
154−(>>=) : Eff a xs xs' ->
155− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
212+(>>=) : EffM m a xs xs' ->
213+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
156214(>>=) = ebind
157215
158216-- namespace SimpleBind
@@ -161,29 +219,29 @@ data Eff : (x : Type)
161219-- (>>=) = ebind
162220
163221||| 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)
222+staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)
165223staticEff = id
166224
167225||| Explicitly give the expected set of result effects for an effectful
168226||| operation.
169−toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
227+toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
170228toEff xs' = id
171229
172−return : a -> Eff a xs (\v => xs)
230+return : a -> EffM m a xs (\v => xs)
173231return x = value x
174232
175233-- ------------------------------------------------------ [ for idiom brackets ]
176234
177235infixl 2 <*>
178236
179−pure : a -> Eff a xs (\v => xs)
237+pure : a -> EffM m a xs (\v => xs)
180238pure = value
181239
182−pureM : (val : a) -> Eff a (xs val) xs
240+pureM : (val : a) -> EffM m a (xs val) xs
183241pureM = value
184242
185−(<*>) : Eff (a -> b) xs (\v => xs) ->
186− Eff a xs (\v => xs) -> Eff b xs (\v => xs)
243+(<*>) : EffM m (a -> b) xs (\v => xs) ->
244+ EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
187245(<*>) prog v = do fn <- prog
188246 arg <- v
189247 return (fn arg)
@@ -203,7 +261,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
203261-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
204262-- updates can be propagated even through failing computations?
205263
206−eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
264+eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
207265eff env (value x) k = k x env
208266eff env (prog `ebind` c) k
209267 = eff env prog (\p', env' => eff env' (c p') k)
@@ -211,6 +269,8 @@ eff env (callP prf effP) k = execEff env prf effP k
211269eff env (liftP prf effP) k
212270 = let env' = dropEnv env prf in
213271 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
272+eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
273+ = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
214274-- FIXME:
215275-- xs is needed explicitly because otherwise the pattern binding for
216276-- 'l' appears too late. Solution seems to be to reorder patterns at the
@@ -235,14 +295,14 @@ call : {a, b: _} -> {e : Effect} ->
235295 (eff : e t a b) ->
236296 {default tactics { search 100; }
237297 prf : EffElem e a xs} ->
238− Eff t xs (\v => updateResTy v xs prf eff)
298+ EffM m t xs (\v => updateResTy v xs prf eff)
239299call e {prf} = callP prf e
240300
241301implicit
242−lift : Eff t ys ys' ->
302+lift : EffM m t ys ys' ->
243303 {default tactics { search 100; }
244304 prf : SubList ys xs} ->
245− Eff t xs (\v => updateWith (ys' v) xs prf)
305+ EffM m t xs (\v => updateWith (ys' v) xs prf)
246306lift e {prf} = liftP prf e
247307
248308
@@ -255,7 +315,7 @@ lift e {prf} = liftP prf e
255315|||
256316||| @prog The effectful program to run.
257317run : Applicative m => {default MkDefaultEnv env : Env m xs}
258− -> (prog : Eff a xs xs') -> m a
318+ -> (prog : EffM m a xs xs') -> m a
259319run {env} prog = eff env prog (\r, env => pure r)
260320
261321||| Run an effectful program in the identity context.
@@ -264,7 +324,7 @@ run {env} prog = eff env prog (\r, env => pure r)
264324||| The `env` argument is implicit and initialised automatically.
265325|||
266326||| @prog The effectful program to run.
267−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a
327+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : EffM id a xs xs') -> a
268328runPure {env} prog = eff env prog (\r, env => r)
269329
270330||| Run an effectful program in a given context `m` with a default value for the environment.
@@ -273,7 +333,7 @@ runPure {env} prog = eff env prog (\r, env => r)
273333|||
274334||| @env The environment to use.
275335||| @prog The effectful program to run.
276−runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a
336+runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a
277337runInit env prog = eff env prog (\r, env => pure r)
278338
279339||| Run an effectful program with a given default value for the environment.
@@ -282,31 +342,31 @@ runInit env prog = eff env prog (\r, env => pure r)
282342|||
283343||| @env The environment to use.
284344||| @prog The effectful program to run.
285−runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a
345+runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a
286346runPureInit env prog = eff env prog (\r, env => r)
287347
288−runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
348+runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
289349runWith inj env prog = eff env prog (\r, env => inj r)
290350
291−runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
351+runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
292352 m (x : a ** Env m (xs' x))
293353runEnv env prog = eff env prog (\r, env => pure (r ** env))
294354
295355-- ----------------------------------------------- [ some higher order things ]
296356
297−mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
357+mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)
298358mapE f [] = pure []
299359mapE f (x :: xs) = [| f x :: mapE f xs |]
300360
301361
302−mapVE : (a -> {xs} Eff b) ->
362+mapVE : (a -> {xs} EffM m b) ->
303363 Vect n a ->
304− {xs} Eff (Vect n b)
364+ {xs} EffM m (Vect n b)
305365mapVE f [] = pure []
306366mapVE f (x :: xs) = [| f x :: mapVE f xs |]
307367
308368
309−when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
369+when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()
310370when True e = Force e
311371when False e = pure ()
312372