@@ -4,35 +4,57 @@ import Language.Reflection
44import Control.Catchable
55import Effect.Default
66
7−%access public
8−
9−---- Effects
7+--- Effectful computations are described as algebraic data types that
8+--- explain how an effect is interpreted in some underlying context.
109
10+%access public
11+-- ----------------------------------------------------------------- [ Effects ]
12+||| The Effect type describes effectful computations.
13+|||
14+||| This type is parameterised by:
15+||| + The input resource.
16+||| + The return type of the computation.
17+||| + The computation to run on the resource.
1118Effect : Type
1219Effect = (x : Type) -> Type -> (x -> Type) -> Type
1320
21+||| The `EFFECT` Data type describes how to promote the Effect
22+||| description into a concrete effect.
1423%error_reverse
1524data EFFECT : Type where
1625 MkEff : Type -> Effect -> EFFECT
1726
27+||| Handler classes describe how an effect `e` is translated to the
28+||| underlying computation context `m` for execution.
1829class Handler (e : Effect) (m : Type -> Type) where
19− handle : res -> (eff : e t res resk) ->
20− ((x : t) -> resk x -> m a) -> m a
21−
22−-- Get the resource type (handy at the REPL to find out about an effect)
30+ ||| How to handle the effect.
31+ |||
32+ ||| @ r The resource being handled.
33+ ||| @ eff The effect to be applied.
34+ ||| @ ctxt The context in which to handle the effect.
35+ handle : (r : res) -> (eff : e t res resk) ->
36+ (ctxt : ((x : t) -> resk x -> m a)) -> m a
37+
38+||| Get the resource type (handy at the REPL to find out about an effect)
2339resourceType : EFFECT -> Type
2440resourceType (MkEff t e) = t
2541
42+-- --------------------------------------------------------- [ Syntactic Sugar ]
43+
2644-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
2745-- up to a small number of parameters...)
2846
47+-- No state transition
2948syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
49+
50+-- The state transition is dependent on a result `b`, a bound variable.
3051syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
3152 = eff inst (\b => outst)
32−syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
3353
34−---- Properties and proof construction
54+--- A simple state transition
55+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
3556
57+-- --------------------------------------- [ Properties and Proof Construction ]
3658using (xs : List a, ys : List a)
3759 data SubList : List a -> List a -> Type where
3860 SubNil : SubList {a} [] []
@@ -53,7 +75,7 @@ data EffElem : Effect -> Type ->
5375 Here : EffElem x a (MkEff a x :: xs)
5476 There : EffElem x a xs -> EffElem x a (y :: xs)
5577
56−-- make an environment corresponding to a sub-list
78+||| make an environment corresponding to a sub-list
5779dropEnv : Env m ys -> SubList xs ys -> Env m xs
5880dropEnv [] SubNil = []
5981dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
@@ -67,7 +89,7 @@ updateWith [] [] SubNil = []
6789updateWith (y :: ys) [] SubNil = y :: ys
6890updateWith [] (x :: xs) (Keep rest) = []
6991
70−-- put things back, replacing old with new in the sub-environment
92+||| Put things back, replacing old with new in the sub-environment
7193rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
7294 Env m xs -> Env m (updateWith ys' xs prf)
7395rebuildEnv [] SubNil env = env
@@ -75,8 +97,7 @@ rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
7597rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
7698rebuildEnv (x :: xs) SubNil [] = x :: xs
7799
78−---- The Effect EDSL itself ----
79−
100+-- -------------------------------------------------- [ The Effect EDSL itself ]
80101-- some proof automation
81102
82103%reflection
@@ -131,11 +152,6 @@ updateResTy : (val : t) ->
131152updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
132153updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
133154
134−-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
135−-- List EFFECT
136−-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
137−-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
138−
139155infix 5 :::, :-, :=
140156
141157data LRes : lbl -> Type -> Type where
@@ -157,11 +173,17 @@ relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
157173relabel {xs = []} l [] = []
158174relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
159175
160−-- the language of Effects
161−
162−data Eff : (m : Type -> Type) ->
163− (x : Type) ->
164− List EFFECT -> (x -> List EFFECT) -> Type where
176+-- ------------------------------------------------- [ The Language of Effects ]
177+||| Definition of an Effect.
178+|||
179+||| @ m The computation context
180+||| @ x The return type of the result.
181+||| @ es The list of allowed side-effects.
182+||| @ ce Function to compute a new list of allowed side-effects.
183+data Eff : (m : Type -> Type)
184+ -> (x : Type)
185+ -> (es : List EFFECT)
186+ -> (ce : x -> List EFFECT) -> Type where
165187 value : a -> Eff m a xs (\v => xs)
166188 with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
167189 Eff m a xs xs'
@@ -192,7 +214,7 @@ data Eff : (m : Type -> Type) ->
192214return : a -> Eff m a xs (\v => xs)
193215return x = value x
194216
195−-- for idiom brackets
217+-- ------------------------------------------------------ [ for idiom brackets ]
196218
197219infixl 2 <$>
198220
@@ -207,7 +229,7 @@ syntax pureM [val] = with_val val (pure ())
207229 arg <- v
208230 return (fn arg)
209231
210−-- an interpreter
232+-- ---------------------------------------------------------- [ an interpreter ]
211233
212234private
213235execEff : Env m xs -> (p : EffElem e res xs) ->
@@ -276,6 +298,9 @@ new : Handler e m =>
276298 Eff m a xs (\v => xs')
277299new {r} e = newInit r e
278300
301+-- --------------------------------------------------------- [ Running Effects ]
302+
303+||| Run an effectful program
279304run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
280305run {env} prog = eff env prog (\r, env => pure r)
281306
@@ -295,7 +320,7 @@ runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
295320 m (x : a ** Env m (xs' x))
296321runEnv env prog = eff env prog (\r, env => pure (r ** env))
297322
298−-- some higher order things
323+-- ----------------------------------------------- [ some higher order things ]
299324
300325mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
301326mapE f [] = pure []
@@ -314,3 +339,4 @@ when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
314339when True e = e
315340when False e = pure ()
316341
342+-- --------------------------------------------------------------------- [ EOF ]