@@ -1,333 +0,0 @@
3−import Language.Reflection
4−import Control.Catchable
7−--- Effectful computations are described as algebraic data types that
8−--- explain how an effect is interpreted in some underlying context.
11−-- ----------------------------------------------------------------- [ Effects ]
12−||| The Effect type describes effectful computations.
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.
19−Effect = (x : Type) -> Type -> (x -> Type) -> Type
21−||| The `EFFECT` Data type describes how to promote the Effect
22−||| description into a concrete effect.
24−data EFFECT : Type where
25− MkEff : Type -> Effect -> EFFECT
27−||| Handler interfaces describe how an effect `e` is translated to the
28−||| underlying computation context `m` for execution.
29−interface Handler (e : Effect) (m : Type -> Type) where
30− ||| How to handle the effect.
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
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
42−-- --------------------------------------------------------- [ Syntactic Sugar ]
44−-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
45−-- up to a small number of parameters...)
47−-- No state transition
48−syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
50−-- The state transition is dependent on a result `b`, a bound variable.
51−syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
52− = eff inst (\b => outst)
54−--- A simple state transition
55−syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
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)
64− subListId : SubList xs xs
65− subListId {xs = Nil} = SubNil
66− subListId {xs = x :: xs} = Keep subListId
69− data Env : (m : Type -> Type) -> List EFFECT -> Type where
71− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
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)
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
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) = []
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
102−-- -------------------------------------------------- [ The Effect EDSL itself ]
104−updateResTy : (val : t) ->
105− (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
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
112−data LRes : lbl -> Type -> Type where
113− (:=) : (x : lbl) -> res -> LRes x res
115−(:::) : lbl -> EFFECT -> EFFECT
116−(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
119− implementation Default a => Default (LRes lbl a) where
120− default = lbl := default
123−unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
124−unlabel {m} {x = MkEff a eff} [l := v] = [v]
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
131−-- ------------------------------------------------- [ The Language of Effects ]
132−||| Definition of an Effect.
134−||| @ m The computation context
135−||| @ x The return type of the result.
136−||| @ es The list of allowed side-effects.
137−||| @ ce Function to compute a new list of allowed side-effects.
138−data Eff : (m : Type -> Type)
140− -> (es : List EFFECT)
141− -> (ce : x -> List EFFECT) -> Type where
142− value : a -> Eff m a xs (\v => xs)
143− with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
145− ebind : Eff m a xs xs' ->
146− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
147− callP : (prf : EffElem e a xs) ->
149− Eff m t xs (\v => updateResTy v xs prf eff)
151− liftP : (prf : SubList ys xs) ->
152− Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
153− newInit : Handler e m =>
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') ->
162− Eff m t [x] xs' -> -- [x] (\v => xs) ->
163− Eff m t [l ::: x] (\v => map (l :::) (xs' v))
165−(>>=) : Eff m a xs xs' ->
166− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
169−-- namespace SimpleBind
170−-- (>>=) : Eff m a xs (\v => xs) ->
171−-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
174−||| 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)
178−||| Explicitly give the expected set of result effects for an effectful
180−toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')
183−return : a -> Eff m a xs (\v => xs)
186−-- ------------------------------------------------------ [ for idiom brackets ]
190−pure : a -> Eff m a xs (\v => xs)
193−syntax pureM [val] = with_val val (pure ())
195−(<*>) : Eff m (a -> b) xs (\v => xs) ->
196− Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
197−(<*>) prog v = do fn <- prog
201−-- ---------------------------------------------------------- [ an interpreter ]
204−execEff : Env m xs -> (p : EffElem e res xs) ->
205− (eff : e a res resk) ->
206− ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
207−execEff (val :: env) Here eff' k
208− = handle val eff' (\v, res => k v (res :: env))
209−-- FIXME: Teach the elaborator to propagate parameters here
210−execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
211− = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
213−-- 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?
216−eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
217−eff env (value x) k = k x env
218−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
219−eff env (prog `ebind` c) k
220− = eff env prog (\p', env' => eff env' (c p') k)
221−eff env (callP prf effP) k = execEff env prf effP k
222−eff env (liftP prf effP) k
223− = let env' = dropEnv env prf in
224− 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
232−-- 'l' appears too late. Solution seems to be to reorder patterns at the
233−-- end so that everything is in scope when it needs to be.
234−eff {xs = [l ::: x]} env (l :- prog) k
235− = let env' = unlabel env in
236− eff env' prog (\p', envk => k p' (relabel l envk))
238−-- yuck :) Haven't got interface implementations working nicely in tactic
239−-- proofs yet, and 'search' can't be told about any hints yet,
240−-- so just brute force it.
241−syntax MkDefaultEnv = with Env
242− (| [], [default], [default, default],
243− [default, default, default],
244− [default, default, default, default],
245− [default, default, default, default, default],
246− [default, default, default, default, default, default],
247− [default, default, default, default, default, default, default],
248− [default, default, default, default, default, default, default, default] |)
250−call : {a, b: _} -> {e : Effect} ->
252− {auto prf : EffElem e a xs} ->
253− Eff m t xs (\v => updateResTy v xs prf eff)
254−call e {prf} = callP prf e
257−lift : Eff m t ys ys' ->
258− {auto prf : SubList ys xs} ->
259− Eff m t xs (\v => updateWith (ys' v) xs prf)
260−lift 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 ]
271−||| 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
278−run {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
287−runPure {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
296−runInit 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
305−runPureInit env prog = eff env prog (\r, env => r)
307−runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
308−runWith inj env prog = eff env prog (\r, env => inj r)
310−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
311− m (x : a ** Env m (xs' x))
312−runEnv env prog = eff env prog (\r, env => pure (r ** env))
314−-- ----------------------------------------------- [ some higher order things ]
316−mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
318−mapE f (x :: xs) = [| f x :: mapE f xs |]
321−mapVE : Applicative m =>
322− (a -> {xs} Eff m b) ->
324− {xs} Eff m (Vect n b)
326−mapVE f (x :: xs) = [| f x :: mapVE f xs |]
329−when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()
330−when True e = Force e
331−when False e = pure ()
333−-- --------------------------------------------------------------------- [ EOF ]