git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/effects/Effects.idr
315 lines 12 kB history raw
1module Effects
3import Language.Reflection
4import Control.Catchable
5import Effect.Default
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||| Handler classes describe how an effect `e` is translated to the
28||| underlying computation context `m` for execution.
29class 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
38||| Get the resource type (handy at the REPL to find out about an effect)
39resourceType : EFFECT -> Type
40resourceType (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
48syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
50-- The state transition is dependent on a result `b`, a bound variable.
51syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
52 = eff inst (\b => outst)
54--- A simple state transition
55syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
57-- --------------------------------------- [ Properties and Proof Construction ]
58data SubList : List a -> List a -> Type where
59 SubNil : SubList [] []
60 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
61 Drop : SubList xs ys -> SubList xs (x :: ys)
63subListId : SubList xs xs
64subListId {xs = Nil} = SubNil
65subListId {xs = x :: xs} = Keep subListId
67namespace Env
68 data Env : (m : Type -> Type) -> List EFFECT -> Type where
69 Nil : Env m Nil
70 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
72data EffElem : Effect -> Type ->
73 List EFFECT -> Type where
74 Here : EffElem x a (MkEff a x :: xs)
75 There : EffElem x a xs -> EffElem x a (y :: xs)
77||| make an environment corresponding to a sub-list
78dropEnv : Env m ys -> SubList xs ys -> Env m xs
79dropEnv [] SubNil = []
80dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
81dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
83updateWith : (ys' : List a) -> (xs : List a) ->
84 SubList ys xs -> List a
85updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
86updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
87updateWith [] [] SubNil = []
88updateWith (y :: ys) [] SubNil = y :: ys
89updateWith [] (x :: xs) (Keep rest) = []
91||| Put things back, replacing old with new in the sub-environment
92rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
93 Env m xs -> Env m (updateWith ys' xs prf)
94rebuildEnv [] SubNil env = env
95rebuildEnv (x :: xs) SubNil env = x :: xs
96rebuildEnv [] (Keep rest) (y :: env) = []
97rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
98rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
101-- -------------------------------------------------- [ The Effect EDSL itself ]
103updateResTy : (val : t) ->
104 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
105 List EFFECT
106updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
107updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
109infix 5 :::, :-, :=
111data LRes : lbl -> Type -> Type where
112 (:=) : (x : lbl) -> res -> LRes x res
114(:::) : lbl -> EFFECT -> EFFECT
115(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
117using (lbl : Type)
118 instance Default a => Default (LRes lbl a) where
119 default = lbl := default
121private
122unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
123unlabel {m} {x = MkEff a eff} [l := v] = [v]
125private
126relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
127relabel {xs = []} l [] = []
128relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
130-- ------------------------------------------------- [ The Language of Effects ]
131||| Definition of a language of effectful programs.
132|||
133||| @ x The return type of the result.
134||| @ es The list of allowed side-effects.
135||| @ ce Function to compute a new list of allowed side-effects.
136data Eff : (x : Type)
137 -> (es : List EFFECT)
138 -> (ce : x -> List EFFECT) -> Type where
139 value : a -> Eff a xs (\v => xs)
140 with_val : (val : a) -> Eff () xs (\v => xs' val) ->
141 Eff a xs xs'
142 ebind : Eff a xs xs' ->
143 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
144 callP : (prf : EffElem e a xs) ->
145 (eff : e t a b) ->
146 Eff t xs (\v => updateResTy v xs prf eff)
148 liftP : (prf : SubList ys xs) ->
149 Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
151 (:-) : (l : ty) ->
152 Eff t [x] xs' -> -- [x] (\v => xs) ->
153 Eff t [l ::: x] (\v => map (l :::) (xs' v))
155%no_implicit
156(>>=) : Eff a xs xs' ->
157 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
158(>>=) = ebind
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
165||| Run a subprogram which results in an effect state the same as the input.
166staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
167staticEff = id
169||| Explicitly give the expected set of result effects for an effectful
170||| operation.
171toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
172toEff xs' = id
174return : a -> Eff a xs (\v => xs)
175return x = value x
177-- ------------------------------------------------------ [ for idiom brackets ]
179infixl 2 <$>
181pure : a -> Eff a xs (\v => xs)
182pure = value
184syntax pureM [val] = with_val val (pure ())
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)
192-- ---------------------------------------------------------- [ an interpreter ]
194private
195execEff : 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
198execEff (val :: env) Here eff' k
199 = handle val eff' (\v, res => k v (res :: env))
200-- FIXME: Teach the elaborator to propagate parameters here
201execEff {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'))
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?
207eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
208eff env (value x) k = k x env
209eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
210eff env (prog `ebind` c) k
211 = eff env prog (\p', env' => eff env' (c p') k)
212eff env (callP prf effP) k = execEff env prf effP k
213eff 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.
220eff {xs = [l ::: x]} env (l :- prog) k
221 = let env' = unlabel env in
222 eff env' prog (\p', envk => k p' (relabel l envk))
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.
227syntax 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] |)
236call : {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)
241call e {prf} = callP prf e
243implicit
244lift : Eff t ys ys' ->
245 {default tactics { search 100; }
246 prf : SubList ys xs} ->
247 Eff t xs (\v => updateWith (ys' v) xs prf)
248lift e {prf} = liftP prf e
251-- --------------------------------------------------------- [ Running Effects ]
252||| Run an effectful program.
253|||
254||| The content (`m`) in which to run the program is taken from the
255||| environment in which the program is called. The `env` argument is
256||| implicit and initialised automatically.
257|||
258||| @prog The effectful program to run.
259run : Applicative m => {default MkDefaultEnv env : Env m xs}
260 -> (prog : Eff a xs xs') -> m a
261run {env} prog = eff env prog (\r, env => pure r)
263||| Run an effectful program in the identity context.
264|||
265||| A helper function useful for when the given context is 'pure'.
266||| The `env` argument is implicit and initialised automatically.
267|||
268||| @prog The effectful program to run.
269runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a
270runPure {env} prog = eff env prog (\r, env => r)
272||| Run an effectful program in a given context `m` with a default value for the environment.
273|||
274||| This is useful for when there is no default environment for the given context.
275|||
276||| @env The environment to use.
277||| @prog The effectful program to run.
278runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a
279runInit env prog = eff env prog (\r, env => pure r)
281||| Run an effectful program with a given default value for the environment.
282|||
283||| A helper function useful for when the given context is 'pure' and there is no default environment.
284|||
285||| @env The environment to use.
286||| @prog The effectful program to run.
287runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a
288runPureInit env prog = eff env prog (\r, env => r)
290runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
291runWith inj env prog = eff env prog (\r, env => inj r)
293runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
294 m (x : a ** Env m (xs' x))
295runEnv env prog = eff env prog (\r, env => pure (r ** env))
297-- ----------------------------------------------- [ some higher order things ]
299mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
300mapE f [] = pure []
301mapE f (x :: xs) = [| f x :: mapE f xs |]
304mapVE : (a -> {xs} Eff b) ->
305 Vect n a ->
306 {xs} Eff (Vect n b)
307mapVE f [] = pure []
308mapVE f (x :: xs) = [| f x :: mapVE f xs |]
311when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
312when True e = Force e
313when False e = pure ()
315-- --------------------------------------------------------------------- [ EOF ]