@@ -0,0 +1,292 @@
1+module Effects
2+
3+import Language.Reflection
4+import Control.Catchable
5+import Effect.Default
6+
7+--- Effectful computations are described as algebraic data types that
8+--- explain how an effect is interpreted in some underlying context.
9+
10+%access public
11+-- ----------------------------------------------------------------- [ Effects ]
12+||| The Effect type describes effectful computations.
13+|||
14+||| This type is parameterised by:
15+||| + The input resource.
16+||| + The return type of the computation.
17+||| + The computation to run on the resource.
18+Effect : Type
19+Effect = (x : Type) -> Type -> (x -> Type) -> Type
20+
21+||| The `EFFECT` Data type describes how to promote the Effect
22+||| description into a concrete effect.
23+%error_reverse
24+data EFFECT : Type where
25+ MkEff : Type -> Effect -> EFFECT
26+
27+||| Handler classes describe how an effect `e` is translated to the
28+||| underlying computation context `m` for execution.
29+class Handler (e : Effect) (m : Type -> Type) where
30+ ||| How to handle the effect.
31+ |||
32+ ||| @ r The resource being handled.
33+ ||| @ eff The effect to be applied.
34+ ||| @ k The continuation to pass the result of the effect
35+ covering handle : (r : res) -> (eff : e t res resk) ->
36+ (k : ((x : t) -> resk x -> m a)) -> m a
37+
38+||| Get the resource type (handy at the REPL to find out about an effect)
39+resourceType : EFFECT -> Type
40+resourceType (MkEff t e) = t
41+
42+-- --------------------------------------------------------- [ Syntactic Sugar ]
43+
44+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
45+-- up to a small number of parameters...)
46+
47+-- No state transition
48+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
49+
50+-- The state transition is dependent on a result `b`, a bound variable.
51+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
52+ = eff inst (\b => outst)
53+
54+--- A simple state transition
55+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
56+
57+-- --------------------------------------- [ Properties and Proof Construction ]
58+using (xs : List a, ys : List a)
59+ data SubList : List a -> List a -> Type where
60+ SubNil : SubList {a} [] []
61+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
62+ Drop : SubList xs ys -> SubList xs (x :: ys)
63+
64+ subListId : SubList xs xs
65+ subListId {xs = Nil} = SubNil
66+ subListId {xs = x :: xs} = Keep subListId
67+
68+namespace Env
69+ data Env : (m : Type -> Type) -> List EFFECT -> Type where
70+ Nil : Env m Nil
71+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
72+
73+data EffElem : Effect -> Type ->
74+ List EFFECT -> Type where
75+ Here : EffElem x a (MkEff a x :: xs)
76+ There : EffElem x a xs -> EffElem x a (y :: xs)
77+
78+||| make an environment corresponding to a sub-list
79+dropEnv : Env m ys -> SubList xs ys -> Env m xs
80+dropEnv [] SubNil = []
81+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
82+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
83+
84+updateWith : (ys' : List a) -> (xs : List a) ->
85+ SubList ys xs -> List a
86+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
87+updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
88+updateWith [] [] SubNil = []
89+updateWith (y :: ys) [] SubNil = y :: ys
90+updateWith [] (x :: xs) (Keep rest) = []
91+
92+||| Put things back, replacing old with new in the sub-environment
93+rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
94+ Env m xs -> Env m (updateWith ys' xs prf)
95+rebuildEnv [] SubNil env = env
96+rebuildEnv (x :: xs) SubNil env = x :: xs
97+rebuildEnv [] (Keep rest) (y :: env) = []
98+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
99+rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
100+
101+
102+-- -------------------------------------------------- [ The Effect EDSL itself ]
103+
104+updateResTy : (val : t) ->
105+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
106+ List EFFECT
107+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
108+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
109+
110+infix 5 :::, :-, :=
111+
112+data LRes : lbl -> Type -> Type where
113+ (:=) : (x : lbl) -> res -> LRes x res
114+
115+(:::) : lbl -> EFFECT -> EFFECT
116+(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
117+
118+using (lbl : Type)
119+ instance Default a => Default (LRes lbl a) where
120+ default = lbl := default
121+
122+private
123+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
124+unlabel {m} {x = MkEff a eff} [l := v] = [v]
125+
126+private
127+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
128+relabel {xs = []} l [] = []
129+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
130+
131+-- ------------------------------------------------- [ The Language of Effects ]
132+||| Definition of a language of effectful programs.
133+|||
134+||| @ x The return type of the result.
135+||| @ es The list of allowed side-effects.
136+||| @ ce Function to compute a new list of allowed side-effects.
137+data Eff : (x : Type)
138+ -> (es : List EFFECT)
139+ -> (ce : x -> List EFFECT) -> Type where
140+ value : a -> Eff a xs (\v => xs)
141+ with_val : (val : a) -> Eff () xs (\v => xs' val) ->
142+ Eff a xs xs'
143+ ebind : Eff a xs xs' ->
144+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
145+ callP : (prf : EffElem e a xs) ->
146+ (eff : e t a b) ->
147+ Eff t xs (\v => updateResTy v xs prf eff)
148+
149+ liftP : (prf : SubList ys xs) ->
150+ Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
151+
152+ (:-) : (l : ty) ->
153+ Eff t [x] xs' -> -- [x] (\v => xs) ->
154+ Eff t [l ::: x] (\v => map (l :::) (xs' v))
155+
156+(>>=) : Eff a xs xs' ->
157+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
158+(>>=) = ebind
159+
160+-- namespace SimpleBind
161+-- (>>=) : Eff m a xs (\v => xs) ->
162+-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
163+-- (>>=) = ebind
164+
165+||| Run a subprogram which results in an effect state the same as the input.
166+staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
167+staticEff = id
168+
169+||| Explicitly give the expected set of result effects for an effectful
170+||| operation.
171+toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
172+toEff xs' = id
173+
174+return : a -> Eff a xs (\v => xs)
175+return x = value x
176+
177+-- ------------------------------------------------------ [ for idiom brackets ]
178+
179+infixl 2 <$>
180+
181+pure : a -> Eff a xs (\v => xs)
182+pure = value
183+
184+syntax pureM [val] = with_val val (pure ())
185+
186+(<$>) : Eff (a -> b) xs (\v => xs) ->
187+ Eff a xs (\v => xs) -> Eff b xs (\v => xs)
188+(<$>) prog v = do fn <- prog
189+ arg <- v
190+ return (fn arg)
191+
192+-- ---------------------------------------------------------- [ an interpreter ]
193+
194+private
195+execEff : Env m xs -> (p : EffElem e res xs) ->
196+ (eff : e a res resk) ->
197+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
198+execEff (val :: env) Here eff' k
199+ = handle val eff' (\v, res => k v (res :: env))
200+-- FIXME: Teach the elaborator to propagate parameters here
201+execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
202+ = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
203+
204+-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
205+-- updates can be propagated even through failing computations?
206+
207+eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
208+eff env (value x) k = k x env
209+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
210+eff env (prog `ebind` c) k
211+ = eff env prog (\p', env' => eff env' (c p') k)
212+eff env (callP prf effP) k = execEff env prf effP k
213+eff env (liftP prf effP) k
214+ = let env' = dropEnv env prf in
215+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
216+-- FIXME:
217+-- xs is needed explicitly because otherwise the pattern binding for
218+-- 'l' appears too late. Solution seems to be to reorder patterns at the
219+-- end so that everything is in scope when it needs to be.
220+eff {xs = [l ::: x]} env (l :- prog) k
221+ = let env' = unlabel env in
222+ eff env' prog (\p', envk => k p' (relabel l envk))
223+
224+-- yuck :) Haven't got type class instances working nicely in tactic
225+-- proofs yet, and 'search' can't be told about any hints yet,
226+-- so just brute force it.
227+syntax MkDefaultEnv = with Env
228+ (| [], [default], [default, default],
229+ [default, default, default],
230+ [default, default, default, default],
231+ [default, default, default, default, default],
232+ [default, default, default, default, default, default],
233+ [default, default, default, default, default, default, default],
234+ [default, default, default, default, default, default, default, default] |)
235+
236+call : {a, b: _} -> {e : Effect} ->
237+ (eff : e t a b) ->
238+ {default tactics { search 100; }
239+ prf : EffElem e a xs} ->
240+ Eff t xs (\v => updateResTy v xs prf eff)
241+call e {prf} = callP prf e
242+
243+implicit
244+lift : Eff t ys ys' ->
245+ {default tactics { search 100; }
246+ prf : SubList ys xs} ->
247+ Eff t xs (\v => updateWith (ys' v) xs prf)
248+lift e {prf} = liftP prf e
249+
250+
251+-- --------------------------------------------------------- [ Running Effects ]
252+
253+||| Run an effectful program
254+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff a xs xs' -> m a
255+run {env} prog = eff env prog (\r, env => pure r)
256+
257+runPure : {default MkDefaultEnv env : Env id xs} -> Eff a xs xs' -> a
258+runPure {env} prog = eff env prog (\r, env => r)
259+
260+runInit : Applicative m => Env m xs -> Eff a xs xs' -> m a
261+runInit env prog = eff env prog (\r, env => pure r)
262+
263+runPureInit : Env id xs -> Eff a xs xs' -> a
264+runPureInit env prog = eff env prog (\r, env => r)
265+
266+runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
267+runWith inj env prog = eff env prog (\r, env => inj r)
268+
269+runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
270+ m (x : a ** Env m (xs' x))
271+runEnv env prog = eff env prog (\r, env => pure (r ** env))
272+
273+-- ----------------------------------------------- [ some higher order things ]
274+
275+mapE : Applicative m => (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
276+mapE f [] = pure []
277+mapE f (x :: xs) = [| f x :: mapE f xs |]
278+
279+
280+mapVE : Applicative m =>
281+ (a -> {xs} Eff b) ->
282+ Vect n a ->
283+ {xs} Eff (Vect n b)
284+mapVE f [] = pure []
285+mapVE f (x :: xs) = [| f x :: mapVE f xs |]
286+
287+
288+when : Applicative m => Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
289+when True e = Force e
290+when False e = pure ()
291+
292+-- --------------------------------------------------------------------- [ EOF ]