@@ -20,7 +20,7 @@ EXCEPTION
2020
2121 EXCEPTION : Type -> EFFECT
2222
23− raise : a -> { [EXCEPTION a ] } Eff m b
23+ raise : a -> Eff b [EXCEPTION a]
2424
2525 instance Handler (Exception a) Maybe
2626 instance Handler (Exception a) List
@@ -42,18 +42,17 @@ FILE\_IO
4242
4343 data OpenFile : Mode -> Type
4444
45− open : Handler FileIO e => String -> (m : Mode) ->
46− { [FILE_IO ()] ==>
47− {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff e Bool
48− close : Handler FileIO e =>
49− { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
45+ open : (fname : String)
46+ -> (m : Mode)
47+ -> Eff Bool [FILE_IO ()]
48+ (\res => [FILE_IO (case res of
49+ True => OpenFile m
50+ False => ())])
51+ close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
5052
51− readLine : Handler FileIO e =>
52− { [FILE_IO (OpenFile Read)] } Eff e String
53− writeLine : Handler FileIO e => String ->
54− { [FILE_IO (OpenFile Write)] } Eff e ()
55− eof : Handler FileIO e =>
56− { [FILE_IO (OpenFile Read)] } Eff e Bool
53+ readLine : Eff String [FILE_IO (OpenFile Read)]
54+ writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
55+ eof : Eff Bool [FILE_IO (OpenFile Read)]
5756
5857 instance Handler FileIO IO
5958
@@ -70,9 +69,9 @@ RND
7069
7170 RND : EFFECT
7271
73− srand : Integer -> { [RND] } Eff m ()
74− rndInt : Integer -> Integer -> { [RND] } Eff m Integer
75− rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
72+ srand : Integer -> Eff m () [RND]
73+ rndInt : Integer -> Integer -> Eff m Integer [RND]
74+ rndFin : (k : Nat) -> Eff m (Fin (S k)) [RND]
7675
7776 instance Handler Random m
7877
@@ -87,7 +86,7 @@ SELECT
8786
8887 SELECT : EFFECT
8988
90− select : List a -> { [SELECT] } Eff m a
89+ select : List a -> Eff m a [SELECT]
9190
9291 instance Handler Selection Maybe
9392 instance Handler Selection List
@@ -103,10 +102,10 @@ STATE
103102
104103 STATE : Type -> EFFECT
105104
106− get : { [STATE x] } Eff m x
107− put : x -> { [STATE x] } Eff m ()
108− putM : y -> { [STATE x] ==> [STATE y] } Eff m ()
109− update : (x -> x) -> { [STATE x] } Eff m ()
105+ get : Eff m x [STATE x]
106+ put : x -> Eff m () [STATE x]
107+ putM : y -> Eff m () [STATE x] [STATE y]
108+ update : (x -> x) -> Eff m () [STATE x]
110109
111110 instance Handler State m
112111
@@ -122,12 +121,12 @@ STDIO
122121
123122 STDIO : EFFECT
124123
125− putChar : Handler StdIO m => Char -> { [STDIO] } Eff m ()
126− putStr : Handler StdIO m => String -> { [STDIO] } Eff m ()
127− putStrLn : Handler StdIO m => String -> { [STDIO] } Eff m ()
124+ putChar : Handler StdIO m => Char -> Eff m () [STDIO]
125+ putStr : Handler StdIO m => String -> Eff m () [STDIO]
126+ putStrLn : Handler StdIO m => String -> Eff m () [STDIO]
128127
129− getStr : Handler StdIO m => { [STDIO] } Eff m String
130− getChar : Handler StdIO m => { [STDIO] } Eff m Char
128+ getStr : Handler StdIO m => Eff m String [STDIO]
129+ getChar : Handler StdIO m => Eff m Char [STDIO]
131130
132131 instance Handler StdIO IO
133132 instance Handler StdIO (IOExcept a)
@@ -145,9 +144,9 @@ SYSTEM
145144
146145 SYSTEM : EFFECT
147146
148− getArgs : Handler System e => { [SYSTEM] } Eff e (List String)
149− time : Handler System e => { [SYSTEM] } Eff e Int
150− getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)
147+ getArgs : Handler System e => Eff e (List String) [SYSTEM]
148+ time : Handler System e => Eff e Int [SYSTEM]
149+ getEnv : Handler System e => String -> Eff e (Maybe String) [SYSTEM]
151150
152151 instance Handler System IO
153152 instance Handler System (IOExcept a)