3import Language.Reflection
4import public Effect.Default
8--- Effectful computations are described as algebraic data types that
9--- explain how an effect is interpreted in some underlying context.
12-- ----------------------------------------------------------------- [ Effects ]
13||| The Effect type describes effectful computations.
15||| This type is parameterised by:
16||| + The return type of the computation.
17||| + The input resource.
18||| + The computation to run on the resource given the return value.
21Effect = (x : Type) -> Type -> (x -> Type) -> Type
23||| The `EFFECT` Data type describes how to promote the Effect
24||| description into a concrete effect.
27data EFFECT : Type where
28 MkEff : Type -> Effect -> EFFECT
30-- 'sig' gives the signature for an effect. There are four versions
31-- depending on whether there is no resource needed,
32-- no state change, a non-dependent change,
33-- or a dependent change. These are easily disambiguated by type.
35namespace NoResourceEffect
37 sig : Effect -> Type -> Type
38 sig e r = e r () (\v => ())
40namespace NoUpdateEffect
42 sig : Effect -> (ret : Type) -> (resource : Type) -> Type
43 sig e r e_in = e r e_in (\v => e_in)
47 sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type
48 sig e r e_in e_out = e r e_in (\v => e_out)
50namespace DepUpdateEffect
53 (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
54 sig e r e_in e_out = e r e_in e_out
56||| Handler interfaces describe how an effect `e` is translated to the
57||| underlying computation context `m` for execution.
59interface Handler (e : Effect) (m : Type -> Type) where
60 ||| How to handle the effect.
62 ||| @ r The resource being handled.
63 ||| @ eff The effect to be applied.
64 ||| @ k The continuation to pass the result of the effect
65 covering handle : (r : res) -> (eff : e t res resk) ->
66 (k : ((x : t) -> resk x -> m a)) -> m a
68||| Get the resource type (handy at the REPL to find out about an effect)
69resourceType : EFFECT -> Type
70resourceType (MkEff t e) = t
72-- --------------------------------------------------------- [ Syntactic Sugar ]
74-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
75-- up to a small number of parameters...)
78syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
80-- The state transition is dependent on a result `b`, a bound variable.
81syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
82 = eff inst (\b => outst)
84--- A simple state transition
85syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
87-- --------------------------------------- [ Properties and Proof Construction ]
90data SubElem : a -> List a -> Type where
91 Z : SubElem a (a :: as)
92 S : SubElem a as -> SubElem a (b :: as)
95data SubList : List a -> List a -> Type where
96 SubNil : SubList [] xs
97 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
99Uninhabited (SubElem x []) where
100 uninhabited Z impossible
101 uninhabited (S _) impossible
103-- Some useful hints for proof construction in polymorphic programs
106dropFirst : SubList xs ys -> SubList xs (x :: ys)
107dropFirst SubNil = SubNil
108dropFirst (InList el sub) = InList (S el) (dropFirst sub)
112subListId : (xs : List a) -> SubList xs xs
114subListId (x :: xs) = InList Z (dropFirst (subListId xs))
117inSuffix : SubElem x ys -> SubList xs ys -> SubElem x (zs ++ ys)
118inSuffix {zs = []} el sub = el
119inSuffix {zs = (x :: xs)} el sub = S (inSuffix el sub)
123dropPrefix : SubList xs ys -> SubList xs (zs ++ ys)
124dropPrefix SubNil = SubNil
125dropPrefix (InList el sub) = InList (inSuffix el sub) (dropPrefix sub)
128inPrefix : SubElem x ys -> SubList xs ys -> SubElem x (ys ++ zs)
129inPrefix {zs = []} {ys} el sub
130 = rewrite appendNilRightNeutral ys in el
131inPrefix {zs = (x :: xs)} Z sub = Z
132inPrefix {zs = (x :: xs)} (S y) sub = S (inPrefix y SubNil)
136dropSuffix : SubList xs ys -> SubList xs (ys ++ zs)
137dropSuffix SubNil = SubNil
138dropSuffix (InList el sub) = InList (inPrefix el sub) (dropSuffix sub)
142 data Env : (m : Type -> Type) -> List EFFECT -> Type where
144 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
146total envElem : SubElem x xs -> Env m xs -> Env m [x]
147envElem Z (x :: xs) = [x]
148envElem (S k) (x :: xs) = envElem k xs
150||| make an environment corresponding to a sub-list
151total dropEnv : Env m ys -> SubList xs ys -> Env m xs
152dropEnv [] SubNil = []
153dropEnv [] (InList idx rest) = absurd idx
154dropEnv (y::ys) SubNil = []
155dropEnv e@(y::ys) (InList idx rest) =
156 let [x] = envElem idx e
157 in x :: dropEnv e rest
160total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
162updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
163updateAt (S k) a [] = []
164updateAt (S k) a (x :: xs) = x :: updateAt k a xs
167total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
168 SubList ys xs -> List EFFECT
169updateWith [] xs sl = xs
170updateWith (y :: ys) xs SubNil = xs
171updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
174total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
175 Env m (updateAt idx a ys)
176replaceEnvAt x Z [] = []
177replaceEnvAt x Z (y :: ys) = x :: ys
178replaceEnvAt x (S k) [] = []
179replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
181||| Put things back, replacing old with new in the sub-environment
183total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
184 Env m xs -> Env m (updateWith ys' xs prf)
185rebuildEnv [] SubNil env = env
186rebuildEnv (x :: xs) SubNil env = env
187rebuildEnv [] (InList w s) env = env
188rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
190-- -------------------------------------------------- [ The Effect EDSL itself ]
193total updateResTy : (val : t) ->
194 (xs : List EFFECT) -> with List Elem (MkEff a e) xs -> e t a b ->
196updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
197updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
202data LRes : lbl -> Type -> Type where
203 (:=) : (x : lbl) -> res -> LRes x res
206(:::) : lbl -> EFFECT -> EFFECT
207(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
210 implementation Default a => Default (LRes lbl a) where
211 default = lbl := default
214unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
215unlabel {m} {x = MkEff a eff} [l := v] = [v]
218relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
219relabel {xs = []} l [] = []
220relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
222-- ------------------------------------------------- [ The Language of Effects ]
223||| Definition of a language of effectful programs.
225||| @ x The return type of the result.
226||| @ es The list of allowed side-effects.
227||| @ ce Function to compute a new list of allowed side-effects.
229data EffM : (m : Type -> Type) -> (x : Type)
230 -> (es : List EFFECT)
231 -> (ce : x -> List EFFECT) -> Type where
232 Value : (val : a) -> EffM m a (xs val) xs
233 EBind : EffM m a xs xs' ->
234 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
235 CallP : (prf : with List Elem (MkEff a e) xs) ->
237 EffM m t xs (\v => updateResTy v xs prf eff)
239 LiftP : (prf : SubList ys xs) ->
240 EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
242 New : Handler e' m => (e : EFFECT) -> resTy ->
243 {auto prf : e = MkEff resTy e'} ->
244 EffM m t (e :: es) (\v => e :: es) ->
245 EffM m t es (\v => es)
248 EffM m t [x] xs' -> -- [x] (\v => xs) ->
249 EffM m t [l ::: x] (\v => map (l :::) (xs' v))
251-- Some type synonyms, so we don't always have to write EffM in full
254 -- Simple effects, no updates
256 Eff : (x : Type) -> (es : List EFFECT) -> Type
257 Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
260 EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type
261 EffT m x es = EffM m x es (\v => es)
264 -- Dependent effects, updates not dependent on result
266 Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
267 Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
270 EffT : (m : Type -> Type) ->
271 (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
272 EffT m x es ce = EffM m x es (\_ => ce)
275 -- Dependent effects, updates dependent on result
277 Eff : (x : Type) -> (es : List EFFECT)
278 -> (ce : x -> List EFFECT) -> Type
279 Eff x es ce = {m : Type -> Type} -> EffM m x es ce
282 EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
283 -> (ce : x -> List EFFECT) -> Type
284 EffT m x es ce = EffM m x es ce
288(>>=) : EffM m a xs xs' ->
289 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
292-- namespace SimpleBind
293-- (>>=) : Eff m a xs (\v => xs) ->
294-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
297||| Run a subprogram which results in an effect state the same as the input.
298staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)
301||| Explicitly give the expected set of result effects for an effectful
303toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
306pure : a -> EffM m a xs (\v => xs)
309pureM : (val : a) -> EffM m a (xs val) xs
312(<*>) : EffM m (a -> b) xs (\v => xs) ->
313 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
314(<*>) prog v = do fn <- prog
319 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
320(<$>) f v = pure f <*> v
322(*>) : EffM m a xs (\v => xs) ->
323 EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
327new : Handler e' m => (e : EFFECT) -> resTy ->
328 {auto prf : e = MkEff resTy e'} ->
329 EffM m t (e :: es) (\v => e :: es) ->
330 EffM m t es (\v => es)
333-- ---------------------------------------------------------- [ an interpreter ]
336execEff : Env m xs -> (p : with List Elem (MkEff res e) xs) ->
337 (eff : e a res resk) ->
338 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
339execEff (val :: env) Here eff' k
340 = handle val eff' (\v, res => k v (res :: env))
341execEff (val :: env) (There p) eff k
342 = execEff env p eff (\v, env' => k v (val :: env'))
344-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
345-- updates can be propagated even through failing computations?
348eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
349eff env (Value x) k = k x env
350eff env (prog `EBind` c) k
351 = eff env prog (\p', env' => eff env' (c p') k)
352eff env (CallP prf effP) k = execEff env prf effP k
353eff env (LiftP prf effP) k
354 = let env' = dropEnv env prf in
355 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
356eff env (New (MkEff resTy newEff) res {prf=Refl} effP) k
357 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
359 = let env' = unlabel env in
360 eff env' prog (\p', envk => k p' (relabel l envk))
362-- yuck :) Haven't got interface implementations working nicely in tactic
363-- proofs yet, and 'search' can't be told about any hints yet,
364-- so just brute force it.
365syntax MkDefaultEnv = with Env
366 (| [], [default], [default, default],
367 [default, default, default],
368 [default, default, default, default],
369 [default, default, default, default, default],
370 [default, default, default, default, default, default],
371 [default, default, default, default, default, default, default],
372 [default, default, default, default, default, default, default, default] |)
375call : {a, b: _} -> {e : Effect} ->
377 {auto prf : with List Elem (MkEff a e) xs} ->
378 EffM m t xs (\v => updateResTy v xs prf eff)
379call e {prf} = CallP prf e
382lift : EffM m t ys ys' ->
383 {auto prf : SubList ys xs} ->
384 EffM m t xs (\v => updateWith (ys' v) xs prf)
385lift e {prf} = LiftP prf e
388-- --------------------------------------------------------- [ Running Effects ]
389||| Run an effectful program.
391||| The content (`m`) in which to run the program is taken from the
392||| environment in which the program is called. The `env` argument is
393||| implicit and initialised automatically.
395||| @prog The effectful program to run.
397run : Applicative m =>
398 (prog : EffM m a xs xs') -> {default MkDefaultEnv env : Env m xs} ->
400run prog {env} = eff env prog (\r, env => pure r)
402||| Run an effectful program in the identity context.
404||| A helper function useful for when the given context is 'pure'.
405||| The `env` argument is implicit and initialised automatically.
407||| @prog The effectful program to run.
409runPure : (prog : EffM Basics.id a xs xs') ->
410 {default MkDefaultEnv env : Env Basics.id xs} -> a
411runPure prog {env} = eff env prog (\r, env => r)
413||| Run an effectful program in a given context `m` with a default value for the environment.
415||| This is useful for when there is no default environment for the given context.
417||| @env The environment to use.
418||| @prog The effectful program to run.
420runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a
421runInit env prog = eff env prog (\r, env => pure r)
423||| Run an effectful program with a given default value for the environment.
425||| A helper function useful for when the given context is 'pure' and there is no default environment.
427||| @env The environment to use.
428||| @prog The effectful program to run.
430runPureInit : (env : Env Basics.id xs) -> (prog : EffM Basics.id a xs xs') -> a
431runPureInit env prog = eff env prog (\r, env => r)
434runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
435runWith inj env prog = eff env prog (\r, env => inj r)
437||| Similar to 'runInit', but take the result of `Env`.
439runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
440 m (x : a ** Env m (xs' x))
441runEnv env prog = eff env prog (\r, env => pure (r ** env))
443||| Similar to 'runEnv', but the context (m) is 'pure'
445runPureEnv : (env : Env Basics.id xs) -> (prog : EffM Basics.id a xs xs') -> (x : a ** Env Basics.id (xs' x))
446runPureEnv env prog = eff env prog (\r, env => (r ** env))
448-- ----------------------------------------------- [ some higher order things ]
450mapE : (a -> EffM m b xs (\_ => xs)) -> List a -> EffM m (List b) xs (\_ => xs)
452mapE f (x :: xs) = [| f x :: mapE f xs |]
455mapVE : (a -> EffM m b xs (\_ => xs)) ->
457 EffM m (Vect n b) xs (\_ => xs)
459mapVE f (x :: xs) = [| f x :: mapVE f xs |]
462when : Bool -> Lazy (EffM m () xs (\_ => xs)) -> EffM m () xs (\_ => xs)
464when False e = pure ()
467-- --------------------------------------------------------------------- [ EOF ]
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list