b0a55aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4784 from buzden/effects-tutorial-fix

Effects tutorial fix and additon of small clarification

commitb0a55aabbd49217711aa89367d2a672251dec530 authorNiklas Larsson <metaniklas@gmail.com> dateMon 25 Nov 2019, 14:44 (7 years ago) parent7d34ebc b41b8c6

2 files changed+39−30

compare with master

unifiedsplit

docs/effects/depeff.rst+16−7 docs/effects/summary.rst+23−23

docs/effects/depeff.rst+16−7

@@ -153,12 +153,21 @@ file management follows a resource usage protocol with the following

153153

154154- When a file is closed, its handle should no longer be used

155155

156−These requirements can be expressed formally in , by creating a

156+These requirements can be expressed formally by creating a

157157``FILE_IO`` effect parameterised over a file handle state, which is

158158either empty, open for reading, or open for writing. The ``FILE_IO``

159−effect’s definition is given below. Note that this

160−effect is mainly for illustrative purposes—typically we would also like

161−to support random access files and better reporting of error conditions.

159+effect’s definition is given below.

160+

161+.. note::

162+ This effect is mainly for illustrative purposes.

163+ Typically we would also like to support random access files and

164+ better reporting of error conditions.

165+

166+ Moreover, the ``FILE`` effect in the ``Effect.File`` module of

167+ the ``effects`` library uses slightly more complicated types to

168+ support erroneous behaviour of each function and to support more

169+ compilcated modes of opening, like for reading **and** writing,

170+ appending or truncating.

162171

163172.. code-block:: idris

164173

@@ -173,7 +182,7 @@ to support random access files and better reporting of error conditions.

173182

174183 open : (fname : String)

175184 -> (m : Mode)

176− -> Eff Bool [FILE_IO ()]

185+ -> Eff Bool [FILE_IO ()]

177186 (\res => [FILE_IO (case res of

178187 True => OpenFile m

179188 False => ())])

@@ -191,7 +200,7 @@ In particular, consider the type of ``open``:

191200

192201 open : (fname : String)

193202 -> (m : Mode)

194− -> Eff Bool [FILE_IO ()]

203+ -> Eff Bool [FILE_IO ()]

195204 (\res => [FILE_IO (case res of

196205 True => OpenFile m

197206 False => ())])

@@ -207,7 +216,7 @@ we continue the protocol accordingly.

207216

208217 readFile : Eff (List String) [FILE_IO (OpenFile Read)]

209218 readFile = readAcc [] where

210− readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]

219+ readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]

211220 readAcc acc = if (not !eof)

212221 then readAcc (!readLine :: acc)

213222 else pure (reverse acc)

docs/effects/summary.rst+23−23

@@ -43,16 +43,16 @@ FILE\_IO

4343 data OpenFile : Mode -> Type

4444

4545 open : (fname : String)

46− -> (m : Mode)

47− -> Eff Bool [FILE_IO ()]

48− (\res => [FILE_IO (case res of

49− True => OpenFile m

50− False => ())])

46+ -> (m : Mode)

47+ -> Eff Bool [FILE_IO ()]

48+ (\res => [FILE_IO (case res of

49+ True => OpenFile m

50+ False => ())])

5151 close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]

5252

53− readLine : Eff String [FILE_IO (OpenFile Read)]

53+ readLine : Eff String [FILE_IO (OpenFile Read)]

5454 writeLine : String -> Eff () [FILE_IO (OpenFile Write)]

55− eof : Eff Bool [FILE_IO (OpenFile Read)]

55+ eof : Eff Bool [FILE_IO (OpenFile Read)]

5656

5757 Handler FileIO IO where { ... }

5858

@@ -69,9 +69,9 @@ RND

6969

7070 RND : EFFECT

7171

72− srand : Integer -> Eff m () [RND]

73− rndInt : Integer -> Integer -> Eff m Integer [RND]

74− rndFin : (k : Nat) -> Eff m (Fin (S k)) [RND]

72+ srand : Integer -> Eff () [RND]

73+ rndInt : Integer -> Integer -> Eff Integer [RND]

74+ rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]

7575

7676 Handler Random m where { ... }

7777

@@ -86,7 +86,7 @@ SELECT

8686

8787 SELECT : EFFECT

8888

89− select : List a -> Eff m a [SELECT]

89+ select : List a -> Eff a [SELECT]

9090

9191 Handler Selection Maybe where { ... }

9292 Handler Selection List where { ... }

@@ -102,10 +102,10 @@ STATE

102102

103103 STATE : Type -> EFFECT

104104

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]

105+ get : Eff x [STATE x]

106+ put : x -> Eff () [STATE x]

107+ putM : y -> Eff () [STATE x] [STATE y]

108+ update : (x -> x) -> Eff () [STATE x]

109109

110110 Handler State m where { ... }

111111

@@ -121,12 +121,12 @@ STDIO

121121

122122 STDIO : EFFECT

123123

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]

124+ putChar : Char -> Eff () [STDIO]

125+ putStr : String -> Eff () [STDIO]

126+ putStrLn : String -> Eff () [STDIO]

127127

128− getStr : Handler StdIO m => Eff m String [STDIO]

129− getChar : Handler StdIO m => Eff m Char [STDIO]

128+ getStr : Eff String [STDIO]

129+ getChar : Eff Char [STDIO]

130130

131131 Handler StdIO IO where { ... }

132132 Handler StdIO (IOExcept a) where { ... }

@@ -144,9 +144,9 @@ SYSTEM

144144

145145 SYSTEM : EFFECT

146146

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]

147+ getArgs : Eff (List String) [SYSTEM]

148+ time : Eff Int [SYSTEM]

149+ getEnv : String -> Eff (Maybe String) [SYSTEM]

150150

151151 Handler System IO where { ... }

152152 Handler System (IOExcept a) where { ... }