git.iko.soy/Idris-dev
on fbb201c help sign in
Idris-dev/libs/effects/Effects.idr
380 lines 14 kB history raw
1module Effects
3import Language.Reflection
4import public Effect.Default
5import Data.Vect
7--- Effectful computations are described as algebraic data types that
8--- explain how an effect is interpreted in some underlying context.
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.
18Effect : Type
19Effect = (x : Type) -> Type -> (x -> Type) -> Type
21||| The `EFFECT` Data type describes how to promote the Effect
22||| description into a concrete effect.
23%error_reverse
24data EFFECT : Type where
25 MkEff : Type -> Effect -> EFFECT
27-- 'sig' gives the signature for an effect. There are four versions
28-- depending on whether there is no resource needed,
29-- no state change, a non-dependent change,
30-- or a dependent change. These are easily disambiguated by type.
32namespace NoResourceEffect
33 sig : Effect -> Type -> Type
34 sig e r = e r () (\v => ())
36namespace NoUpdateEffect
37 sig : Effect -> (ret : Type) -> (resource : Type) -> Type
38 sig e r e_in = e r e_in (\v => e_in)
40namespace UpdateEffect
41 sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type
42 sig e r e_in e_out = e r e_in (\v => e_out)
44namespace DepUpdateEffect
45 sig : Effect ->
46 (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
47 sig e r e_in e_out = e r e_in e_out
49||| Handler classes describe how an effect `e` is translated to the
50||| underlying computation context `m` for execution.
51class Handler (e : Effect) (m : Type -> Type) where
52 ||| How to handle the effect.
53 |||
54 ||| @ r The resource being handled.
55 ||| @ eff The effect to be applied.
56 ||| @ k The continuation to pass the result of the effect
57 covering handle : (r : res) -> (eff : e t res resk) ->
58 (k : ((x : t) -> resk x -> m a)) -> m a
60||| Get the resource type (handy at the REPL to find out about an effect)
61resourceType : EFFECT -> Type
62resourceType (MkEff t e) = t
64-- --------------------------------------------------------- [ Syntactic Sugar ]
66-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
67-- up to a small number of parameters...)
69-- No state transition
70syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
72-- The state transition is dependent on a result `b`, a bound variable.
73syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
74 = eff inst (\b => outst)
76--- A simple state transition
77syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
79-- --------------------------------------- [ Properties and Proof Construction ]
80data SubList : List a -> List a -> Type where
81 SubNil : SubList [] []
82 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
83 Drop : SubList xs ys -> SubList xs (x :: ys)
85%hint
86subListId : SubList xs xs
87subListId {xs = Nil} = SubNil
88subListId {xs = x :: xs} = Keep subListId
90namespace Env
91 data Env : (m : Type -> Type) -> List EFFECT -> Type where
92 Nil : Env m Nil
93 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
95data EffElem : Effect -> Type ->
96 List EFFECT -> Type where
97 Here : EffElem x a (MkEff a x :: xs)
98 There : EffElem x a xs -> EffElem x a (y :: xs)
100||| make an environment corresponding to a sub-list
101dropEnv : Env m ys -> SubList xs ys -> Env m xs
102dropEnv [] SubNil = []
103dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
104dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
106updateWith : (ys' : List a) -> (xs : List a) ->
107 SubList ys xs -> List a
108updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
109updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
110updateWith [] [] SubNil = []
111updateWith (y :: ys) [] SubNil = y :: ys
112updateWith [] (x :: xs) (Keep rest) = []
114||| Put things back, replacing old with new in the sub-environment
115rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
116 Env m xs -> Env m (updateWith ys' xs prf)
117rebuildEnv [] SubNil env = env
118rebuildEnv (x :: xs) SubNil env = x :: xs
119rebuildEnv [] (Keep rest) (y :: env) = []
120rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
121rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
124-- -------------------------------------------------- [ The Effect EDSL itself ]
126updateResTy : (val : t) ->
127 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
128 List EFFECT
129updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
130updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
132infix 5 :::, :-, :=
134data LRes : lbl -> Type -> Type where
135 (:=) : (x : lbl) -> res -> LRes x res
137(:::) : lbl -> EFFECT -> EFFECT
138(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
140using (lbl : Type)
141 instance Default a => Default (LRes lbl a) where
142 default = lbl := default
144private
145unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
146unlabel {m} {x = MkEff a eff} [l := v] = [v]
148private
149relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
150relabel {xs = []} l [] = []
151relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
153-- ------------------------------------------------- [ The Language of Effects ]
154||| Definition of a language of effectful programs.
155|||
156||| @ x The return type of the result.
157||| @ es The list of allowed side-effects.
158||| @ ce Function to compute a new list of allowed side-effects.
159data EffM : (m : Type -> Type) -> (x : Type)
160 -> (es : List EFFECT)
161 -> (ce : x -> List EFFECT) -> Type where
162 value : (val : a) -> EffM m a (xs val) xs
163 ebind : EffM m a xs xs' ->
164 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
165 callP : (prf : EffElem e a xs) ->
166 (eff : e t a b) ->
167 EffM m t xs (\v => updateResTy v xs prf eff)
169 liftP : (prf : SubList ys xs) ->
170 EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
172 new : Handler e' m => (e : EFFECT) -> resTy ->
173 {auto prf : e = MkEff resTy e'} ->
174 EffM m t (e :: es) (\v => e :: es) ->
175 EffM m t es (\v => es)
177 (:-) : (l : ty) ->
178 EffM m t [x] xs' -> -- [x] (\v => xs) ->
179 EffM m t [l ::: x] (\v => map (l :::) (xs' v))
181-- Some type synonyms, so we don't always have to write EffM in full
183namespace SimpleEff
184 -- Simple effects, no updates
185 Eff : (x : Type) -> (es : List EFFECT) -> Type
186 Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
188 EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type
189 EffT m x es = EffM m x es (\v => es)
191namespace TransEff
192 -- Dependent effects, updates not dependent on result
193 Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
194 Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
196 EffT : (m : Type -> Type) ->
197 (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
198 EffT m x es ce = EffM m x es (\_ => ce)
200namespace DepEff
201 -- Dependent effects, updates dependent on result
202 Eff : (x : Type) -> (es : List EFFECT)
203 -> (ce : x -> List EFFECT) -> Type
204 Eff x es ce = {m : Type -> Type} -> EffM m x es ce
206 EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
207 -> (ce : x -> List EFFECT) -> Type
208 EffT m x es ce = EffM m x es ce
211%no_implicit
212(>>=) : EffM m a xs xs' ->
213 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
214(>>=) = ebind
216-- namespace SimpleBind
217-- (>>=) : Eff m a xs (\v => xs) ->
218-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
219-- (>>=) = ebind
221||| Run a subprogram which results in an effect state the same as the input.
222staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)
223staticEff = id
225||| Explicitly give the expected set of result effects for an effectful
226||| operation.
227toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
228toEff xs' = id
230return : a -> EffM m a xs (\v => xs)
231return x = value x
233-- ------------------------------------------------------ [ for idiom brackets ]
235infixl 2 <*>
237pure : a -> EffM m a xs (\v => xs)
238pure = value
240pureM : (val : a) -> EffM m a (xs val) xs
241pureM = value
243(<*>) : EffM m (a -> b) xs (\v => xs) ->
244 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
245(<*>) prog v = do fn <- prog
246 arg <- v
247 return (fn arg)
249-- ---------------------------------------------------------- [ an interpreter ]
251private
252execEff : Env m xs -> (p : EffElem e res xs) ->
253 (eff : e a res resk) ->
254 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
255execEff (val :: env) Here eff' k
256 = handle val eff' (\v, res => k v (res :: env))
257-- FIXME: Teach the elaborator to propagate parameters here
258execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
259 = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
261-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
262-- updates can be propagated even through failing computations?
264eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
265eff env (value x) k = k x env
266eff env (prog `ebind` c) k
267 = eff env prog (\p', env' => eff env' (c p') k)
268eff env (callP prf effP) k = execEff env prf effP k
269eff env (liftP prf effP) k
270 = let env' = dropEnv env prf in
271 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
272eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
273 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
274-- FIXME:
275-- xs is needed explicitly because otherwise the pattern binding for
276-- 'l' appears too late. Solution seems to be to reorder patterns at the
277-- end so that everything is in scope when it needs to be.
278eff {xs = [l ::: x]} env (l :- prog) k
279 = let env' = unlabel env in
280 eff env' prog (\p', envk => k p' (relabel l envk))
282-- yuck :) Haven't got type class instances working nicely in tactic
283-- proofs yet, and 'search' can't be told about any hints yet,
284-- so just brute force it.
285syntax MkDefaultEnv = with Env
286 (| [], [default], [default, default],
287 [default, default, default],
288 [default, default, default, default],
289 [default, default, default, default, default],
290 [default, default, default, default, default, default],
291 [default, default, default, default, default, default, default],
292 [default, default, default, default, default, default, default, default] |)
294call : {a, b: _} -> {e : Effect} ->
295 (eff : e t a b) ->
296 {auto prf : EffElem e a xs} ->
297 EffM m t xs (\v => updateResTy v xs prf eff)
298call e {prf} = callP prf e
300implicit
301lift : EffM m t ys ys' ->
302 {auto prf : SubList ys xs} ->
303 EffM m t xs (\v => updateWith (ys' v) xs prf)
304lift e {prf} = liftP prf e
307-- --------------------------------------------------------- [ Running Effects ]
308||| Run an effectful program.
309|||
310||| The content (`m`) in which to run the program is taken from the
311||| environment in which the program is called. The `env` argument is
312||| implicit and initialised automatically.
313|||
314||| @prog The effectful program to run.
315%no_implicit
316run : Applicative m =>
317 (prog : EffM m a xs xs') -> {default MkDefaultEnv env : Env m xs} ->
318 m a
319run prog {env} = eff env prog (\r, env => pure r)
321||| Run an effectful program in the identity context.
322|||
323||| A helper function useful for when the given context is 'pure'.
324||| The `env` argument is implicit and initialised automatically.
325|||
326||| @prog The effectful program to run.
327%no_implicit
328runPure : (prog : EffM id a xs xs') ->
329 {default MkDefaultEnv env : Env id xs} -> a
330runPure prog {env} = eff env prog (\r, env => r)
332||| Run an effectful program in a given context `m` with a default value for the environment.
333|||
334||| This is useful for when there is no default environment for the given context.
335|||
336||| @env The environment to use.
337||| @prog The effectful program to run.
338%no_implicit
339runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a
340runInit env prog = eff env prog (\r, env => pure r)
342||| Run an effectful program with a given default value for the environment.
343|||
344||| A helper function useful for when the given context is 'pure' and there is no default environment.
345|||
346||| @env The environment to use.
347||| @prog The effectful program to run.
348%no_implicit
349runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a
350runPureInit env prog = eff env prog (\r, env => r)
352%no_implicit
353runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
354runWith inj env prog = eff env prog (\r, env => inj r)
356%no_implicit
357runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
358 m (x : a ** Env m (xs' x))
359runEnv env prog = eff env prog (\r, env => pure (r ** env))
361-- ----------------------------------------------- [ some higher order things ]
363mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)
364mapE f [] = pure []
365mapE f (x :: xs) = [| f x :: mapE f xs |]
368mapVE : (a -> {xs} EffM m b) ->
369 Vect n a ->
370 {xs} EffM m (Vect n b)
371mapVE f [] = pure []
372mapVE f (x :: xs) = [| f x :: mapVE f xs |]
375when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()
376when True e = Force e
377when False e = pure ()
380-- --------------------------------------------------------------------- [ EOF ]