@@ -10,7 +10,7 @@ import Effect.Default
10%access public
10%access public
11-- ----------------------------------------------------------------- [ Effects ]
11-- ----------------------------------------------------------------- [ Effects ]
12||| The Effect type describes effectful computations.
12||| The Effect type describes effectful computations.
14||| This type is parameterised by:
14||| This type is parameterised by:
15||| + The input resource.
15||| + The input resource.
16||| + The return type of the computation.
16||| + The return type of the computation.
@@ -28,11 +28,11 @@ data EFFECT : Type where
28||| underlying computation context `m` for execution.
28||| underlying computation context `m` for execution.
29class Handler (e : Effect) (m : Type -> Type) where
29class Handler (e : Effect) (m : Type -> Type) where
30 ||| How to handle the effect.
30 ||| How to handle the effect.
32 ||| @ r The resource being handled.
32 ||| @ r The resource being handled.
33 ||| @ eff The effect to be applied.
33 ||| @ eff The effect to be applied.
34 ||| @ k The continuation to pass the result of the effect
34 ||| @ 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) ->
36 (k : ((x : t) -> resk x -> m a)) -> m a
36 (k : ((x : t) -> resk x -> m a)) -> m a
38||| Get the resource type (handy at the REPL to find out about an effect)
38||| Get the resource type (handy at the REPL to find out about an effect)
@@ -48,28 +48,27 @@ resourceType (MkEff t e) = t
48syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
48syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
50-- The state transition is dependent on a result `b`, a bound variable.
50-- The state transition is dependent on a result `b`, a bound variable.
51−syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
51+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
52 = eff inst (\b => outst)
52 = eff inst (\b => outst)
54--- A simple state transition
54--- A simple state transition
55syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
55syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
57-- --------------------------------------- [ Properties and Proof Construction ]
57-- --------------------------------------- [ Properties and Proof Construction ]
58−using (xs : List a, ys : List a)
59− data SubList : List a -> List a -> Type where
58+data SubList : List a -> List a -> Type where
60− SubNil : SubList {a} [] []
59+ SubNil : SubList [] []
61− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
60+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
62− Drop : SubList xs ys -> SubList xs (x :: ys)
61+ Drop : SubList xs ys -> SubList xs (x :: ys)
64− subListId : SubList xs xs
63+subListId : SubList xs xs
65− subListId {xs = Nil} = SubNil
64+subListId {xs = Nil} = SubNil
66− subListId {xs = x :: xs} = Keep subListId
65+subListId {xs = x :: xs} = Keep subListId
68namespace Env
67namespace Env
69 data Env : (m : Type -> Type) -> List EFFECT -> Type where
68 data Env : (m : Type -> Type) -> List EFFECT -> Type where
70 Nil : Env m Nil
69 Nil : Env m Nil
71 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
70 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
73data EffElem : Effect -> Type ->
72data EffElem : Effect -> Type ->
74 List EFFECT -> Type where
73 List EFFECT -> Type where
75 Here : EffElem x a (MkEff a x :: xs)
74 Here : EffElem x a (MkEff a x :: xs)
@@ -129,71 +128,62 @@ relabel {xs = []} l [] = []
129relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
128relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
131-- ------------------------------------------------- [ The Language of Effects ]
130-- ------------------------------------------------- [ The Language of Effects ]
132−||| Definition of an Effect.
131+||| Definition of a language of effectful programs.
134−||| @ m The computation context
135||| @ x The return type of the result.
133||| @ x The return type of the result.
136||| @ es The list of allowed side-effects.
134||| @ es The list of allowed side-effects.
137||| @ ce Function to compute a new list of allowed side-effects.
135||| @ 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)
140 -> (es : List EFFECT)
137 -> (es : List EFFECT)
141 -> (ce : x -> List EFFECT) -> Type where
138 -> (ce : x -> List EFFECT) -> Type where
142− value : a -> Eff m a xs (\v => xs)
139+ value : a -> Eff a xs (\v => xs)
143− with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
140+ with_val : (val : a) -> Eff () xs (\v => xs' val) ->
144− Eff m a xs xs'
141+ Eff a xs xs'
145− ebind : Eff m a xs xs' ->
142+ ebind : Eff a xs xs' ->
146− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
143+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
147 callP : (prf : EffElem e a xs) ->
144 callP : (prf : EffElem e a xs) ->
148 (eff : e t a b) ->
145 (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)
151 liftP : (prf : SubList ys xs) ->
148 liftP : (prf : SubList ys xs) ->
152− Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
149+ Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
153− newInit : Handler e m =>
150+
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') ->
161− (:-) : (l : ty) ->
151+ (:-) : (l : ty) ->
162− Eff m t [x] xs' -> -- [x] (\v => xs) ->
152+ Eff t [x] xs' -> -- [x] (\v => xs) ->
163− Eff m t [l ::: x] (\v => map (l :::) (xs' v))
153+ Eff t [l ::: x] (\v => map (l :::) (xs' v))
165−(>>=) : Eff m a xs xs' ->
155+(>>=) : Eff a xs xs' ->
166− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
156+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
167−(>>=) = ebind
157+(>>=) = ebind
169-- namespace SimpleBind
159-- namespace SimpleBind
170−-- (>>=) : Eff m a xs (\v => xs) ->
160+-- (>>=) : Eff m a xs (\v => xs) ->
171-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
161-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
172−-- (>>=) = ebind
162+-- (>>=) = ebind
174||| Run a subprogram which results in an effect state the same as the input.
164||| 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)
176staticEff = id
166staticEff = id
178||| Explicitly give the expected set of result effects for an effectful
168||| Explicitly give the expected set of result effects for an effectful
179||| operation.
169||| 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')
181toEff xs' = id
171toEff xs' = id
183−return : a -> Eff m a xs (\v => xs)
173+return : a -> Eff a xs (\v => xs)
184return x = value x
174return x = value x
186-- ------------------------------------------------------ [ for idiom brackets ]
176-- ------------------------------------------------------ [ for idiom brackets ]
188infixl 2 <$>
178infixl 2 <$>
190−pure : a -> Eff m a xs (\v => xs)
180+pure : a -> Eff a xs (\v => xs)
191pure = value
181pure = value
193syntax pureM [val] = with_val val (pure ())
183syntax pureM [val] = with_val val (pure ())
195−(<$>) : Eff m (a -> b) xs (\v => xs) ->
185+(<$>) : Eff (a -> b) xs (\v => xs) ->
196− Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
186+ Eff a xs (\v => xs) -> Eff b xs (\v => xs)
197(<$>) prog v = do fn <- prog
187(<$>) prog v = do fn <- prog
199 return (fn arg)
189 return (fn arg)
@@ -213,20 +203,15 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
213-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
203-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
214-- updates can be propagated even through failing computations?
204-- updates can be propagated even through failing computations?
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
217eff env (value x) k = k x env
207eff 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')
219eff env (prog `ebind` c) k
209eff env (prog `ebind` c) k
220 = eff env prog (\p', env' => eff env' (c p') k)
210 = eff env prog (\p', env' => eff env' (c p') k)
221eff env (callP prf effP) k = execEff env prf effP k
211eff env (callP prf effP) k = execEff env prf effP k
222eff env (liftP prf effP) k
212eff env (liftP prf effP) k
223 = let env' = dropEnv env prf in
213 = let env' = dropEnv env prf in
224 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
214 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)
231-- xs is needed explicitly because otherwise the pattern binding for
216-- xs is needed explicitly because otherwise the pattern binding for
232-- 'l' appears too late. Solution seems to be to reorder patterns at the
217-- 'l' appears too late. Solution seems to be to reorder patterns at the
@@ -249,84 +234,56 @@ syntax MkDefaultEnv = with Env
250call : {a, b: _} -> {e : Effect} ->
235call : {a, b: _} -> {e : Effect} ->
251 (eff : e t a b) ->
236 (eff : e t a b) ->
237+ {default tactics { search 100; }
252− {auto prf : EffElem e a xs} ->
238+ prf : EffElem e a xs} ->
253− Eff m t xs (\v => updateResTy v xs prf eff)
239+ Eff t xs (\v => updateResTy v xs prf eff)
254call e {prf} = callP prf e
240call e {prf} = callP prf e
257−lift : Eff m t ys ys' ->
243+lift : Eff t ys ys' ->
244+ {default tactics { search 100; }
258− {auto prf : SubList ys xs} ->
245+ prf : SubList ys xs} ->
259− Eff m t xs (\v => updateWith (ys' v) xs prf)
246+ Eff t xs (\v => updateWith (ys' v) xs prf)
260lift e {prf} = liftP prf e
247lift e {prf} = liftP prf e
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
269-- --------------------------------------------------------- [ Running Effects ]
250-- --------------------------------------------------------- [ Running Effects ]
271−||| Run an effectful program.
252+||| Run an effectful program
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.
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
253+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff a xs xs' -> m a
278run {env} prog = eff env prog (\r, env => pure r)
254run {env} prog = eff env prog (\r, env => pure r)
280−||| Run an effectful program in the identity context `id`.
282−||| A helper function useful for when the given context is 'pure'.
283−||| The `env` argument is implicit and initialised automatically.
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
287runPure {env} prog = eff env prog (\r, env => r)
257runPure {env} prog = eff env prog (\r, env => r)
289−||| Run an effectful program with a default value for the environment context.
291−||| This is useful for when no default value exists for a given resource type.
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
296runInit env prog = eff env prog (\r, env => pure r)
260runInit env prog = eff env prog (\r, env => pure r)
298−||| Run an effectful program in the identity context `id` with a given default value for the environment context.
300−||| A helper function useful for when the given context is 'pure'.
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
305runPureInit env prog = eff env prog (\r, env => r)
263runPureInit env prog = eff env prog (\r, env => r)
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
308runWith inj env prog = eff env prog (\r, env => inj r)
266runWith inj env prog = eff env prog (\r, env => inj r)
310−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
268+runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
311 m (x : a ** Env m (xs' x))
269 m (x : a ** Env m (xs' x))
312runEnv env prog = eff env prog (\r, env => pure (r ** env))
270runEnv env prog = eff env prog (\r, env => pure (r ** env))
314-- ----------------------------------------------- [ some higher order things ]
272-- ----------------------------------------------- [ some higher order things ]
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)
317mapE f [] = pure []
275mapE f [] = pure []
318mapE f (x :: xs) = [| f x :: mapE f xs |]
276mapE f (x :: xs) = [| f x :: mapE f xs |]
321−mapVE : Applicative m =>
322− (a -> {xs} Eff m b) ->
279+mapVE : (a -> {xs} Eff b) ->
323− Vect n a ->
280+ Vect n a ->
324− {xs} Eff m (Vect n b)
281+ {xs} Eff (Vect n b)
325mapVE f [] = pure []
282mapVE f [] = pure []
326mapVE f (x :: xs) = [| f x :: mapVE f xs |]
283mapVE f (x :: xs) = [| f x :: mapVE f xs |]
329−when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()
286+when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
330when True e = Force e
287when True e = Force e
331when False e = pure ()
288when False e = pure ()