git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/libs/effects/Effects.idr
314 lines 11 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||| 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 : (val : a) -> Eff a (xs val) xs
140 ebind : Eff a xs xs' ->
141 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
142 callP : (prf : EffElem e a xs) ->
143 (eff : e t a b) ->
144 Eff t xs (\v => updateResTy v xs prf eff)
146 liftP : (prf : SubList ys xs) ->
147 Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
149 (:-) : (l : ty) ->
150 Eff t [x] xs' -> -- [x] (\v => xs) ->
151 Eff t [l ::: x] (\v => map (l :::) (xs' v))
153%no_implicit
154(>>=) : Eff a xs xs' ->
155 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
156(>>=) = ebind
158-- namespace SimpleBind
159-- (>>=) : Eff m a xs (\v => xs) ->
160-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
161-- (>>=) = ebind
163||| Run a subprogram which results in an effect state the same as the input.
164staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
165staticEff = id
167||| Explicitly give the expected set of result effects for an effectful
168||| operation.
169toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
170toEff xs' = id
172return : a -> Eff a xs (\v => xs)
173return x = value x
175-- ------------------------------------------------------ [ for idiom brackets ]
177infixl 2 <*>
179pure : a -> Eff a xs (\v => xs)
180pure = value
182pureM : (val : a) -> Eff a (xs val) xs
183pureM = value
185(<*>) : Eff (a -> b) xs (\v => xs) ->
186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
187(<*>) prog v = do fn <- prog
188 arg <- v
189 return (fn arg)
191-- ---------------------------------------------------------- [ an interpreter ]
193private
194execEff : Env m xs -> (p : EffElem e res xs) ->
195 (eff : e a res resk) ->
196 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
197execEff (val :: env) Here eff' k
198 = handle val eff' (\v, res => k v (res :: env))
199-- FIXME: Teach the elaborator to propagate parameters here
200execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
201 = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
203-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
204-- updates can be propagated even through failing computations?
206eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
207eff env (value x) k = k x env
208eff env (prog `ebind` c) k
209 = eff env prog (\p', env' => eff env' (c p') k)
210eff env (callP prf effP) k = execEff env prf effP k
211eff env (liftP prf effP) k
212 = let env' = dropEnv env prf in
213 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
214-- FIXME:
215-- xs is needed explicitly because otherwise the pattern binding for
216-- 'l' appears too late. Solution seems to be to reorder patterns at the
217-- end so that everything is in scope when it needs to be.
218eff {xs = [l ::: x]} env (l :- prog) k
219 = let env' = unlabel env in
220 eff env' prog (\p', envk => k p' (relabel l envk))
222-- yuck :) Haven't got type class instances working nicely in tactic
223-- proofs yet, and 'search' can't be told about any hints yet,
224-- so just brute force it.
225syntax MkDefaultEnv = with Env
226 (| [], [default], [default, default],
227 [default, default, default],
228 [default, default, default, default],
229 [default, default, default, default, default],
230 [default, default, default, default, default, default],
231 [default, default, default, default, default, default, default],
232 [default, default, default, default, default, default, default, default] |)
234call : {a, b: _} -> {e : Effect} ->
235 (eff : e t a b) ->
236 {default tactics { search 100; }
237 prf : EffElem e a xs} ->
238 Eff t xs (\v => updateResTy v xs prf eff)
239call e {prf} = callP prf e
241implicit
242lift : Eff t ys ys' ->
243 {default tactics { search 100; }
244 prf : SubList ys xs} ->
245 Eff t xs (\v => updateWith (ys' v) xs prf)
246lift e {prf} = liftP prf e
249-- --------------------------------------------------------- [ Running Effects ]
250||| Run an effectful program.
251|||
252||| The content (`m`) in which to run the program is taken from the
253||| environment in which the program is called. The `env` argument is
254||| implicit and initialised automatically.
255|||
256||| @prog The effectful program to run.
257run : Applicative m => {default MkDefaultEnv env : Env m xs}
258 -> (prog : Eff a xs xs') -> m a
259run {env} prog = eff env prog (\r, env => pure r)
261||| Run an effectful program in the identity context.
262|||
263||| A helper function useful for when the given context is 'pure'.
264||| The `env` argument is implicit and initialised automatically.
265|||
266||| @prog The effectful program to run.
267runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a
268runPure {env} prog = eff env prog (\r, env => r)
270||| Run an effectful program in a given context `m` with a default value for the environment.
271|||
272||| This is useful for when there is no default environment for the given context.
273|||
274||| @env The environment to use.
275||| @prog The effectful program to run.
276runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a
277runInit env prog = eff env prog (\r, env => pure r)
279||| Run an effectful program with a given default value for the environment.
280|||
281||| A helper function useful for when the given context is 'pure' and there is no default environment.
282|||
283||| @env The environment to use.
284||| @prog The effectful program to run.
285runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a
286runPureInit env prog = eff env prog (\r, env => r)
288runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
289runWith inj env prog = eff env prog (\r, env => inj r)
291runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
292 m (x : a ** Env m (xs' x))
293runEnv env prog = eff env prog (\r, env => pure (r ** env))
295-- ----------------------------------------------- [ some higher order things ]
297mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
298mapE f [] = pure []
299mapE f (x :: xs) = [| f x :: mapE f xs |]
302mapVE : (a -> {xs} Eff b) ->
303 Vect n a ->
304 {xs} Eff (Vect n b)
305mapVE f [] = pure []
306mapVE f (x :: xs) = [| f x :: mapVE f xs |]
309when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
310when True e = Force e
311when False e = pure ()
314-- --------------------------------------------------------------------- [ EOF ]