@@ -2,20 +2,34 @@ module Effects
22
33import Language.Reflection
44import Control.Catchable
5+import Effect.Default
56
67%access public
78
89---- Effects
910
1011Effect : Type
11−Effect = Type -> Type -> Type -> Type
12+Effect = (x : Type) -> Type -> (x -> Type) -> Type
1213
1314%error_reverse
1415data EFFECT : Type where
1516 MkEff : Type -> Effect -> EFFECT
1617
1718class Handler (e : Effect) (m : Type -> Type) where
18− handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a
19+ handle : res -> (eff : e t res resk) ->
20+ ((x : t) -> resk x -> m a) -> m a
21+
22+-- Get the resource type (handy at the REPL to find out about an effect)
23+resourceType : EFFECT -> Type
24+resourceType (MkEff t e) = t
25+
26+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
27+-- up to a small number of parameters...)
28+
29+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
30+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
31+ = eff inst (\b => outst)
32+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
1933
2034---- Properties and proof construction
2135
@@ -29,11 +43,12 @@ using (xs : List a, ys : List a)
2943 subListId {xs = Nil} = SubNil
3044 subListId {xs = x :: xs} = Keep subListId
3145
32−data Env : (m : Type -> Type) -> List EFFECT -> Type where
33− Nil : Env m Nil
34− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
35−
36−data EffElem : (Type -> Type -> Type -> Type) -> Type ->
46+namespace Env
47+ data Env : (m : Type -> Type) -> List EFFECT -> Type where
48+ Nil : Env m Nil
49+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
50+
51+data EffElem : Effect -> Type ->
3752 List EFFECT -> Type where
3853 Here : EffElem x a (MkEff a x :: xs)
3954 There : EffElem x a xs -> EffElem x a (y :: xs)
@@ -79,7 +94,7 @@ reflectListEffElem _ = Refine "Here" `Seq` Solve
7994
8095%reflection
8196reflectSubList : List a -> Tactic
82−reflectSubList [] = Refine "SubNil" `Seq` Solve
97+reflectSubList [] = Refine "subListId" `Seq` Solve
8398reflectSubList (x :: xs)
8499 = Try (Refine "subListId" `Seq` Solve)
85100 (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
@@ -87,22 +102,39 @@ reflectSubList (x :: xs)
87102reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
88103reflectSubList _ = Refine "subListId" `Seq` Solve
89104
105+%reflection
106+reflectDefaultList : List a -> Tactic
107+reflectDefaultList [] = Refine "enil" `Seq` Solve
108+reflectDefaultList (x :: xs)
109+ = Refine "econs" `Seq`
110+ (Solve `Seq`
111+ (Instance `Seq`
112+ (Refine "default" `Seq`
113+ (Solve `Seq`
114+ (Instance `Seq`
115+ (reflectDefaultList xs))))))
116+reflectDefaultList (x ++ y) = Refine "Nil" `Seq` Solve
117+reflectDefaultList _ = Refine "Nil" `Seq` Solve
118+
90119%reflection
91120reflectEff : (P : Type) -> Tactic
92121reflectEff (EffElem m a xs)
93122 = reflectListEffElem xs `Seq` Solve
94123reflectEff (SubList xs ys)
95124 = reflectSubList ys `Seq` Solve
125+reflectEff (Env m xs)
126+ = reflectDefaultList xs `Seq` Solve
96127
97−updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
128+updateResTy : (val : t) ->
129+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
98130 List EFFECT
99−updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
100−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
131+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
132+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
101133
102−updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
103− List EFFECT
104−updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
105−updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
134+-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
135+-- List EFFECT
136+-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
137+-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
106138
107139infix 5 :::, :-, :=
108140
@@ -110,93 +142,67 @@ data LRes : lbl -> Type -> Type where
110142 (:=) : (x : lbl) -> res -> LRes x res
111143
112144(:::) : lbl -> EFFECT -> EFFECT
113−(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
145+(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
146+
147+using (lbl : Type)
148+ instance Default a => Default (LRes lbl a) where
149+ default = lbl := default
114150
115151private
116152unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
117153unlabel {m} {x = MkEff a eff} [l := v] = [v]
118154
119155private
120−relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
121−relabel {x = MkEff a eff} l [v] = [l := v]
156+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
157+relabel {xs = []} l [] = []
158+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
122159
123160-- the language of Effects
124161
125−data EffM : (m : Type -> Type) ->
126− List EFFECT -> List EFFECT -> Type -> Type where
127− value : a -> EffM m xs xs a
128− ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
129− effect : (prf : EffElem e a xs) ->
130− (eff : e a b t) ->
131− EffM m xs (updateResTy xs prf eff) t
132− lift : (prf : SubList ys xs) ->
133− EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
134− new : Handler e m =>
135− res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
136− EffM m xs xs' a
137− test : (prf : EffElem e (Either l r) xs) ->
138− EffM m (updateResTyImm xs prf l) xs' t ->
139− EffM m (updateResTyImm xs prf r) xs' t ->
140− EffM m xs xs' t
141− test_lbl : {x : lbl} ->
142− (prf : EffElem e (LRes x (Either l r)) xs) ->
143− EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
144− EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
145− EffM m xs xs' t
146− catch : Catchable m err =>
147− EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
148− EffM m xs xs' a
149− (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
150−
151−syntax [tag] ":!" [val] = !(tag :- val)
152−
153−-- Eff : List (EFFECT m) -> Type -> Type
154−
155−-- For making proofs implicitly for 'test' and 'test_lbl'
156−
157−syntax if_valid then [e] else [t] =
158− test (tactics { byReflection reflectEff; }) t e
159−
160−syntax if_valid [lbl] then [e] else [t] =
161− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
162−
163−syntax if_error then [t] else [e] =
164− test (tactics { byReflection reflectEff; }) t e
165−
166−syntax if_error [lbl] then [t] else [e] =
167− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
168−
169−-- These may read better in some contexts
170−
171−syntax if_right then [e] else [t] =
172− test (tactics { byReflection reflectEff; }) t e
173−
174−syntax if_right [lbl] then [e] else [t] =
175− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
176−
177−syntax if_left then [t] else [e] =
178− test (tactics { byReflection reflectEff; }) t e
179−
180−syntax if_left [lbl] then [t] else [e] =
181− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
182−
183−
184−-- for 'do' notation
185−
186−return : a -> EffM m xs xs a
162+data Eff : (m : Type -> Type) ->
163+ (x : Type) ->
164+ List EFFECT -> (x -> List EFFECT) -> Type where
165+ value : a -> Eff m a xs (\v => xs)
166+ with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
167+ Eff m a xs xs'
168+ ebind : Eff m a xs xs' ->
169+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
170+ effect : (prf : EffElem e a xs) ->
171+ (eff : e t a b) ->
172+ Eff m t xs (\v => updateResTy v xs prf eff)
173+
174+ lift : (prf : SubList ys xs) ->
175+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
176+ newInit : Handler e m =>
177+ res ->
178+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
179+ Eff m a xs (\v => xs')
180+ catch : Catchable m err =>
181+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->
182+ Eff m a xs xs'
183+
184+ (:-) : (l : ty) ->
185+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
186+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))
187+
188+(>>=) : Eff m a xs xs' ->
189+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
190+(>>=) = ebind
191+
192+return : a -> Eff m a xs (\v => xs)
187193return x = value x
188194
189−(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
190−(>>=) = ebind
191−
192195-- for idiom brackets
193196
194197infixl 2 <$>
195198
196−pure : a -> EffM m xs xs a
199+pure : a -> Eff m a xs (\v => xs)
197200pure = value
198201
199−(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b
202+syntax pureM [val] = with_val val (pure ())
203+
204+(<$>) : Eff m (a -> b) xs (\v => xs) ->
205+ Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
200206(<$>) prog v = do fn <- prog
201207 arg <- v
202208 return (fn arg)
@@ -205,53 +211,28 @@ pure = value
205211
206212private
207213execEff : Env m xs -> (p : EffElem e res xs) ->
208− (eff : e res b a) ->
209− (Env m (updateResTy xs p eff) -> a -> m t) -> m t
214+ (eff : e a res resk) ->
215+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
210216execEff (val :: env) Here eff' k
211− = handle val eff' (\res, v => k (res :: env) v)
212−execEff {e} {res} {b} {a} (val :: env) (There p) eff k
213− = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)
214−
215−private
216−testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->
217− (Env m (updateResTyImm xs p l) -> m b) ->
218− (Env m (updateResTyImm xs p r) -> m b) ->
219− m b
220−testEff (Left err :: env) Here lk rk = lk (err :: env)
221−testEff (Right ok :: env) Here lk rk = rk (ok :: env)
222−testEff (val :: env) (There p) lk rk
223− = testEff env p (\envk => lk (val :: envk))
224− (\envk => rk (val :: envk))
225−
226−private
227−testEffLbl : {x : lblTy} ->
228− Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->
229− (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->
230− (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->
231− m b
232−testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)
233−testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)
234−testEffLbl (val :: env) (There p) lk rk
235− = testEffLbl env p (\envk => lk (val :: envk))
236− (\envk => rk (val :: envk))
217+ = handle val eff' (\v, res => k v (res :: env))
218+-- FIXME: Teach the elaborator to propagate parameters here
219+execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
220+ = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
237221
238222-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
239223-- updates can be propagated even through failing computations?
240224
241−eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
242−eff env (value x) k = k env x
225+eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
226+eff env (value x) k = k x env
227+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
243228eff env (prog `ebind` c) k
244− = eff env prog (\env', p' => eff env' (c p') k)
229+ = eff env prog (\p', env' => eff env' (c p') k)
245230eff env (effect prf effP) k = execEff env prf effP k
246231eff env (lift prf effP) k
247232 = let env' = dropEnv env prf in
248− eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
249−eff env (new r prog) k
250− = eff (r :: env) prog (\(v :: envk), p' => k envk p')
251−eff env (test prf l r) k
252− = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)
253−eff env (test_lbl prf l r) k
254− = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)
233+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
234+eff env (newInit r prog) k
235+ = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)
255236eff env (catch prog handler) k
256237 = catch (eff env prog k)
257238 (\e => eff env (handler e) k)
@@ -261,48 +242,75 @@ eff env (catch prog handler) k
261242-- end so that everything is in scope when it needs to be.
262243eff {xs = [l ::: x]} env (l :- prog) k
263244 = let env' = unlabel env in
264− eff env' prog (\envk, p' => k (relabel l envk) p')
245+ eff env' prog (\p', envk => k p' (relabel l envk))
246+
247+-- yuck :) Haven't got type class instances working nicely in tactic
248+-- proofs yet, so just brute force it.
249+syntax MkDefaultEnv = with Env
250+ (| [], [default], [default, default],
251+ [default, default, default],
252+ [default, default, default, default],
253+ [default, default, default, default, default],
254+ [default, default, default, default, default, default],
255+ [default, default, default, default, default, default, default],
256+ [default, default, default, default, default, default, default, default] |)
265257
266258implicit
267−lift' : EffM m ys ys' t ->
259+lift' : Eff m t ys ys' ->
268260 {default tactics { byReflection reflectEff; }
269261 prf : SubList ys xs} ->
270− EffM m xs (updateWith ys' xs prf) t
262+ Eff m t xs (\v => updateWith (ys' v) xs prf)
271263lift' e {prf} = lift prf e
272264
273265implicit
274266effect' : {a, b: _} -> {e : Effect} ->
275− (eff : e a b t) ->
267+ (eff : e t a b) ->
276268 {default tactics { byReflection reflectEff; }
277269 prf : EffElem e a xs} ->
278− EffM m xs (updateResTy xs prf eff) t
270+ Eff m t xs (\v => updateResTy v xs prf eff)
279271effect' e {prf} = effect prf e
280272
273+new : Handler e m =>
274+ {default default r : res} ->
275+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
276+ Eff m a xs (\v => xs')
277+new {r} e = newInit r e
281278
282−run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
283−run env prog = eff env prog (\env, r => pure r)
279+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
280+run {env} prog = eff env prog (\r, env => pure r)
284281
285−runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
286−runEnv env prog = eff env prog (\env, r => pure (env, r))
282+runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a
283+runPure {env} prog = eff env prog (\r, env => r)
287284
288−runPure : Env id xs -> EffM id xs xs' a -> a
289−runPure env prog = eff env prog (\env, r => r)
285+runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a
286+runInit env prog = eff env prog (\r, env => pure r)
290287
291−-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
292−-- runPureEnv env prog = eff env prog (\env, r => (env, r))
288+runPureInit : Env id xs -> Eff id a xs xs' -> a
289+runPureInit env prog = eff env prog (\r, env => r)
293290
294−runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
295−runWith inj env prog = eff env prog (\env, r => inj r)
291+runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
292+runWith inj env prog = eff env prog (\r, env => inj r)
296293
297−Eff : (Type -> Type) -> List EFFECT -> Type -> Type
298−Eff m xs t = EffM m xs xs t
294+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
295+ m (x : a ** Env m (xs' x))
296+runEnv env prog = eff env prog (\r, env => pure (r ** env))
299297
300298-- some higher order things
301299
302−mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
300+mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
303301mapE f [] = pure []
304302mapE f (x :: xs) = [| f x :: mapE f xs |]
305303
306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
304+
305+mapVE : Applicative m =>
306+ (a -> {xs} Eff m b) ->
307+ Vect n a ->
308+ {xs} Eff m (Vect n b)
309+mapVE f [] = pure []
310+mapVE f (x :: xs) = [| f x :: mapVE f xs |]
311+
312+
313+when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
307314when True e = e
308315when False e = pure ()
316+