@@ -0,0 +1,271 @@
1+module Effects
2+
3+import Language.Reflection
4+import Control.Catchable
5+import Effect.Default
6+
7+%access public
8+
9+---- Effects
10+
11+Effect : Type
12+Effect = (x : Type) -> Type -> (x -> Type) -> Type
13+
14+data EFFECT : Type where
15+ MkEff : Type -> Effect -> EFFECT
16+
17+class Handler (e : Effect) (m : Type -> Type) where
18+ handle : res -> (eff : e t res resk) ->
19+ ((x : t) -> resk x -> m a) -> m a
20+
21+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
22+-- up to a small number of parameters...)
23+
24+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
25+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
26+
27+---- Properties and proof construction
28+
29+using (xs : List a, ys : List a)
30+ data SubList : List a -> List a -> Type where
31+ SubNil : SubList {a} [] []
32+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
33+ Drop : SubList xs ys -> SubList xs (x :: ys)
34+
35+ subListId : SubList xs xs
36+ subListId {xs = Nil} = SubNil
37+ subListId {xs = x :: xs} = Keep subListId
38+
39+namespace Env
40+ data Env : (m : Type -> Type) -> List EFFECT -> Type where
41+ Nil : Env m Nil
42+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
43+
44+data EffElem : Effect -> Type ->
45+ List EFFECT -> Type where
46+ Here : EffElem x a (MkEff a x :: xs)
47+ There : EffElem x a xs -> EffElem x a (y :: xs)
48+
49+-- make an environment corresponding to a sub-list
50+dropEnv : Env m ys -> SubList xs ys -> Env m xs
51+dropEnv [] SubNil = []
52+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
53+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
54+
55+updateWith : (ys' : List a) -> (xs : List a) ->
56+ SubList ys xs -> List a
57+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
58+updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
59+updateWith [] [] SubNil = []
60+updateWith (y :: ys) [] SubNil = y :: ys
61+updateWith [] (x :: xs) (Keep rest) = []
62+
63+-- put things back, replacing old with new in the sub-environment
64+rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
65+ Env m xs -> Env m (updateWith ys' xs prf)
66+rebuildEnv [] SubNil env = env
67+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
68+rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
69+rebuildEnv (x :: xs) SubNil [] = x :: xs
70+
71+---- The Effect EDSL itself ----
72+
73+-- some proof automation
74+
75+%reflection
76+reflectListEffElem : List a -> Tactic
77+reflectListEffElem [] = Refine "Here" `Seq` Solve
78+reflectListEffElem (x :: xs)
79+ = Try (Refine "Here" `Seq` Solve)
80+ (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))
81+-- TMP HACK! FIXME!
82+-- The evaluator needs a 'function case' to know its a reflection function
83+-- until we propagate that information! Without this, the _ case won't get
84+-- matched.
85+reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve
86+reflectListEffElem _ = Refine "Here" `Seq` Solve
87+
88+%reflection
89+reflectSubList : List a -> Tactic
90+reflectSubList [] = Refine "subListId" `Seq` Solve
91+reflectSubList (x :: xs)
92+ = Try (Refine "subListId" `Seq` Solve)
93+ (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
94+ (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))
95+reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
96+reflectSubList _ = Refine "subListId" `Seq` Solve
97+
98+%reflection
99+reflectEff : (P : Type) -> Tactic
100+reflectEff (EffElem m a xs)
101+ = reflectListEffElem xs `Seq` Solve
102+reflectEff (SubList xs ys)
103+ = reflectSubList ys `Seq` Solve
104+
105+updateResTy : (val : t) ->
106+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
107+ List EFFECT
108+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
109+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
110+
111+-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
112+-- List EFFECT
113+-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
114+-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
115+
116+infix 5 :::, :-, :=
117+
118+data LRes : lbl -> Type -> Type where
119+ (:=) : (x : lbl) -> res -> LRes x res
120+
121+(:::) : lbl -> EFFECT -> EFFECT
122+(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
123+
124+using (lbl : Type)
125+ instance Default a => Default (LRes lbl a) where
126+ default = lbl := default
127+
128+private
129+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
130+unlabel {m} {x = MkEff a eff} [l := v] = [v]
131+
132+private
133+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
134+relabel {xs = []} l [] = []
135+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
136+
137+-- the language of Effects
138+
139+data Eff : (m : Type -> Type) ->
140+ (x : Type) ->
141+ List EFFECT -> (x -> List EFFECT) -> Type where
142+ value : a -> Eff m a xs (\v => xs)
143+ ebind : Eff m a xs xs' ->
144+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
145+ effect : (prf : EffElem e a xs) ->
146+ (eff : e t a b) ->
147+ Eff m t xs (\v => updateResTy v xs prf eff)
148+
149+ lift : (prf : SubList ys xs) ->
150+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
151+ new : Handler e m =>
152+ res ->
153+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
154+ Eff m a xs (\v => xs')
155+ catch : Catchable m err =>
156+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->
157+ Eff m a xs xs'
158+
159+ (:-) : (l : ty) ->
160+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
161+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))
162+
163+(>>=) : Eff m a xs xs' ->
164+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
165+(>>=) = ebind
166+
167+implicit
168+lift' : Eff m t ys ys' ->
169+ {default tactics { byReflection reflectEff; }
170+ prf : SubList ys xs} ->
171+ Eff m t xs (\v => updateWith (ys' v) xs prf)
172+lift' e {prf} = lift prf e
173+
174+implicit
175+effect' : {a, b: _} -> {e : Effect} ->
176+ (eff : e t a b) ->
177+ {default tactics { byReflection reflectEff; }
178+ prf : EffElem e a xs} ->
179+ Eff m t xs (\v => updateResTy v xs prf eff)
180+effect' e {prf} = effect prf e
181+
182+return : a -> Eff m a xs (\v => xs)
183+return x = value x
184+
185+-- for idiom brackets
186+
187+infixl 2 <$>
188+
189+pure : a -> Eff m a xs (\v => xs)
190+pure = value
191+
192+(<$>) : Eff m (a -> b) xs (\v => xs) ->
193+ Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
194+(<$>) prog v = do fn <- prog
195+ arg <- v
196+ return (fn arg)
197+
198+-- an interpreter
199+
200+private
201+execEff : Env m xs -> (p : EffElem e res xs) ->
202+ (eff : e a res resk) ->
203+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
204+execEff (val :: env) Here eff' k
205+ = handle val eff' (\v, res => k v (res :: env))
206+execEff (val :: env) (There p) eff k
207+ = execEff env p eff (\v, env' => k v (val :: env'))
208+
209+-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
210+-- updates can be propagated even through failing computations?
211+
212+eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
213+eff env (value x) k = k x env
214+eff env (prog `ebind` c) k
215+ = eff env prog (\p', env' => eff env' (c p') k)
216+eff env (effect prf effP) k = execEff env prf effP k
217+eff env (lift prf effP) k
218+ = let env' = dropEnv env prf in
219+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
220+eff env (new r prog) k
221+ = let env' = r :: env in
222+ eff env' prog (\p' => \ (v :: envk) => k p' envk)
223+eff env (catch prog handler) k
224+ = catch (eff env prog k)
225+ (\e => eff env (handler e) k)
226+-- FIXME:
227+-- xs is needed explicitly because otherwise the pattern binding for
228+-- 'l' appears too late. Solution seems to be to reorder patterns at the
229+-- end so that everything is in scope when it needs to be.
230+eff {xs = [l ::: x]} env (l :- prog) k
231+ = let env' = unlabel env in
232+ eff env' prog (\p', envk => k p' (relabel l envk))
233+
234+run : Applicative m => Env m xs -> Eff m a xs xs' -> m a
235+run env prog = eff env prog (\r, env => pure r)
236+
237+-- yuck :)
238+syntax MkDefaultEnv = (| [], [default], [default, default],
239+ [default, default, default],
240+ [default, default, default, default],
241+ [default, default, default, default, default],
242+ [default, default, default, default, default, default],
243+ [default, default, default, default, default, default, default],
244+ [default, default, default, default, default, default, default, default] |)
245+
246+run' : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
247+run' {env} prog = eff env prog (\r, env => pure r)
248+
249+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
250+ m (x : a ** Env m (xs' x))
251+runEnv env prog = eff env prog (\r, env => pure (r ** env))
252+
253+runPure : Env id xs -> Eff id a xs xs' -> a
254+runPure env prog = eff env prog (\r, env => r)
255+
256+-- runPureEnv : Env id xs -> Eff id a xs xs' -> (x : a ** Env id (xs' x))
257+-- runPureEnv env prog = eff env prog (%unifyLog (\r, env => id (r ** env)))
258+
259+runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
260+runWith inj env prog = eff env prog (\r, env => inj r)
261+
262+-- some higher order things
263+
264+mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
265+mapE f [] = pure []
266+mapE f (x :: xs) = [| f x :: mapE f xs |]
267+
268+when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
269+when True e = e
270+when False e = pure ()
271+