git.iko.soy/Idris-dev
on master help sign in
No need for Handler constraints on effectful ops

They are required on 'run' anyway - having them on the functions here does no more than add noise to the type.

commit34d6f394e4412e0ef40f8024a417bca700577df4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 4 Jun 2014, 17:20 (12 years ago) parenta75bd0f
2 files changed+10−15
compare with master
unifiedsplit
libs/effects/Effect/File.idr+5−10 libs/effects/Effect/StdIO.idr+5−5
libs/effects/Effect/File.idr+5−10
@@ -101,8 +101,7 @@ FILE_IO t = MkEff t FileIO
101101|||
102102||| @ fname The file name to be opened.
103103||| @ m The file mode.
104−open : Handler FileIO e =>
105− (fname : String)
104+open : (fname : String)
106105 -> (m : Mode)
107106 -> { [FILE_IO ()] ==> [FILE_IO (if result
108107 then OpenFile m
@@ -111,23 +110,19 @@ open f m = call $ Open f m
111110
112111
113112||| Close a file.
114−close : Handler FileIO e =>
115− { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
113+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
116114close = call $ Close
117115
118116||| Read a line from the file.
119−readLine : Handler FileIO e =>
120− { [FILE_IO (OpenFile Read)] } Eff e String
117+readLine : { [FILE_IO (OpenFile Read)] } Eff e String
121118readLine = call $ ReadLine
122119
123120||| Write a line to a file.
124−writeLine : Handler FileIO e =>
125− String -> { [FILE_IO (OpenFile Write)] } Eff e ()
121+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e ()
126122writeLine str = call $ WriteLine str
127123
128124||| End of file?
129−eof : Handler FileIO e =>
130− { [FILE_IO (OpenFile Read)] } Eff e Bool
125+eof : { [FILE_IO (OpenFile Read)] } Eff e Bool
131126eof = call $ EOF
132127
133128-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/StdIO.idr+5−5
@@ -39,22 +39,22 @@ STDIO : EFFECT
3939STDIO = MkEff () StdIO
4040
4141||| Write a string to standard output.
42−putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
42+putStr : String -> { [STDIO] } Eff e ()
4343putStr s = call $ PutStr s
4444
4545||| Write a character to standard output.
46−putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
46+putChar : Char -> { [STDIO] } Eff e ()
4747putChar c = call $ PutCh c
4848
4949||| Write a string to standard output, terminating with a newline.
50−putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
50+putStrLn : String -> { [STDIO] } Eff e ()
5151putStrLn s = putStr (s ++ "\n")
5252
5353||| Read a string from standard input.
54−getStr : Handler StdIO e => { [STDIO] } Eff e String
54+getStr : { [STDIO] } Eff e String
5555getStr = call $ GetStr
5656
5757||| Read a character from standard input.
58−getChar : Handler StdIO e => { [STDIO] } Eff e Char
58+getChar : { [STDIO] } Eff e Char
5959getChar = call $ GetCh
6060