git.iko.soy/Idris-dev
on master help sign in
Trying a new Effects api
c3cdb9cEdwin Brady
libs/effects/Effect/Exception.idr+4−15
compare with master
unifiedsplit
@@ -4,8 +4,8 @@ import Effects
4import System
4import System
5import Control.IOExcept
5import Control.IOExcept
6
6
7−data Exception : Type -> Effect where
7+data Exception : Type -> Effect where
8− Raise : a -> { () } Exception a b
8+ Raise : a -> sig (Exception a) b
9
9
10instance Handler (Exception a) Maybe where
10instance Handler (Exception a) Maybe where
11 handle _ (Raise e) k = Nothing
11 handle _ (Raise e) k = Nothing
@@ -14,7 +14,7 @@ instance Handler (Exception a) List where
14 handle _ (Raise e) k = []
14 handle _ (Raise e) k = []
15
15
16instance Show a => Handler (Exception a) IO where
16instance Show a => Handler (Exception a) IO where
17− handle _ (Raise e) k = do printLn e
17+ handle _ (Raise e) k = do print e
18 believe_me (exit 1)
18 believe_me (exit 1)
19
19
20instance Handler (Exception a) (IOExcept a) where
20instance Handler (Exception a) (IOExcept a) where
@@ -26,16 +26,5 @@ instance Handler (Exception a) (Either a) where
26EXCEPTION : Type -> EFFECT
26EXCEPTION : Type -> EFFECT
27EXCEPTION t = MkEff () (Exception t)
27EXCEPTION t = MkEff () (Exception t)
28
28
29−raise : a -> { [EXCEPTION a ] } Eff b
29+raise : a -> Eff b [EXCEPTION a]
30raise err = call $ Raise err
30raise err = call $ Raise err
31−
32−
33−
34−
35−
36−
37−-- TODO: Catching exceptions mid program?
38−-- probably need to invoke a new interpreter
39−
40−-- possibly add a 'handle' to the Eff language so that an alternative
41−-- handler can be introduced mid interpretation?
libs/effects/Effect/File.idr+16−16
@@ -46,29 +46,29 @@ data FileIO : Effect where
46 ||| @ m The file mode.
46 ||| @ m The file mode.
47 Open : (fname: String)
47 Open : (fname: String)
48 -> (m : Mode)
48 -> (m : Mode)
49− -> {() ==> {res} if res
49+ -> sig FileIO Bool () (\res => case res of
50− then OpenFile m
50+ True => OpenFile m
51− else ()} FileIO Bool
51+ False => ())
52
52
53 ||| Close a file.
53 ||| Close a file.
54 |||
54 |||
55 ||| Closing a file moves the state from Open to closed.
55 ||| Closing a file moves the state from Open to closed.
56− Close : {OpenFile m ==> ()} FileIO ()
56+ Close : sig FileIO () (OpenFile m) ()
57
57
58 ||| Read a line from the file.
58 ||| Read a line from the file.
59 |||
59 |||
60 ||| Only files that are open for reading can be read.
60 ||| Only files that are open for reading can be read.
61− ReadLine : {OpenFile Read} FileIO String
61+ ReadLine : sig FileIO String (OpenFile Read)
62
62
63 ||| Write a string to a file.
63 ||| Write a string to a file.
64 |||
64 |||
65 ||| Only file that are open for writing can be written to.
65 ||| Only file that are open for writing can be written to.
66− WriteString : String -> {OpenFile Write} FileIO ()
66+ WriteString : String -> sig FileIO () (OpenFile Write)
67
67
68 ||| End of file?
68 ||| End of file?
69 |||
69 |||
70 ||| Only files open for reading can be tested for EOF
70 ||| Only files open for reading can be tested for EOF
71− EOF : {OpenFile Read} FileIO Bool
71+ EOF : sig FileIO Bool (OpenFile Read)
72
72
73-- ------------------------------------------------------------ [ The Handlers ]
73-- ------------------------------------------------------------ [ The Handlers ]
74
74
@@ -117,31 +117,31 @@ FILE_IO t = MkEff t FileIO
117||| @ m The file mode.
117||| @ m The file mode.
118open : (fname : String)
118open : (fname : String)
119 -> (m : Mode)
119 -> (m : Mode)
120− -> { [FILE_IO ()] ==> {result}
121− [FILE_IO (if result
122− then OpenFile m
123− else ())] } Eff Bool
120+ -> Eff Bool [FILE_IO ()]
121+ (\res => [FILE_IO (case res of
122+ True => OpenFile m
123+ False => ())])
124open f m = call $ Open f m
124open f m = call $ Open f m
125
125
126
126
127||| Close a file.
127||| Close a file.
128−close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()
128+close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
129close = call $ Close
129close = call $ Close
130
130
131||| Read a line from the file.
131||| Read a line from the file.
132−readLine : { [FILE_IO (OpenFile Read)] } Eff String
132+readLine : Eff String [FILE_IO (OpenFile Read)]
133readLine = call $ ReadLine
133readLine = call $ ReadLine
134
134
135||| Write a string to a file.
135||| Write a string to a file.
136−writeString : String -> { [FILE_IO (OpenFile Write)] } Eff ()
136+writeString : String -> Eff () [FILE_IO (OpenFile Write)]
137writeString str = call $ WriteString str
137writeString str = call $ WriteString str
138
138
139||| Write a line to a file.
139||| Write a line to a file.
140−writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()
140+writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
141writeLine str = call $ WriteString (str ++ "\n")
141writeLine str = call $ WriteString (str ++ "\n")
142
142
143||| End of file?
143||| End of file?
144−eof : { [FILE_IO (OpenFile Read)] } Eff Bool
144+eof : Eff Bool [FILE_IO (OpenFile Read)]
145eof = call $ EOF
145eof = call $ EOF
146
146
147-- --------------------------------------------------------------------- [ EOF ]
147-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Random.idr+12−13
@@ -5,28 +5,27 @@ import Data.Vect
5import Data.Fin
5import Data.Fin
6
6
7data Random : Effect where
7data Random : Effect where
8− getRandom : { Integer } Random Integer
8+ getRandom : sig Random Integer Integer
9− setSeed : Integer -> { Integer } Random ()
9+ setSeed : Integer -> sig Random () Integer
10
10
11−using (m : Type -> Type)
12− instance Handler Random m where
11+instance Handler Random m where
13− handle seed getRandom k
12+ handle seed getRandom k
14− = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
13+ = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
15− k seed' seed'
14+ k seed' seed'
16− handle seed (setSeed n) k = k () n
15+ handle seed (setSeed n) k = k () n
17
16
18RND : EFFECT
17RND : EFFECT
19RND = MkEff Integer Random
18RND = MkEff Integer Random
20
19
21||| Generates a random Integer in a given range
20||| Generates a random Integer in a given range
22−rndInt : Integer -> Integer -> { [RND] } Eff Integer
21+rndInt : Integer -> Integer -> Eff Integer [RND]
23rndInt lower upper = do v <- call $ getRandom
22rndInt lower upper = do v <- call $ getRandom
24 return ((v `prim__sremBigInt` (upper - lower)) + lower)
23 return ((v `prim__sremBigInt` (upper - lower)) + lower)
25
24
26||| Generate a random number in Fin (S `k`)
25||| Generate a random number in Fin (S `k`)
27|||
26|||
28||| Note that rndFin k takes values 0, 1, ..., k.
27||| Note that rndFin k takes values 0, 1, ..., k.
29−rndFin : (k : Nat) -> { [RND] } Eff (Fin (S k))
28+rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]
30rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))
29rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))
31 return (toFin v)
30 return (toFin v)
32 where toFin : Integer -> Fin (S k)
31 where toFin : Integer -> Fin (S k)
@@ -35,15 +34,15 @@ rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast
35 Nothing => toFin (assert_smaller x (x - cast (S k)))
34 Nothing => toFin (assert_smaller x (x - cast (S k)))
36
35
37||| Select a random element from a vector
36||| Select a random element from a vector
38−rndSelect' : Vect (S k) a -> { [RND] } Eff a
37+rndSelect' : Vect (S k) a -> Eff a [RND]
39rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
38rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
40
39
41||| Select a random element from a list, or Nothing if the list is empty
40||| Select a random element from a list, or Nothing if the list is empty
42−rndSelect : List a -> { [RND] } Eff (Maybe a)
41+rndSelect : List a -> Eff (Maybe a) [RND]
43rndSelect [] = return Nothing
42rndSelect [] = return Nothing
44rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
43rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
45
44
46||| Sets the random seed
45||| Sets the random seed
47−srand : Integer -> { [RND] } Eff ()
46+srand : Integer -> Eff () [RND]
48srand n = call $ setSeed n
47srand n = call $ setSeed n
49
48
libs/effects/Effect/Select.idr+2−2
@@ -3,7 +3,7 @@ module Effect.Select
3import Effects
3import Effects
4
4
5data Selection : Effect where
5data Selection : Effect where
6− Select : List a -> { () } Selection a
6+ Select : List a -> sig Selection a ()
7
7
8instance Handler Selection Maybe where
8instance Handler Selection Maybe where
9 handle _ (Select xs) k = tryAll xs where
9 handle _ (Select xs) k = tryAll xs where
@@ -18,6 +18,6 @@ instance Handler Selection List where
18SELECT : EFFECT
18SELECT : EFFECT
19SELECT = MkEff () Selection
19SELECT = MkEff () Selection
20
20
21−select : List a -> { [SELECT] } Eff a
21+select : List a -> Eff a [SELECT]
22select xs = call $ Select xs
22select xs = call $ Select xs
23
23
libs/effects/Effect/State.idr+8−8
@@ -5,8 +5,8 @@ import Effects
5%access public
5%access public
6
6
7data State : Effect where
7data State : Effect where
8− Get : { a } State a
8+ Get : sig State a a
9− Put : b -> { a ==> b } State ()
9+ Put : b -> sig State () a b
10
10
11-- using (m : Type -> Type)
11-- using (m : Type -> Type)
12instance Handler State m where
12instance Handler State m where
@@ -16,22 +16,22 @@ instance Handler State m where
16STATE : Type -> EFFECT
16STATE : Type -> EFFECT
17STATE t = MkEff t State
17STATE t = MkEff t State
18
18
19−get : { [STATE x] } Eff x
19+get : Eff x [STATE x]
20get = call $ Get
20get = call $ Get
21
21
22−put : x -> { [STATE x] } Eff ()
22+put : x -> Eff () [STATE x]
23put val = call $ Put val
23put val = call $ Put val
24
24
25−putM : y -> { [STATE x] ==> [STATE y] } Eff ()
25+putM : y -> Eff () [STATE x] [STATE y]
26putM val = call $ Put val
26putM val = call $ Put val
27
27
28−update : (x -> x) -> { [STATE x] } Eff ()
28+update : (x -> x) -> Eff () [STATE x]
29update f = put (f !get)
29update f = put (f !get)
30
30
31−updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff ()
31+updateM : (x -> y) -> Eff () [STATE x] [STATE y]
32updateM f = putM (f !get)
32updateM f = putM (f !get)
33
33
34−locally : x -> ({ [STATE x] } Eff t) -> { [STATE y] } Eff t
34+locally : x -> (Eff t [STATE x]) -> Eff t [STATE y]
35locally newst prog = do st <- get
35locally newst prog = do st <- get
36 putM newst
36 putM newst
37 val <- prog
37 val <- prog
libs/effects/Effect/StdIO.idr+13−24
@@ -9,10 +9,10 @@ import Control.IOExcept
9
9
10||| The internal representation of StdIO effects
10||| The internal representation of StdIO effects
11data StdIO : Effect where
11data StdIO : Effect where
12− PutStr : String -> { () } StdIO ()
12+ PutStr : String -> sig StdIO ()
13− GetStr : { () } StdIO String
13+ GetStr : sig StdIO String
14− PutCh : Char -> { () } StdIO ()
14+ PutCh : Char -> sig StdIO ()
15− GetCh : { () } StdIO Char
15+ GetCh : sig StdIO Char
16
16
17
17
18-------------------------------------------------------------
18-------------------------------------------------------------
@@ -22,13 +22,13 @@ data StdIO : Effect where
22instance Handler StdIO IO where
22instance Handler StdIO IO where
23 handle () (PutStr s) k = do putStr s; k () ()
23 handle () (PutStr s) k = do putStr s; k () ()
24 handle () GetStr k = do x <- getLine; k x ()
24 handle () GetStr k = do x <- getLine; k x ()
25− handle () (PutCh c) k = do putChar c; k () ()
25+ handle () (PutCh c) k = do putChar c; k () ()
26 handle () GetCh k = do x <- getChar; k x ()
26 handle () GetCh k = do x <- getChar; k x ()
27
27
28instance Handler StdIO (IOExcept a) where
28instance Handler StdIO (IOExcept a) where
29 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
29 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
30 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
30 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
31− handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
31+ handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
33
33
34-------------------------------------------------------------
34-------------------------------------------------------------
@@ -39,33 +39,22 @@ STDIO : EFFECT
39STDIO = MkEff () StdIO
39STDIO = MkEff () StdIO
40
40
41||| Write a string to standard output.
41||| Write a string to standard output.
42−putStr : String -> { [STDIO] } Eff ()
42+putStr : String -> Eff () [STDIO]
43putStr s = call $ PutStr s
43putStr s = call $ PutStr s
44
44
45−||| Write a string to standard output, terminating with a newline.
46−putStrLn : String -> { [STDIO] } Eff ()
47−putStrLn s = putStr (s ++ "\n")
48−
49||| Write a character to standard output.
45||| Write a character to standard output.
50−putChar : Char -> { [STDIO] } Eff ()
46+putChar : Char -> Eff () [STDIO]
51putChar c = call $ PutCh c
47putChar c = call $ PutCh c
52
48
53−||| Write a character to standard output, terminating with a newline.
49+||| Write a string to standard output, terminating with a newline.
54−putCharLn : Char -> { [STDIO] } Eff ()
50+putStrLn : String -> Eff () [STDIO]
55−putCharLn c = putStrLn (singleton c)
51+putStrLn s = putStr (s ++ "\n")
56
52
57||| Read a string from standard input.
53||| Read a string from standard input.
58−getStr : { [STDIO] } Eff String
54+getStr : Eff String [STDIO]
59getStr = call $ GetStr
55getStr = call $ GetStr
60
56
61||| Read a character from standard input.
57||| Read a character from standard input.
62−getChar : { [STDIO] } Eff Char
58+getChar : Eff Char [STDIO]
63getChar = call $ GetCh
59getChar = call $ GetCh
64
60
65−||| Given a parameter `a` 'show' `a` to standard output.
66−print : Show a => a -> { [STDIO] } Eff ()
67−print a = putStr (show a)
68−
69−||| Given a parameter `a` 'show' `a` to a standard output, terminating with a newline
70−printLn : Show a => a -> { [STDIO] } Eff ()
71−printLn a = putStrLn (show a)
libs/effects/Effect/System.idr+8−8
@@ -8,10 +8,10 @@ import System
8import Control.IOExcept
8import Control.IOExcept
9
9
10data System : Effect where
10data System : Effect where
11− Args : { () } System (List String)
11+ Args : sig System (List String)
12− Time : { () } System Int
12+ Time : sig System Int
13− GetEnv : String -> { () } System (Maybe String)
13+ GetEnv : String -> sig System (Maybe String)
14− CSystem : String -> { () } System Int
14+ CSystem : String -> sig System Int
15
15
16instance Handler System IO where
16instance Handler System IO where
17 handle () Args k = do x <- getArgs; k x ()
17 handle () Args k = do x <- getArgs; k x ()
@@ -30,14 +30,14 @@ instance Handler System (IOExcept a) where
30SYSTEM : EFFECT
30SYSTEM : EFFECT
31SYSTEM = MkEff () System
31SYSTEM = MkEff () System
32
32
33−getArgs : { [SYSTEM] } Eff (List String)
33+getArgs : Eff (List String) [SYSTEM]
34getArgs = call Args
34getArgs = call Args
35
35
36−time : { [SYSTEM] } Eff Int
36+time : Eff Int [SYSTEM]
37time = call Time
37time = call Time
38
38
39−getEnv : String -> { [SYSTEM] } Eff (Maybe String)
39+getEnv : String -> Eff (Maybe String) [SYSTEM]
40getEnv s = call $ GetEnv s
40getEnv s = call $ GetEnv s
41
41
42−system : String -> { [SYSTEM] } Eff Int
42+system : String -> Eff Int [SYSTEM]
43system s = call $ CSystem s
43system s = call $ CSystem s
libs/effects/Effects.idr+85−33
@@ -24,6 +24,27 @@ Effect = (x : Type) -> Type -> (x -> Type) -> Type
24data EFFECT : Type where
24data EFFECT : Type where
25 MkEff : Type -> Effect -> EFFECT
25 MkEff : Type -> Effect -> EFFECT
26
26
27+-- 'sig' gives the signature for an effect. There are three versions
28+-- depending on whether there is no state change, a non-dependent change,
29+-- or a dependent change. These are easily disambiguated by type.
30+
31+namespace NoResourceEffect
32+ sig : Effect -> Type -> Type
33+ sig e r = e r () (\v => ())
34+
35+namespace NoUpdateEffect
36+ sig : Effect -> (ret : Type) -> (resource : Type) -> Type
37+ sig e r e_in = e r e_in (\v => e_in)
38+
39+namespace UpdateEffect
40+ sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type
41+ sig e r e_in e_out = e r e_in (\v => e_out)
42+
43+namespace DepUpdateEffect
44+ sig : Effect ->
45+ (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
46+ sig e r e_in e_out = e r e_in e_out
47+
27||| Handler classes describe how an effect `e` is translated to the
48||| Handler classes describe how an effect `e` is translated to the
28||| underlying computation context `m` for execution.
49||| underlying computation context `m` for execution.
29class Handler (e : Effect) (m : Type -> Type) where
50class Handler (e : Effect) (m : Type -> Type) where
@@ -60,6 +81,7 @@ data SubList : List a -> List a -> Type where
60 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
81 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
61 Drop : SubList xs ys -> SubList xs (x :: ys)
82 Drop : SubList xs ys -> SubList xs (x :: ys)
62
83
84+%hint
63subListId : SubList xs xs
85subListId : SubList xs xs
64subListId {xs = Nil} = SubNil
86subListId {xs = Nil} = SubNil
65subListId {xs = x :: xs} = Keep subListId
87subListId {xs = x :: xs} = Keep subListId
@@ -133,26 +155,56 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
133||| @ x The return type of the result.
155||| @ x The return type of the result.
134||| @ es The list of allowed side-effects.
156||| @ es The list of allowed side-effects.
135||| @ ce Function to compute a new list of allowed side-effects.
157||| @ ce Function to compute a new list of allowed side-effects.
136−data Eff : (x : Type)
158+data EffM : (m : Type -> Type) -> (x : Type)
137− -> (es : List EFFECT)
159+ -> (es : List EFFECT)
138− -> (ce : x -> List EFFECT) -> Type where
160+ -> (ce : x -> List EFFECT) -> Type where
139− value : (val : a) -> Eff a (xs val) xs
161+ value : (val : a) -> EffM m a (xs val) xs
140− ebind : Eff a xs xs' ->
162+ ebind : EffM m a xs xs' ->
141− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
163+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
142 callP : (prf : EffElem e a xs) ->
164 callP : (prf : EffElem e a xs) ->
143 (eff : e t a b) ->
165 (eff : e t a b) ->
144− Eff t xs (\v => updateResTy v xs prf eff)
166+ EffM m t xs (\v => updateResTy v xs prf eff)
145
167
146 liftP : (prf : SubList ys xs) ->
168 liftP : (prf : SubList ys xs) ->
147− Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
169+ EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
148
170
149 (:-) : (l : ty) ->
171 (:-) : (l : ty) ->
150− Eff t [x] xs' -> -- [x] (\v => xs) ->
172+ EffM m t [x] xs' -> -- [x] (\v => xs) ->
151− Eff t [l ::: x] (\v => map (l :::) (xs' v))
173+ EffM m t [l ::: x] (\v => map (l :::) (xs' v))
174+
175+-- Some type synonyms, so we don't always have to write EffM in full
176+
177+namespace SimpleEff
178+ -- Simple effects, no updates
179+ Eff : (x : Type) -> (es : List EFFECT) -> Type
180+ Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
181+
182+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type
183+ EffT m x es = EffM m x es (\v => es)
184+
185+namespace TransEff
186+ -- Dependent effects, updates not dependent on result
187+ Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
188+ Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
189+
190+ EffT : (m : Type -> Type) ->
191+ (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
192+ EffT m x es ce = EffM m x es (\_ => ce)
193+
194+namespace DepEff
195+ -- Dependent effects, updates dependent on result
196+ Eff : (x : Type) -> (es : List EFFECT)
197+ -> (ce : x -> List EFFECT) -> Type
198+ Eff x es ce = {m : Type -> Type} -> EffM m x es ce
199+
200+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
201+ -> (ce : x -> List EFFECT) -> Type
202+ EffT m x es ce = EffM m x es ce
203+
152
204
153%no_implicit
205%no_implicit
154−(>>=) : Eff a xs xs' ->
206+(>>=) : EffM m a xs xs' ->
155− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
207+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
156(>>=) = ebind
208(>>=) = ebind
157
209
158-- namespace SimpleBind
210-- namespace SimpleBind
@@ -161,29 +213,29 @@ data Eff : (x : Type)
161-- (>>=) = ebind
213-- (>>=) = ebind
162
214
163||| Run a subprogram which results in an effect state the same as the input.
215||| Run a subprogram which results in an effect state the same as the input.
164−staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
216+staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)
165staticEff = id
217staticEff = id
166
218
167||| Explicitly give the expected set of result effects for an effectful
219||| Explicitly give the expected set of result effects for an effectful
168||| operation.
220||| operation.
169−toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
221+toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
170toEff xs' = id
222toEff xs' = id
171
223
172−return : a -> Eff a xs (\v => xs)
224+return : a -> EffM m a xs (\v => xs)
173return x = value x
225return x = value x
174
226
175-- ------------------------------------------------------ [ for idiom brackets ]
227-- ------------------------------------------------------ [ for idiom brackets ]
176
228
177infixl 2 <*>
229infixl 2 <*>
178
230
179−pure : a -> Eff a xs (\v => xs)
231+pure : a -> EffM m a xs (\v => xs)
180pure = value
232pure = value
181
233
182−pureM : (val : a) -> Eff a (xs val) xs
234+pureM : (val : a) -> EffM m a (xs val) xs
183pureM = value
235pureM = value
184
236
185−(<*>) : Eff (a -> b) xs (\v => xs) ->
237+(<*>) : EffM m (a -> b) xs (\v => xs) ->
186− Eff a xs (\v => xs) -> Eff b xs (\v => xs)
238+ EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
187(<*>) prog v = do fn <- prog
239(<*>) prog v = do fn <- prog
188 arg <- v
240 arg <- v
189 return (fn arg)
241 return (fn arg)
@@ -203,7 +255,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
203-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
255-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
204-- updates can be propagated even through failing computations?
256-- updates can be propagated even through failing computations?
205
257
206−eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
258+eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
207eff env (value x) k = k x env
259eff env (value x) k = k x env
208eff env (prog `ebind` c) k
260eff env (prog `ebind` c) k
209 = eff env prog (\p', env' => eff env' (c p') k)
261 = eff env prog (\p', env' => eff env' (c p') k)
@@ -235,14 +287,14 @@ call : {a, b: _} -> {e : Effect} ->
235 (eff : e t a b) ->
287 (eff : e t a b) ->
236 {default tactics { search 100; }
288 {default tactics { search 100; }
237 prf : EffElem e a xs} ->
289 prf : EffElem e a xs} ->
238− Eff t xs (\v => updateResTy v xs prf eff)
290+ EffM m t xs (\v => updateResTy v xs prf eff)
239call e {prf} = callP prf e
291call e {prf} = callP prf e
240
292
241implicit
293implicit
242−lift : Eff t ys ys' ->
294+lift : EffM m t ys ys' ->
243 {default tactics { search 100; }
295 {default tactics { search 100; }
244 prf : SubList ys xs} ->
296 prf : SubList ys xs} ->
245− Eff t xs (\v => updateWith (ys' v) xs prf)
297+ EffM m t xs (\v => updateWith (ys' v) xs prf)
246lift e {prf} = liftP prf e
298lift e {prf} = liftP prf e
247
299
248
300
@@ -255,7 +307,7 @@ lift e {prf} = liftP prf e
255|||
307|||
256||| @prog The effectful program to run.
308||| @prog The effectful program to run.
257run : Applicative m => {default MkDefaultEnv env : Env m xs}
309run : Applicative m => {default MkDefaultEnv env : Env m xs}
258− -> (prog : Eff a xs xs') -> m a
310+ -> (prog : EffM m a xs xs') -> m a
259run {env} prog = eff env prog (\r, env => pure r)
311run {env} prog = eff env prog (\r, env => pure r)
260
312
261||| Run an effectful program in the identity context.
313||| Run an effectful program in the identity context.
@@ -264,7 +316,7 @@ run {env} prog = eff env prog (\r, env => pure r)
264||| The `env` argument is implicit and initialised automatically.
316||| The `env` argument is implicit and initialised automatically.
265|||
317|||
266||| @prog The effectful program to run.
318||| @prog The effectful program to run.
267−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a
319+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : EffM id a xs xs') -> a
268runPure {env} prog = eff env prog (\r, env => r)
320runPure {env} prog = eff env prog (\r, env => r)
269
321
270||| Run an effectful program in a given context `m` with a default value for the environment.
322||| Run an effectful program in a given context `m` with a default value for the environment.
@@ -273,7 +325,7 @@ runPure {env} prog = eff env prog (\r, env => r)
273|||
325|||
274||| @env The environment to use.
326||| @env The environment to use.
275||| @prog The effectful program to run.
327||| @prog The effectful program to run.
276−runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a
328+runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a
277runInit env prog = eff env prog (\r, env => pure r)
329runInit env prog = eff env prog (\r, env => pure r)
278
330
279||| Run an effectful program with a given default value for the environment.
331||| Run an effectful program with a given default value for the environment.
@@ -282,31 +334,31 @@ runInit env prog = eff env prog (\r, env => pure r)
282|||
334|||
283||| @env The environment to use.
335||| @env The environment to use.
284||| @prog The effectful program to run.
336||| @prog The effectful program to run.
285−runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a
337+runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a
286runPureInit env prog = eff env prog (\r, env => r)
338runPureInit env prog = eff env prog (\r, env => r)
287
339
288−runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
340+runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
289runWith inj env prog = eff env prog (\r, env => inj r)
341runWith inj env prog = eff env prog (\r, env => inj r)
290
342
291−runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
343+runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
292 m (x : a ** Env m (xs' x))
344 m (x : a ** Env m (xs' x))
293runEnv env prog = eff env prog (\r, env => pure (r ** env))
345runEnv env prog = eff env prog (\r, env => pure (r ** env))
294
346
295-- ----------------------------------------------- [ some higher order things ]
347-- ----------------------------------------------- [ some higher order things ]
296
348
297−mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
349+mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)
298mapE f [] = pure []
350mapE f [] = pure []
299mapE f (x :: xs) = [| f x :: mapE f xs |]
351mapE f (x :: xs) = [| f x :: mapE f xs |]
300
352
301
353
302−mapVE : (a -> {xs} Eff b) ->
354+mapVE : (a -> {xs} EffM m b) ->
303 Vect n a ->
355 Vect n a ->
304− {xs} Eff (Vect n b)
356+ {xs} EffM m (Vect n b)
305mapVE f [] = pure []
357mapVE f [] = pure []
306mapVE f (x :: xs) = [| f x :: mapVE f xs |]
358mapVE f (x :: xs) = [| f x :: mapVE f xs |]
307
359
308
360
309−when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
361+when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()
310when True e = Force e
362when True e = Force e
311when False e = pure ()
363when False e = pure ()
312
364
test/effects001/test021.idr+1−2
@@ -9,8 +9,7 @@ import Control.IOExcept
9data Count : Type where
9data Count : Type where
10
10
11FileIO : Type -> Type -> Type
11FileIO : Type -> Type -> Type
12−FileIO st t
13− = { [FILE_IO st, STDIO, Count ::: STATE Int] } Eff t
12+FileIO st t = Eff t [FILE_IO st, STDIO, Count ::: STATE Int]
14
13
15readFile : FileIO (OpenFile Read) (List String)
14readFile : FileIO (OpenFile Read) (List String)
16readFile = readAcc [] where
15readFile = readAcc [] where
test/effects001/test021a.idr+1−1
@@ -18,7 +18,7 @@ Env = List (String, Integer)
18-- Evaluator t
18-- Evaluator t
19-- = Eff m [EXCEPTION String, RND, STATE Env] t
19-- = Eff m [EXCEPTION String, RND, STATE Env] t
20
20
21−eval : Expr -> { [EXCEPTION String, STDIO, RND, STATE Env] } Eff Integer
21+eval : Expr -> Eff Integer [EXCEPTION String, STDIO, RND, STATE Env]
22eval (Var x) = do vs <- get
22eval (Var x) = do vs <- get
23 case lookup x vs of
23 case lookup x vs of
24 Nothing => raise ("No such variable " ++ x)
24 Nothing => raise ("No such variable " ++ x)
test/effects002/test025.idr+2−2
@@ -6,8 +6,8 @@ import Control.IOExcept
6import Data.Vect
6import Data.Vect
7
7
8MemoryIO : Type -> Type -> Type -> Type
8MemoryIO : Type -> Type -> Type -> Type
9−MemoryIO td ts r = { [ Dst ::: RAW_MEMORY td
9+MemoryIO td ts r = Eff r [Dst ::: RAW_MEMORY td,
10− , Src ::: RAW_MEMORY ts ] } Eff r
10+ Src ::: RAW_MEMORY ts]
11
11
12inpVect : Vect 5 Bits8
12inpVect : Vect 5 Bits8
13inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]
13inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]
test/effects003/hangman.idr+28−26
@@ -74,55 +74,59 @@ data HangmanRules : Effect where
74-- the number of missing letters, if not, reduce the number of guesses left
74-- the number of missing letters, if not, reduce the number of guesses left
75
75
76 Guess : (x : Char) ->
76 Guess : (x : Char) ->
77+ sig HangmanRules Bool
77− { Hangman (Running (S g) (S w)) ==>
78+ (Hangman (Running (S g) (S w)))
79+ (\inword =>
78− {inword} (case inword of
80+ case inword of
79 True => Hangman (Running (S g) w)
81 True => Hangman (Running (S g) w)
80− False => Hangman (Running g (S w))) }
82+ False => Hangman (Running g (S w)))
81− HangmanRules Bool
82
83
83-- The 'Won' operation requires that there are no missing letters
84-- The 'Won' operation requires that there are no missing letters
84
85
86+ Won : sig HangmanRules ()
87+ (Hangman (Running g 0))
85− Won : { Hangman (Running g 0) ==> Hangman NotRunning } HangmanRules ()
88+ (Hangman NotRunning)
86
89
87-- The 'Lost' operation requires that there are no guesses left
90-- The 'Lost' operation requires that there are no guesses left
88
91
92+ Lost : sig HangmanRules ()
93+ (Hangman (Running 0 g))
89− Lost : { Hangman (Running 0 g) ==> Hangman NotRunning } HangmanRules ()
94+ (Hangman NotRunning)
90
95
91-- Set up a new game, initialised with 6 guesses and the missing letters in
96-- Set up a new game, initialised with 6 guesses and the missing letters in
92-- the given word. Note that if there are no letters in the word, we won't
97-- the given word. Note that if there are no letters in the word, we won't
93-- be able to run 'Guess'!
98-- be able to run 'Guess'!
94
99
95 NewWord : (w : String) ->
100 NewWord : (w : String) ->
96− { h ==> Hangman (Running 6 (length (letters w))) } HangmanRules ()
101+ sig HangmanRules () h (Hangman (Running 6 (length (letters w))))
97
102
98-- Finally, allow us to get the current game state
103-- Finally, allow us to get the current game state
99
104
100− Get : { h } HangmanRules h
105+ Get : sig HangmanRules h h
101
106
102HANGMAN : HState -> EFFECT
107HANGMAN : HState -> EFFECT
103HANGMAN h = MkEff (Hangman h) HangmanRules
108HANGMAN h = MkEff (Hangman h) HangmanRules
104
109
105-- Promote explicit effecst to Eff programs
110-- Promote explicit effecst to Eff programs
106
111
107−guess : Char ->
112+guess : Char -> Eff Bool
108− { [HANGMAN (Running (S g) (S w))] ==>
113+ [HANGMAN (Running (S g) (S w))]
109− {inword} [HANGMAN (case inword of
114+ (\inword => [HANGMAN (case inword of
110− True => Running (S g) w
115+ True => Running (S g) w
111− False => Running g (S w))] } Eff Bool
116+ False => Running g (S w))])
112guess c = call (Main.Guess c)
117guess c = call (Main.Guess c)
113
118
114−won : { [HANGMAN (Running g 0)] ==> [HANGMAN NotRunning]} Eff ()
119+won : Eff () [HANGMAN (Running g 0)] [HANGMAN NotRunning]
115won = call Won
120won = call Won
116
121
117−lost : { [HANGMAN (Running 0 g)] ==> [HANGMAN NotRunning]} Eff ()
122+lost : Eff () [HANGMAN (Running 0 g)] [HANGMAN NotRunning]
118lost = call Lost
123lost = call Lost
119
124
120−new_word : (w : String) ->
125+new_word : (w : String) -> Eff () [HANGMAN h]
121− { [HANGMAN h] ==>
122− [HANGMAN (Running 6 (length (letters w)))]} Eff ()
126+ [HANGMAN (Running 6 (length (letters w)))]
123new_word w = call (NewWord w)
127new_word w = call (NewWord w)
124
128
125−get : { [HANGMAN h] } Eff (Hangman h)
129+get : Eff (Hangman h) [HANGMAN h]
126get = call Get
130get = call Get
127
131
128-----------------------------------------------------------------------
132-----------------------------------------------------------------------
@@ -163,8 +167,8 @@ were valid letters in it!
163soRefl : So x -> (x = True)
167soRefl : So x -> (x = True)
164soRefl Oh = Refl
168soRefl Oh = Refl
165
169
166−game : { [HANGMAN (Running (S g) w), STDIO] ==>
170+game : Eff () [HANGMAN (Running (S g) w), STDIO]
167− [HANGMAN NotRunning, STDIO] } Eff ()
171+ [HANGMAN NotRunning, STDIO]
168game {w=Z} = won
172game {w=Z} = won
169game {w=S _}
173game {w=S _}
170 = do putStrLn (show !get)
174 = do putStrLn (show !get)
@@ -175,10 +179,8 @@ game {w=S _}
175 (Right p) => do putStrLn "Invalid input!"
179 (Right p) => do putStrLn "Invalid input!"
176 game
180 game
177 where
181 where
178− processGuess : -- {g,w:_} ->
179− Char -> { [HANGMAN (Running (S g) (S w)), STDIO] ==>
182+ processGuess : Char -> Eff () [HANGMAN (Running (S g) (S w)), STDIO]
180− [HANGMAN NotRunning, STDIO] }
183+ [HANGMAN NotRunning, STDIO]
181− Eff ()
182 processGuess {g} c {w}
184 processGuess {g} c {w}
183 = case !(guess c) of
185 = case !(guess c) of
184 True => do putStrLn "Good guess!"
186 True => do putStrLn "Good guess!"
@@ -203,7 +205,7 @@ wlen = proof search
203
205
204{- It typechecks! Ship it! -}
206{- It typechecks! Ship it! -}
205
207
206−runGame : { [HANGMAN NotRunning, RND, STDIO] } Eff ()
208+runGame : Eff () [HANGMAN NotRunning, RND, STDIO]
207runGame = do srand 1234567890
209runGame = do srand 1234567890
208 let w = index !(rndFin _) words
210 let w = index !(rndFin _) words
209 new_word w
211 new_word w