@@ -4,35 +4,57 @@ import Language.Reflection
4import Control.Catchable
4import Control.Catchable
5import Effect.Default
5import Effect.Default
7−%access public
7+--- Effectful computations are described as algebraic data types that
8−
8+--- explain how an effect is interpreted in some underlying context.
11+-- ----------------------------------------------------------------- [ Effects ]
12+||| The Effect type describes effectful computations.
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.
11Effect : Type
18Effect : Type
12Effect = (x : Type) -> Type -> (x -> Type) -> Type
19Effect = (x : Type) -> Type -> (x -> Type) -> Type
21+||| The `EFFECT` Data type describes how to promote the Effect
22+||| description into a concrete effect.
14%error_reverse
23%error_reverse
15data EFFECT : Type where
24data EFFECT : Type where
16 MkEff : Type -> Effect -> EFFECT
25 MkEff : Type -> Effect -> EFFECT
27+||| Handler classes describe how an effect `e` is translated to the
28+||| underlying computation context `m` for execution.
18class Handler (e : Effect) (m : Type -> Type) where
29class Handler (e : Effect) (m : Type -> Type) where
30+ ||| How to handle the effect.
32+ ||| @ r The resource being handled.
33+ ||| @ eff The effect to be applied.
34+ ||| @ ctxt The context in which to handle the effect.
19− handle : res -> (eff : e t res resk) ->
35+ handle : (r : res) -> (eff : e t res resk) ->
20− ((x : t) -> resk x -> m a) -> m a
36+ (ctxt : ((x : t) -> resk x -> m a)) -> m a
22−-- Get the resource type (handy at the REPL to find out about an effect)
38+||| Get the resource type (handy at the REPL to find out about an effect)
23resourceType : EFFECT -> Type
39resourceType : EFFECT -> Type
24resourceType (MkEff t e) = t
40resourceType (MkEff t e) = t
42+-- --------------------------------------------------------- [ Syntactic Sugar ]
26-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
44-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
27-- up to a small number of parameters...)
45-- up to a small number of parameters...)
47+-- No state transition
29syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
48syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
50+-- The state transition is dependent on a result `b`, a bound variable.
30syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
51syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
31 = eff inst (\b => outst)
52 = eff inst (\b => outst)
32−syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
34−---- Properties and proof construction
54+--- A simple state transition
55+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
57+-- --------------------------------------- [ Properties and Proof Construction ]
36using (xs : List a, ys : List a)
58using (xs : List a, ys : List a)
37 data SubList : List a -> List a -> Type where
59 data SubList : List a -> List a -> Type where
38 SubNil : SubList {a} [] []
60 SubNil : SubList {a} [] []
@@ -53,7 +75,7 @@ data EffElem : Effect -> Type ->
53 Here : EffElem x a (MkEff a x :: xs)
75 Here : EffElem x a (MkEff a x :: xs)
54 There : EffElem x a xs -> EffElem x a (y :: xs)
76 There : EffElem x a xs -> EffElem x a (y :: xs)
56−-- make an environment corresponding to a sub-list
78+||| make an environment corresponding to a sub-list
57dropEnv : Env m ys -> SubList xs ys -> Env m xs
79dropEnv : Env m ys -> SubList xs ys -> Env m xs
58dropEnv [] SubNil = []
80dropEnv [] SubNil = []
59dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
81dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
@@ -67,7 +89,7 @@ updateWith [] [] SubNil = []
67updateWith (y :: ys) [] SubNil = y :: ys
89updateWith (y :: ys) [] SubNil = y :: ys
68updateWith [] (x :: xs) (Keep rest) = []
90updateWith [] (x :: xs) (Keep rest) = []
70−-- put things back, replacing old with new in the sub-environment
92+||| Put things back, replacing old with new in the sub-environment
71rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
93rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
72 Env m xs -> Env m (updateWith ys' xs prf)
94 Env m xs -> Env m (updateWith ys' xs prf)
73rebuildEnv [] SubNil env = env
95rebuildEnv [] SubNil env = env
@@ -75,8 +97,7 @@ rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
75rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
97rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
76rebuildEnv (x :: xs) SubNil [] = x :: xs
98rebuildEnv (x :: xs) SubNil [] = x :: xs
78−---- The Effect EDSL itself ----
100+-- -------------------------------------------------- [ The Effect EDSL itself ]
80-- some proof automation
101-- some proof automation
82%reflection
103%reflection
@@ -131,11 +152,6 @@ updateResTy : (val : t) ->
131updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
152updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
132updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
153updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
134−-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
136−-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
137−-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
139infix 5 :::, :-, :=
155infix 5 :::, :-, :=
141data LRes : lbl -> Type -> Type where
157data LRes : lbl -> Type -> Type where
@@ -157,11 +173,17 @@ relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
157relabel {xs = []} l [] = []
173relabel {xs = []} l [] = []
158relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
174relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
160−-- the language of Effects
176+-- ------------------------------------------------- [ The Language of Effects ]
161−
177+||| Definition of an Effect.
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.
162−data Eff : (m : Type -> Type) ->
183+data Eff : (m : Type -> Type)
163− (x : Type) ->
184+ -> (x : Type)
185+ -> (es : List EFFECT)
164− List EFFECT -> (x -> List EFFECT) -> Type where
186+ -> (ce : x -> List EFFECT) -> Type where
165 value : a -> Eff m a xs (\v => xs)
187 value : a -> Eff m a xs (\v => xs)
166 with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
188 with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
167 Eff m a xs xs'
189 Eff m a xs xs'
@@ -192,7 +214,7 @@ data Eff : (m : Type -> Type) ->
192return : a -> Eff m a xs (\v => xs)
214return : a -> Eff m a xs (\v => xs)
193return x = value x
215return x = value x
195−-- for idiom brackets
217+-- ------------------------------------------------------ [ for idiom brackets ]
197infixl 2 <$>
219infixl 2 <$>
@@ -207,7 +229,7 @@ syntax pureM [val] = with_val val (pure ())
208 return (fn arg)
230 return (fn arg)
210−-- an interpreter
232+-- ---------------------------------------------------------- [ an interpreter ]
213execEff : Env m xs -> (p : EffElem e res xs) ->
235execEff : Env m xs -> (p : EffElem e res xs) ->
@@ -276,6 +298,9 @@ new : Handler e m =>
276 Eff m a xs (\v => xs')
298 Eff m a xs (\v => xs')
277new {r} e = newInit r e
299new {r} e = newInit r e
301+-- --------------------------------------------------------- [ Running Effects ]
303+||| Run an effectful program
279run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
304run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
280run {env} prog = eff env prog (\r, env => pure r)
305run {env} prog = eff env prog (\r, env => pure r)
@@ -295,7 +320,7 @@ runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
295 m (x : a ** Env m (xs' x))
320 m (x : a ** Env m (xs' x))
296runEnv env prog = eff env prog (\r, env => pure (r ** env))
321runEnv env prog = eff env prog (\r, env => pure (r ** env))
298−-- some higher order things
323+-- ----------------------------------------------- [ some higher order things ]
300mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
325mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
301mapE f [] = pure []
326mapE f [] = pure []
@@ -314,3 +339,4 @@ when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
314when True e = e
339when True e = e
315when False e = pure ()
340when False e = pure ()
342+-- --------------------------------------------------------------------- [ EOF ]