git.iko.soy/Idris-dev
on 16fe40d help sign in
Idris-dev/effects/Effects.idr
218 lines 7.4 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
84infix 5 :::, :-, :=
86data LRes : lbl -> Type -> Type where
87 (:=) : (x : lbl) -> res -> LRes x res
89(:::) : lbl -> EFFECT -> EFFECT
90(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
92private
93unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
94unlabel {m} {x = MkEff a eff} [l := v] = [v]
96private
97relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
98relabel {x = MkEff a eff} l [v] = [l := v]
100-- the language of Effects
102data EffM : (m : Type -> Type) ->
103 List EFFECT -> List EFFECT -> Type -> Type where
104 value : a -> EffM m xs xs a
105 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
106 effect : (prf : EffElem e a xs) ->
107 (eff : e a b t) ->
108 EffM m xs (updateResTy xs prf eff) t
109 lift : (prf : SubList ys xs) ->
110 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
111 new : Handler e m =>
112 res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
113 EffM m xs xs' a
114 catch : Catchable m err =>
115 EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
116 EffM m xs xs' a
117 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
119-- Eff : List (EFFECT m) -> Type -> Type
121implicit
122lift' : {default tactics { applyTactic findSubList 20; solve; }
123 prf : SubList ys xs} ->
124 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
125lift' {prf} e = lift prf e
127implicit
128effect' : {a, b: _} -> {e : Effect} ->
129 {default tactics { applyTactic findEffElem 20; solve; }
130 prf : EffElem e a xs} ->
131 (eff : e a b t) ->
132 EffM m xs (updateResTy xs prf eff) t
133effect' {prf} e = effect prf e
136-- for 'do' notation
138return : a -> EffM m xs xs a
139return x = value x
141(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
142(>>=) = ebind
144-- for idiom brackets
146infixl 2 <$>
148pure : a -> EffM m xs xs a
149pure = value
151(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b
152(<$>) prog v = do fn <- prog
153 arg <- v
154 return (fn arg)
156-- an interpreter
158private
159execEff : Env m xs -> (p : EffElem e res xs) ->
160 (eff : e res b a) ->
161 (Env m (updateResTy xs p eff) -> a -> m t) -> m t
162execEff (val :: env) Here eff' k
163 = handle val eff' (\res, v => k (res :: env) v)
164execEff (val :: env) (There p) eff k
165 = execEff env p eff (\env', v => k (val :: env') v)
167-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
168-- updates can be propagated even through failing computations?
170eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
171eff env (value x) k = k env x
172eff env (prog `ebind` c) k
173 = eff env prog (\env', p' => eff env' (c p') k)
174eff env (effect prf effP) k = execEff env prf effP k
175eff env (lift prf effP) k
176 = let env' = dropEnv env prf in
177 eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
178eff env (new r prog) k
179 = let env' = r :: env in
180 eff env' prog (\(v :: envk), p' => k envk p')
181eff env (catch prog handler) k
182 = catch (eff env prog k)
183 (\e => eff env (handler e) k)
184-- FIXME:
185-- xs is needed explicitly because otherwise the pattern binding for
186-- 'l' appears too late. Solution seems to be to reorder patterns at the
187-- end so that everything is in scope when it needs to be.
188eff {xs = [l ::: x]} env (l :- prog) k
189 = let env' = unlabel env in
190 eff env' prog (\envk, p' => k (relabel l envk) p')
192run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
193run env prog = eff env prog (\env, r => pure r)
195runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
196runEnv env prog = eff env prog (\env, r => pure (env, r))
198runPure : Env id xs -> EffM id xs xs' a -> a
199runPure env prog = eff env prog (\env, r => r)
201runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
202runPureEnv env prog = eff env prog (\env, r => (env, r))
204runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
205runWith inj env prog = eff env prog (\env, r => inj r)
207Eff : (Type -> Type) -> List EFFECT -> Type -> Type
208Eff m xs t = EffM m xs xs t
210-- some higher order things
212mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
213mapE f [] = pure []
214mapE f (x :: xs) = [| f x :: mapE f xs |]
216when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
217when True e = e
218when False e = pure ()