@@ -0,0 +1,63 @@
1+module Effect.Protocols
3+-- Helpers for writing and using effects that implement protocols with
10+-- 'sig' gives the signature for an effect. There are three versions
11+-- depending on whether there is no state change, a non-dependent change,
12+-- or a dependent change. These are easily disambiguated by type.
14+namespace NoUpdateEffect
15+ sig : Effect -> Type -> Type -> Type
16+ sig e r e_in = e r e_in (\v => e_in)
18+namespace UpdateEffect
19+ sig : Effect -> Type -> Type -> Type -> Type
20+ sig e r e_in e_out = e r e_in (\v => e_out)
22+namespace DepUpdateEffect
23+ sig : Effect -> (x : Type) -> Type -> (x -> Type) -> Type
24+ sig e r e_in e_out = e r e_in e_out
27+-- a single effect transition.
29+data EffTrans : Type -> Type -> Type where
30+ (:=>) : a -> b -> EffTrans a b
32+-- 'trans' gives a single effect transition. Again three versions, for
33+-- no transition, non-dependent transition and dependent transition, again
34+-- disambiguated by type, but the one with no update can be implicit.
36+namespace NoUpdateTrans
38+ trans : a -> EffTrans a (x -> a)
39+ trans t = t :=> (\v => t)
42+ trans : a -> b -> EffTrans a (x -> b)
43+ trans s t = s :=> (\v => t)
45+namespace DepUpdateTrans
46+ trans : a -> b -> EffTrans a b
50+ List (EffTrans EFFECT (x -> EFFECT)) ->
52+Proto x xs = Eff x (proto_in xs) (\val : x => proto_out xs val)
54+ proto_out : List (EffTrans EFFECT (x -> EFFECT)) -> x -> List EFFECT
55+ proto_out [] val = []
56+ proto_out ((e_in :=> e_out) :: xs) val
57+ = let rec = proto_out xs val in e_out val :: rec
59+ proto_in : List (EffTrans EFFECT (x -> EFFECT)) -> List EFFECT
61+ proto_in ((e_in :=> e_out) :: xs)
62+ = let rec = proto_in xs in e_in :: rec