@@ -2,20 +2,34 @@ module Effects
3import Language.Reflection
3import Language.Reflection
4import Control.Catchable
4import Control.Catchable
6%access public
7%access public
8---- Effects
9---- Effects
10Effect : Type
11Effect : Type
11−Effect = Type -> Type -> Type -> Type
12+Effect = (x : Type) -> Type -> (x -> Type) -> Type
13%error_reverse
14%error_reverse
14data EFFECT : Type where
15data EFFECT : Type where
15 MkEff : Type -> Effect -> EFFECT
16 MkEff : Type -> Effect -> EFFECT
17class Handler (e : Effect) (m : Type -> Type) where
18class 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
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
26+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
27+-- up to a small number of parameters...)
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)
20---- Properties and proof construction
34---- Properties and proof construction
@@ -29,11 +43,12 @@ using (xs : List a, ys : List a)
29 subListId {xs = Nil} = SubNil
43 subListId {xs = Nil} = SubNil
30 subListId {xs = x :: xs} = Keep subListId
44 subListId {xs = x :: xs} = Keep subListId
32−data Env : (m : Type -> Type) -> List EFFECT -> Type where
47+ data Env : (m : Type -> Type) -> List EFFECT -> Type where
33− Nil : Env m Nil
48+ Nil : Env m Nil
34− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
49+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
36−data EffElem : (Type -> Type -> Type -> Type) -> Type ->
51+data EffElem : Effect -> Type ->
37 List EFFECT -> Type where
52 List EFFECT -> Type where
38 Here : EffElem x a (MkEff a x :: xs)
53 Here : EffElem x a (MkEff a x :: xs)
39 There : EffElem x a xs -> EffElem x a (y :: xs)
54 There : EffElem x a xs -> EffElem x a (y :: xs)
@@ -79,7 +94,7 @@ reflectListEffElem _ = Refine "Here" `Seq` Solve
80%reflection
95%reflection
81reflectSubList : List a -> Tactic
96reflectSubList : List a -> Tactic
82−reflectSubList [] = Refine "SubNil" `Seq` Solve
97+reflectSubList [] = Refine "subListId" `Seq` Solve
83reflectSubList (x :: xs)
98reflectSubList (x :: xs)
84 = Try (Refine "subListId" `Seq` Solve)
99 = Try (Refine "subListId" `Seq` Solve)
85 (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
100 (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
@@ -87,22 +102,39 @@ reflectSubList (x :: xs)
87reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
102reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
88reflectSubList _ = Refine "subListId" `Seq` Solve
103reflectSubList _ = Refine "subListId" `Seq` Solve
106+reflectDefaultList : List a -> Tactic
107+reflectDefaultList [] = Refine "enil" `Seq` Solve
108+reflectDefaultList (x :: xs)
109+ = Refine "econs" `Seq`
112+ (Refine "default" `Seq`
115+ (reflectDefaultList xs))))))
116+reflectDefaultList (x ++ y) = Refine "Nil" `Seq` Solve
117+reflectDefaultList _ = Refine "Nil" `Seq` Solve
90%reflection
119%reflection
91reflectEff : (P : Type) -> Tactic
120reflectEff : (P : Type) -> Tactic
92reflectEff (EffElem m a xs)
121reflectEff (EffElem m a xs)
93 = reflectListEffElem xs `Seq` Solve
122 = reflectListEffElem xs `Seq` Solve
94reflectEff (SubList xs ys)
123reflectEff (SubList xs ys)
95 = reflectSubList ys `Seq` Solve
124 = reflectSubList ys `Seq` Solve
125+reflectEff (Env m xs)
126+ = reflectDefaultList xs `Seq` Solve
128+updateResTy : (val : t) ->
97−updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
129+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
98 List EFFECT
130 List EFFECT
99−updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
131+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
100−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
132+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
102−updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
134+-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
103− List EFFECT
135+-- List EFFECT
104−updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
136+-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
105−updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
137+-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
107infix 5 :::, :-, :=
139infix 5 :::, :-, :=
@@ -110,93 +142,67 @@ data LRes : lbl -> Type -> Type where
110 (:=) : (x : lbl) -> res -> LRes x res
142 (:=) : (x : lbl) -> res -> LRes x res
112(:::) : lbl -> EFFECT -> EFFECT
144(:::) : 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
148+ instance Default a => Default (LRes lbl a) where
149+ default = lbl := default
116unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
152unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
117unlabel {m} {x = MkEff a eff} [l := v] = [v]
153unlabel {m} {x = MkEff a eff} [l := v] = [v]
120−relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
156+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
157+relabel {xs = []} l [] = []
121−relabel {x = MkEff a eff} l [v] = [l := v]
158+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
123-- the language of Effects
160-- the language of Effects
125−data EffM : (m : Type -> Type) ->
162+data Eff : (m : Type -> Type) ->
126− List EFFECT -> List EFFECT -> Type -> Type where
164+ List EFFECT -> (x -> List EFFECT) -> Type where
127− value : a -> EffM m xs xs a
165+ value : a -> Eff m a xs (\v => xs)
166+ with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
128− ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
168+ ebind : Eff m a xs xs' ->
169+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
129− effect : (prf : EffElem e a xs) ->
170+ effect : (prf : EffElem e a xs) ->
130− (eff : e a b t) ->
171+ (eff : e t a b) ->
131− EffM m xs (updateResTy xs prf eff) t
172+ Eff m t xs (\v => updateResTy v xs prf eff)
132− lift : (prf : SubList ys xs) ->
174+ lift : (prf : SubList ys xs) ->
133− EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
175+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
134− new : Handler e m =>
176+ newInit : Handler e m =>
135− res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
178+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
136− EffM m xs xs' a
179+ Eff m a xs (\v => xs')
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 ->
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 ->
146− catch : Catchable m err =>
180+ catch : Catchable m err =>
147− EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
181+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->
148− EffM m xs xs' a
182+ Eff m a xs xs'
149− (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
183+
150−
184+ (:-) : (l : ty) ->
151−syntax [tag] ":!" [val] = !(tag :- val)
185+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
152−
186+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))
153−-- Eff : List (EFFECT m) -> Type -> Type
187+
154−
188+(>>=) : Eff m a xs xs' ->
155−-- For making proofs implicitly for 'test' and 'test_lbl'
189+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
157−syntax if_valid then [e] else [t] =
191+
158− test (tactics { byReflection reflectEff; }) t e
160−syntax if_valid [lbl] then [e] else [t] =
161− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
163−syntax if_error then [t] else [e] =
164− test (tactics { byReflection reflectEff; }) t e
166−syntax if_error [lbl] then [t] else [e] =
167− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
169−-- These may read better in some contexts
171−syntax if_right then [e] else [t] =
172− test (tactics { byReflection reflectEff; }) t e
174−syntax if_right [lbl] then [e] else [t] =
175− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
177−syntax if_left then [t] else [e] =
178− test (tactics { byReflection reflectEff; }) t e
180−syntax if_left [lbl] then [t] else [e] =
181− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
186−return : a -> EffM m xs xs a
192+return : a -> Eff m a xs (\v => xs)
187return x = value x
193return x = value x
189−(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
192-- for idiom brackets
195-- for idiom brackets
194infixl 2 <$>
197infixl 2 <$>
196−pure : a -> EffM m xs xs a
199+pure : a -> Eff m a xs (\v => xs)
197pure = value
200pure = value
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 ())
204+(<$>) : Eff m (a -> b) xs (\v => xs) ->
205+ Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
200(<$>) prog v = do fn <- prog
206(<$>) prog v = do fn <- prog
202 return (fn arg)
208 return (fn arg)
@@ -205,53 +211,28 @@ pure = value
207execEff : Env m xs -> (p : EffElem e res xs) ->
213execEff : Env m xs -> (p : EffElem e res xs) ->
208− (eff : e res b a) ->
214+ (eff : e a res resk) ->
209− (Env m (updateResTy xs p eff) -> a -> m t) -> m t
215+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
210execEff (val :: env) Here eff' k
216execEff (val :: env) Here eff' k
211− = handle val eff' (\res, v => k (res :: env) v)
217+ = handle val eff' (\v, res => k v (res :: env))
218+-- FIXME: Teach the elaborator to propagate parameters here
212−execEff {e} {res} {b} {a} (val :: env) (There p) eff k
219+execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
213− = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)
220+ = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
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) ->
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))
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) ->
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))
238-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
222-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
239-- updates can be propagated even through failing computations?
223-- updates can be propagated even through failing computations?
241−eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
225+eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
242−eff env (value x) k = k env x
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')
243eff env (prog `ebind` c) k
228eff 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)
245eff env (effect prf effP) k = execEff env prf effP k
230eff env (effect prf effP) k = execEff env prf effP k
246eff env (lift prf effP) k
231eff env (lift prf effP) k
247 = let env' = dropEnv env prf in
232 = let env' = dropEnv env prf in
248− eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
233+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
249−eff env (new r prog) k
234+eff env (newInit r prog) k
250− = eff (r :: env) prog (\(v :: envk), p' => k envk p')
235+ = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)
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)
255eff env (catch prog handler) k
236eff env (catch prog handler) k
256 = catch (eff env prog k)
237 = catch (eff env prog k)
257 (\e => eff env (handler e) k)
238 (\e => eff env (handler e) k)
@@ -261,48 +242,75 @@ eff env (catch prog handler) k
261-- end so that everything is in scope when it needs to be.
242-- end so that everything is in scope when it needs to be.
262eff {xs = [l ::: x]} env (l :- prog) k
243eff {xs = [l ::: x]} env (l :- prog) k
263 = let env' = unlabel env in
244 = 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))
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] |)
267−lift' : EffM m ys ys' t ->
259+lift' : Eff m t ys ys' ->
268 {default tactics { byReflection reflectEff; }
260 {default tactics { byReflection reflectEff; }
269 prf : SubList ys xs} ->
261 prf : SubList ys xs} ->
270− EffM m xs (updateWith ys' xs prf) t
262+ Eff m t xs (\v => updateWith (ys' v) xs prf)
271lift' e {prf} = lift prf e
263lift' e {prf} = lift prf e
274effect' : {a, b: _} -> {e : Effect} ->
266effect' : {a, b: _} -> {e : Effect} ->
275− (eff : e a b t) ->
267+ (eff : e t a b) ->
276 {default tactics { byReflection reflectEff; }
268 {default tactics { byReflection reflectEff; }
277 prf : EffElem e a xs} ->
269 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)
279effect' e {prf} = effect prf e
271effect' e {prf} = effect prf e
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
282−run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
279+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
283−run env prog = eff env prog (\env, r => pure r)
280+run {env} prog = eff env prog (\r, env => pure r)
285−runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
282+runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a
286−runEnv env prog = eff env prog (\env, r => pure (env, r))
283+runPure {env} prog = eff env prog (\r, env => r)
288−runPure : Env id xs -> EffM id xs xs' a -> a
285+runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a
289−runPure env prog = eff env prog (\env, r => r)
286+runInit env prog = eff env prog (\r, env => pure r)
291−-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
288+runPureInit : Env id xs -> Eff id a xs xs' -> a
292−-- runPureEnv env prog = eff env prog (\env, r => (env, r))
289+runPureInit env prog = eff env prog (\r, env => r)
294−runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
291+runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
295−runWith inj env prog = eff env prog (\env, r => inj r)
292+runWith inj env prog = eff env prog (\r, env => inj r)
297−Eff : (Type -> Type) -> List EFFECT -> Type -> Type
294+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
298−Eff m xs t = EffM m xs xs t
295+ m (x : a ** Env m (xs' x))
296+runEnv env prog = eff env prog (\r, env => pure (r ** env))
300-- some higher order things
298-- some higher order things
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)
303mapE f [] = pure []
301mapE f [] = pure []
304mapE f (x :: xs) = [| f x :: mapE f xs |]
302mapE f (x :: xs) = [| f x :: mapE f xs |]
305+mapVE : Applicative m =>
306+ (a -> {xs} Eff m b) ->
308+ {xs} Eff m (Vect n b)
310+mapVE f (x :: xs) = [| f x :: mapVE f xs |]
306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
313+when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
307when True e = e
314when True e = e
308when False e = pure ()
315when False e = pure ()