git.iko.soy/Idris-dev
on bfa39bf help sign in
Idris-dev/effects/Effects.idr
289 lines 10 kB history raw
1module Effects
3import Language.Reflection
4import Control.Catchable
6%access public
8---- Effects
10Effect : Type
11Effect = Type -> Type -> Type -> Type
13data EFFECT : Type where
14 MkEff : Type -> Effect -> EFFECT
16class Handler (e : Effect) (m : Type -> Type) where
17 handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a
19---- Properties and proof construction
21using (xs : List a, ys : List a)
22 data SubList : List a -> List a -> Type where
23 SubNil : SubList {a} [] []
24 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
25 Drop : SubList xs ys -> SubList xs (x :: ys)
27 subListId : SubList xs xs
28 subListId {xs = Nil} = SubNil
29 subListId {xs = x :: xs} = Keep subListId
31data Env : (m : Type -> Type) -> List EFFECT -> Type where
32 Nil : Env m Nil
33 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
35data EffElem : (Type -> Type -> Type -> Type) -> Type ->
36 List EFFECT -> Type where
37 Here : EffElem x a (MkEff a x :: xs)
38 There : EffElem x a xs -> EffElem x a (y :: xs)
40-- make an environment corresponding to a sub-list
41dropEnv : Env m ys -> SubList xs ys -> Env m xs
42dropEnv [] SubNil = []
43dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
44dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
46updateWith : (ys' : List a) -> (xs : List a) ->
47 SubList ys xs -> List a
48updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
49updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
50updateWith [] [] SubNil = []
51updateWith (y :: ys) [] SubNil = y :: ys
52updateWith [] (x :: xs) (Keep rest) = []
54-- put things back, replacing old with new in the sub-environment
55rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
56 Env m xs -> Env m (updateWith ys' xs prf)
57rebuildEnv [] SubNil env = env
58rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
59rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
60rebuildEnv (x :: xs) SubNil [] = x :: xs
62---- The Effect EDSL itself ----
64-- some proof automation
65findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
66findEffElem Z ctxt goal = Refine "Here" `Seq` Solve
67findEffElem (S n) ctxt goal = GoalType "EffElem"
68 (Try (Refine "Here" `Seq` Solve)
69 (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))
71findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic
72findSubList Z ctxt goal = Refine "SubNil" `Seq` Solve
73findSubList (S n) ctxt goal
74 = GoalType "SubList"
75 (Try (Refine "subListId" `Seq` Solve)
76 ((Try (Refine "Keep" `Seq` Solve)
77 (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt goal))
79updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
80 List EFFECT
81updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
82updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
84updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
85 List EFFECT
86updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
87updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
89infix 5 :::, :-, :=
91data LRes : lbl -> Type -> Type where
92 (:=) : (x : lbl) -> res -> LRes x res
94(:::) : lbl -> EFFECT -> EFFECT
95(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
97private
98unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
99unlabel {m} {x = MkEff a eff} [l := v] = [v]
101private
102relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
103relabel {x = MkEff a eff} l [v] = [l := v]
105-- the language of Effects
107data EffM : (m : Type -> Type) ->
108 List EFFECT -> List EFFECT -> Type -> Type where
109 value : a -> EffM m xs xs a
110 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
111 effect : (prf : EffElem e a xs) ->
112 (eff : e a b t) ->
113 EffM m xs (updateResTy xs prf eff) t
114 lift : (prf : SubList ys xs) ->
115 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
116 new : Handler e m =>
117 res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
118 EffM m xs xs' a
119 test : (prf : EffElem e (Either l r) xs) ->
120 EffM m (updateResTyImm xs prf l) xs' t ->
121 EffM m (updateResTyImm xs prf r) xs' t ->
122 EffM m xs xs' t
123 test_lbl : {x : lbl} ->
124 (prf : EffElem e (LRes x (Either l r)) xs) ->
125 EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
126 EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
127 EffM m xs xs' t
128 catch : Catchable m err =>
129 EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
130 EffM m xs xs' a
131 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
133syntax [tag] ":!" [val] = !(tag :- val)
135-- Eff : List (EFFECT m) -> Type -> Type
137implicit
138lift' : {default tactics { applyTactic findSubList 20; solve; }
139 prf : SubList ys xs} ->
140 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
141lift' {prf} e = lift prf e
143implicit
144effect' : {a, b: _} -> {e : Effect} ->
145 {default tactics { applyTactic findEffElem 20; solve; }
146 prf : EffElem e a xs} ->
147 (eff : e a b t) ->
148 EffM m xs (updateResTy xs prf eff) t
149effect' {prf} e = effect prf e
151-- For making proofs implicitly for 'test' and 'test_lbl'
153syntax if_valid then [e] else [t] =
154 test (tactics { applyTactic findEffElem 20; solve; }) t e
156syntax if_valid [lbl] then [e] else [t] =
157 test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e
159syntax if_error then [t] else [e] =
160 test (tactics { applyTactic findEffElem 20; solve; }) t e
162syntax if_error [lbl] then [t] else [e] =
163 test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e
165-- These may read better in some contexts
167syntax if_right then [e] else [t] =
168 test (tactics { applyTactic findEffElem 20; solve; }) t e
170syntax if_right [lbl] then [e] else [t] =
171 test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e
173syntax if_left then [t] else [e] =
174 test (tactics { applyTactic findEffElem 20; solve; }) t e
176syntax if_left [lbl] then [t] else [e] =
177 test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e
180-- for 'do' notation
182return : a -> EffM m xs xs a
183return x = value x
185(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
186(>>=) = ebind
188-- for idiom brackets
190infixl 2 <$>
192pure : a -> EffM m xs xs a
193pure = value
195(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b
196(<$>) prog v = do fn <- prog
197 arg <- v
198 return (fn arg)
200-- an interpreter
202private
203execEff : Env m xs -> (p : EffElem e res xs) ->
204 (eff : e res b a) ->
205 (Env m (updateResTy xs p eff) -> a -> m t) -> m t
206execEff (val :: env) Here eff' k
207 = handle val eff' (\res, v => k (res :: env) v)
208execEff (val :: env) (There p) eff k
209 = execEff env p eff (\env', v => k (val :: env') v)
211private
212testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->
213 (Env m (updateResTyImm xs p l) -> m b) ->
214 (Env m (updateResTyImm xs p r) -> m b) ->
215 m b
216testEff (Left err :: env) Here lk rk = lk (err :: env)
217testEff (Right ok :: env) Here lk rk = rk (ok :: env)
218testEff (val :: env) (There p) lk rk
219 = testEff env p (\envk => lk (val :: envk))
220 (\envk => rk (val :: envk))
222private
223testEffLbl : {x : lbl} ->
224 Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->
225 (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->
226 (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->
227 m b
228testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)
229testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)
230testEffLbl (val :: env) (There p) lk rk
231 = testEffLbl env p (\envk => lk (val :: envk))
232 (\envk => rk (val :: envk))
234-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
235-- updates can be propagated even through failing computations?
237eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
238eff env (value x) k = k env x
239eff env (prog `ebind` c) k
240 = eff env prog (\env', p' => eff env' (c p') k)
241eff env (effect prf effP) k = execEff env prf effP k
242eff env (lift prf effP) k
243 = let env' = dropEnv env prf in
244 eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
245eff env (new r prog) k
246 = let env' = r :: env in
247 eff env' prog (\(v :: envk), p' => k envk p')
248eff env (test prf l r) k
249 = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)
250eff env (test_lbl prf l r) k
251 = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)
252eff env (catch prog handler) k
253 = catch (eff env prog k)
254 (\e => eff env (handler e) k)
255-- FIXME:
256-- xs is needed explicitly because otherwise the pattern binding for
257-- 'l' appears too late. Solution seems to be to reorder patterns at the
258-- end so that everything is in scope when it needs to be.
259eff {xs = [l ::: x]} env (l :- prog) k
260 = let env' = unlabel env in
261 eff env' prog (\envk, p' => k (relabel l envk) p')
263run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
264run env prog = eff env prog (\env, r => pure r)
266runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
267runEnv env prog = eff env prog (\env, r => pure (env, r))
269runPure : Env id xs -> EffM id xs xs' a -> a
270runPure env prog = eff env prog (\env, r => r)
272runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
273runPureEnv env prog = eff env prog (\env, r => (env, r))
275runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
276runWith inj env prog = eff env prog (\env, r => inj r)
278Eff : (Type -> Type) -> List EFFECT -> Type -> Type
279Eff m xs t = EffM m xs xs t
281-- some higher order things
283mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
284mapE f [] = pure []
285mapE f (x :: xs) = [| f x :: mapE f xs |]
287when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
288when True e = e
289when False e = pure ()