@@ -0,0 +1,207 @@
3+import Language.Reflection
4+import Control.Catchable
11+Effect = Type -> Type -> Type -> Type
14+ MkEff : Type -> Effect -> EFF
16+class 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
21+using (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
31+data Env : (m : Type -> Type) -> List EFF -> Type where
33+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
35+data EffElem : (Type -> Type -> Type -> Type) -> Type ->
36+ List EFF -> 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
41+dropEnv : Env m ys -> SubList xs ys -> Env m xs
42+dropEnv [] SubNil = []
43+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
44+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
46+updateWith : (ys' : List a) -> (xs : List a) ->
47+ SubList ys xs -> List a
48+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
49+updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
50+updateWith [] [] SubNil = []
52+-- put things back, replacing old with new in the sub-environment
53+rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
54+ Env m xs -> Env m (updateWith ys' xs prf)
55+rebuildEnv [] SubNil env = env
56+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
57+rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
59+---- The Effect EDSL itself ----
61+-- some proof automation
62+findEffElem : Nat -> Tactic -- Nat is maximum search depth
63+findEffElem O = Refine "Here" `Seq` Solve
64+findEffElem (S n) = GoalType "EffElem"
65+ (Try (Refine "Here" `Seq` Solve)
66+ (Refine "There" `Seq` (Solve `Seq` findEffElem n)))
68+findSubList : Nat -> Tactic
69+findSubList O = Refine "SubNil" `Seq` Solve
72+ (Try (Refine "subListId" `Seq` Solve)
73+ ((Try (Refine "Keep" `Seq` Solve)
74+ (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))
76+updateResTy : (xs : List EFF) -> EffElem e a xs -> e a b t ->
78+updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
79+updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
83+data LRes : lbl -> Type -> Type where
84+ (:=) : (x : lbl) -> res -> LRes x res
86+(:::) : lbl -> EFF -> EFF
87+(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
90+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
91+unlabel {m} {x = MkEff a eff} [l := v] = [v]
94+relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
95+relabel {x = MkEff a eff} l [v] = [l := v]
97+-- the language of Effects
99+data EffM : (m : Type -> Type) ->
100+ List EFF -> List EFF -> Type -> Type where
101+ value : a -> EffM m xs xs a
102+ ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
103+ effect : {a, b: _} -> {e : Effect} ->
104+ (prf : EffElem e a xs) ->
106+ EffM m xs (updateResTy xs prf eff) t
107+ lift : (prf : SubList ys xs) ->
108+ EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
109+ new : Handler e m =>
110+ res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
112+ catch : Catchable m err =>
113+ EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
115+ (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
117+-- Eff : List (EFF m) -> Type -> Type
120+lift' : {default tactics { reflect findSubList 10; solve; }
121+ prf : SubList ys xs} ->
122+ EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
123+lift' {prf} e = lift prf e
126+effect' : {a, b: _} -> {e : Effect} ->
127+ {default tactics { reflect findEffElem 10; solve; }
128+ prf : EffElem e a xs} ->
130+ EffM m xs (updateResTy xs prf eff) t
131+effect' {prf} e = effect prf e
136+return : a -> EffM m xs xs a
139+(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
142+-- for idiom brackets
146+pure : a -> EffM m xs xs a
149+(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b
150+(<$>) prog v = do fn <- prog
157+execEff : Env m xs -> (p : EffElem e res xs) ->
158+ (eff : e res b a) ->
159+ (Env m (updateResTy xs p eff) -> a -> m t) -> m t
160+execEff (val :: env) Here eff' k
161+ = handle val eff' (\res, v => k (res :: env) v)
162+execEff (val :: env) (There p) eff k
163+ = execEff env p eff (\env', v => k (val :: env') v)
165+eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
166+eff env (value x) k = k env x
167+eff env (prog `ebind` c) k
168+ = eff env prog (\env', p' => eff env' (c p') k)
169+eff env (effect prf effP) k = execEff env prf effP k
170+eff env (lift prf effP) k
171+ = let env' = dropEnv env prf in
172+ eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
173+eff env (new r prog) k
174+ = let env' = r :: env in
175+ eff env' prog (\(v :: envk), p' => k envk p')
176+eff env (catch prog handler) k
177+ = catch (eff env prog k)
178+ (\e => eff env (handler e) k)
179+eff {xs = [l ::: x]} env (l :- prog) k
180+ = let env' = unlabel {l} env in
181+ eff env' prog (\envk, p' => k (relabel l envk) p')
183+run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
184+run env prog = eff env prog (\env, r => pure r)
186+runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
187+runEnv env prog = eff env prog (\env, r => pure (env, r))
189+runPure : Env id xs -> EffM id xs xs' a -> a
190+runPure env prog = eff env prog (\env, r => r)
192+runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
193+runWith inj env prog = eff env prog (\env, r => inj r)
195+Eff : (Type -> Type) -> List EFF -> Type -> Type
196+Eff m xs t = EffM m xs xs t
198+-- some higher order things
200+mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
202+mapE f (x :: xs) = [| f x :: mapE f xs |]
204+when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
206+when False e = pure ()