2ac0079 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Bring effects tutorial up to date

2ac0079Edwin Brady11 years ago

docs/effects/depeff.rst+44−39

compare with master

unifiedsplit

@@ -24,7 +24,7 @@ It might look something like the following:

25.. code-block:: idris

27− readInt : { [STATE (List Int), STDIO] } Eff ()

27+ readInt : Eff () [STATE (List Int), STDIO]

28 readInt = do let x = trim !getStr

29 put (cast x :: !get)

@@ -33,7 +33,7 @@ But what if, instead of a list of integers, we would like to store a

34.. code-block:: idris

36− readInt : { [STATE (Vect n Int), STDIO] } Eff ()

36+ readInt : Eff () [STATE (Vect n Int), STDIO]

37 readInt = do let x = trim !getStr

38 put (cast x :: !get)

@@ -43,8 +43,8 @@ express this as follows:

44.. code-block:: idris

46− readInt : { [STATE (Vect n Int), STDIO] ==>

46+ readInt : Eff ()[STATE (Vect n Int), STDIO]

47− [STATE (Vect (S n) Int), STDIO] } Eff ()

47+ [STATE (Vect (S n) Int), STDIO]

48 readInt = do let x = trim !getStr

49 putM (cast x :: !get)

@@ -56,7 +56,7 @@ It has the following type:

57.. code-block:: idris

59− putM : y -> { [STATE x] ==> [STATE y] } Eff ()

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

61Result-dependent Effects

62========================

@@ -69,8 +69,8 @@ digits). As a first attempt, we could try the following, returning a

70.. code-block:: idris

72− readInt : { [STATE (Vect n Int), STDIO] ==>

72+ readInt : Eff Bool [STATE (Vect n Int), STDIO]

73− [STATE (Vect (S n) Int), STDIO] } Eff Bool

73+ [STATE (Vect (S n) Int), STDIO]

74 readInt = do let x = trim !getStr

75 case all isDigit (unpack x) of

76 False => pure False

@@ -91,31 +91,31 @@ value read from the user was valid. We can express this in the type:

92.. code-block:: idris

94− readInt : { [STATE (Vect n Int), STDIO] ==>

94+ readInt : Eff Bool [STATE (Vect n Int), STDIO]

95− {ok} if ok then [STATE (Vect (S n) Int), STDIO]

95+ (\ok => if ok then [STATE (Vect (S n) Int), STDIO]

96− else [STATE (Vect n Int), STDIO] } Eff Bool

96+ else [STATE (Vect n Int), STDIO])

97 readInt = do let x = trim !getStr

98 case all isDigit (unpack x) of

99 False => pure False

100 True => do putM (cast x :: !get)

101− pure True

101+ pureM True

102+

103+Using ``pureM`` rather than ``pure`` allows the output effects to be

104+calculated from the value given. Its type is:

105+

106+.. code-block:: idris

102

107

103−The notation ``{ xs ==> res xs’ } Eff a`` in a type means that the

108+ pureM : (val : a) -> EffM m a (xs val) xs

104−effects available are updated from ``xs`` to ``xs’``, *and* the

105−resulting effects ``xs’`` may depend on the result of the operation

106−``res``, of type ``a``. Here, the resulting effects are computed from

107−the result ``ok``—if ``True``, the vector is extended, otherwise it

108−remains the same.

109

110−When using the function, we will naturally have to check its return

110+When using ``readInt``, we will have to check its return

111value in order to know what the new set of effects is. For example, to

112read a set number of values into a vector, we could write the following:

113

114.. code-block:: idris

115

116 readN : (n : Nat) ->

117− { [STATE (Vect m Int), STDIO] ==>

117+ Eff () [STATE (Vect m Int), STDIO]

118− [STATE (Vect (n + m) Int), STDIO] } Eff ()

118+ [STATE (Vect (n + m) Int), STDIO]

119 readN Z = pure ()

120 readN {m} (S k) = case !readInt of

121 True => rewrite plusSuccRightSucc k m in readN k

@@ -171,14 +171,17 @@ to support random access files and better reporting of error conditions.

171

172 data OpenFile : Mode -> Type

173

174− open : String -> (m : Mode) ->

174+ open : (fname : String)

175− { [FILE_IO ()] ==>

175+ -> (m : Mode)

176− {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff Bool

176+ -> Eff Bool [FILE_IO ()]

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

178+ True => OpenFile m

179+ False => ())])

177− close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()

180+ close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]

178

181

179− readLine : { [FILE_IO (OpenFile Read)] } Eff String

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

180− writeLine : { [FILE_IO (OpenFile Write)] } Eff ()

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

181− eof : { [FILE_IO (OpenFile Read)] } Eff Bool

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

182

185

183 instance Handler FileIO IO

186 instance Handler FileIO IO

184

187

@@ -186,9 +189,12 @@ In particular, consider the type of ``open``:

186

189

187.. code-block:: idris

190.. code-block:: idris

188

191

189− open : String -> (m : Mode) ->

192+ open : (fname : String)

190− { [FILE_IO ()] ==>

193+ -> (m : Mode)

191− {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff Bool

194+ -> Eff Bool [FILE_IO ()]

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

196+ True => OpenFile m

197+ False => ())])

192

198

193This returns a ``Bool`` which indicates whether opening the file was

199This returns a ``Bool`` which indicates whether opening the file was

194successful. The resulting state depends on whether the operation was

200successful. The resulting state depends on whether the operation was

@@ -199,10 +205,9 @@ we continue the protocol accordingly.

199.. _eff-readfile:

205.. _eff-readfile:

200.. code-block:: idris

206.. code-block:: idris

201

207

202− readFile : { [FILE_IO (OpenFile Read)] } Eff (List String)

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

203 readFile = readAcc [] where

209 readFile = readAcc [] where

204− readAcc : List String -> { [FILE_IO (OpenFile Read)] }

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

205− Eff (List String)

206 readAcc acc = if (not !eof)

211 readAcc acc = if (not !eof)

207 then readAcc (!readLine :: acc)

212 then readAcc (!readLine :: acc)

208 else pure (reverse acc)

213 else pure (reverse acc)

@@ -214,7 +219,7 @@ correctly following the protocol:

214

219

215.. code-block:: idris

220.. code-block:: idris

216

221

217− dumpFile : String -> { [FILE_IO (), STDIO] } Eff ()

222+ dumpFile : String -> Eff () [FILE_IO (), STDIO]

218 dumpFile name = case !(open name Read) of

223 dumpFile name = case !(open name Read) of

219 True => do putStrLn (show !readFile)

224 True => do putStrLn (show !readFile)

220 close

225 close

@@ -255,7 +260,7 @@ Idris supports *pattern-matching* bindings, such as the following:

255

260

256.. code-block:: idris

261.. code-block:: idris

257

262

258− dumpFile : String -> { [FILE_IO (), STDIO] } Eff ()

263+ dumpFile : String -> Eff () [FILE_IO (), STDIO]

259 dumpFile name = do True <- open name Read

264 dumpFile name = do True <- open name Read

260 putStrLn (show !readFile)

265 putStrLn (show !readFile)

261 close

266 close

@@ -267,7 +272,7 @@ example, we could write:

267

272

268.. code-block:: idris

273.. code-block:: idris

269

274

270− dumpFile : String -> { [FILE_IO (), STDIO] } Eff ()

275+ dumpFile : String -> Eff () [FILE_IO (), STDIO]

271 dumpFile name = do True <- open name Read | False => putStrLn "Error"

276 dumpFile name = do True <- open name Read | False => putStrLn "Error"

272 putStrLn (show !readFile)

277 putStrLn (show !readFile)

273 close

278 close

@@ -297,7 +302,7 @@ reading command line arguments, among other things (see Appendix

297

302

298.. code-block:: idris

303.. code-block:: idris

299

304

300− getArgs : { [SYSTEM] } Eff (List String)

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

301

306

302A main program can read command line arguments as follows, where in the

307A main program can read command line arguments as follows, where in the

303list which is returned, the first element ``prog`` is the executable

308list which is returned, the first element ``prog`` is the executable

@@ -305,7 +310,7 @@ name and the second is an expected argument:

305

310

306.. code-block:: idris

311.. code-block:: idris

307

312

308− emain : { [SYSTEM, STDIO] } Eff ()

313+ emain : Eff () [SYSTEM, STDIO]

309 emain = do [prog, arg] <- getArgs

314 emain = do [prog, arg] <- getArgs

310 putStrLn $ "Argument is " ++ arg

315 putStrLn $ "Argument is " ++ arg

311 {- ... rest of function ... -}

316 {- ... rest of function ... -}

@@ -316,7 +321,7 @@ alternatives to give a better (more informative) error:

316

321

317.. code-block:: idris

322.. code-block:: idris

318

323

319− emain : { [SYSTEM, STDIO] } Eff ()

324+ emain : Eff () [SYSTEM, STDIO]

320 emain = do [prog, arg] <- getArgs | [] => putStrLn "Can't happen!"

325 emain = do [prog, arg] <- getArgs | [] => putStrLn "Can't happen!"

321 | [prog] => putStrLn "No arguments!"

326 | [prog] => putStrLn "No arguments!"

322 | _ => putStrLn "Too many arguments!"

327 | _ => putStrLn "Too many arguments!"

docs/effects/hangman.rst+27−30

@@ -95,7 +95,7 @@ NewWord

95 choice of 6 is somewhat arbitrary here) and the number of unique

96 letters in the word still to be guessed.

98−StrState

98+Get

99 Get a string representation of the game state. This is for display

100 purposes; there are no pre- or postconditions.

101

@@ -106,16 +106,19 @@ effect signature:

106

107 data MysteryRules : Effect where

108 Guess : (x : Char) ->

109− { Mystery (Running (S g) (S w)) ==>

110− {inword} if inword then Mystery (Running (S g) w)

111− else Mystery (Running g (S w)) }

112− MysteryRules Bool

109+ sig MysteryRules Bool

110+ (Mystery (Running (S g) (S w)))

111+ (\inword =>

112+ Mystery (case inword of

113+ True => (Running (S g) w)

114+ False => (Running g (S w))))

115+ Won : sig MysteryRules () (Mystery (Running g 0))

113− Won : { Mystery (Running g 0) ==> Mystery NotRunning } MysteryRules ()

116+ (Mystery NotRunning)

117+ Lost : sig MysteryRules () (Mystery (Running 0 g))

114− Lost : { Mystery (Running 0 g) ==> Mystery NotRunning } MysteryRules ()

118+ (Mystery NotRunning)

115− NewWord : (w : String) ->

119+ NewWord : (w : String) ->

116− { Mystery NotRunning ==>

117− Mystery (Running 6 (length (letters w))) } MysteryRules ()

120+ sig MysteryRules () h (Mystery (Running 6 (length (letters w))))

118− StrState : { Mystery h } MysteryRules String

121+ Get : sig MysteryRules String (Mystery h)

119

122

120This description says nothing about how the rules are implemented. In

123This description says nothing about how the rules are implemented. In

121particular, it does not specify *how* to tell whether a guessed letter

124particular, it does not specify *how* to tell whether a guessed letter

@@ -195,7 +198,7 @@ implementation for ``MysteryRules`` is surprisingly straightforward:

195 handle (MkG w g got []) Won k = k () (GameWon w)

198 handle (MkG w g got []) Won k = k () (GameWon w)

196 handle (MkG w Z got m) Lost k = k () (GameLost w)

199 handle (MkG w Z got m) Lost k = k () (GameLost w)

197

200

198− handle st StrState k = k (show st) st

201+ handle st Get k = k (show st) st

199 handle st (NewWord w) k = k () (initState w)

202 handle st (NewWord w) k = k () (initState w)

200

203

201 handle (MkG w (S g) got m) (Guess x) k =

204 handle (MkG w (S g) got m) (Guess x) k =

@@ -219,8 +222,8 @@ for the game which uses the ``MYSTERY`` effect:

219

222

220.. code-block:: idris

223.. code-block:: idris

221

224

222− game : { [MYSTERY (Running (S g) w), STDIO] ==>

225+ game : Eff () [MYSTERY (Running (S g) w), STDIO]

223− [MYSTERY NotRunning, STDIO] } Eff ()

226+ [MYSTERY NotRunning, STDIO]

224

227

225The type indicates that the game must start in a running state, with

228The type indicates that the game must start in a running state, with

226some guesses available, and eventually reach a not-running state (i.e.

229some guesses available, and eventually reach a not-running state (i.e.

@@ -239,12 +242,12 @@ running ``game``:

239

242

240.. code-block:: idris

243.. code-block:: idris

241

244

242− runGame : { [MYSTERY NotRunning, RND, SYSTEM, STDIO] } Eff ()

245+ runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]

243 runGame = do srand (cast !time)

246 runGame = do srand (cast !time)

244 let w = index !(rndFin WEWEWE) words

247 let w = index !(rndFin WEWEWE) words

245 NewWord w

248 NewWord w

246 game

249 game

247− putStrLn !StrState

250+ putStrLn !Get

248

251

249We use the system time (``time`` from the ``SYSTEM`` effect; see

252We use the system time (``time`` from the ``SYSTEM`` effect; see

250Appendix :ref:`sect-appendix`) to initialise the random number

253Appendix :ref:`sect-appendix`) to initialise the random number

@@ -271,11 +274,11 @@ presented below:

271

274

272.. code-block:: idris

275.. code-block:: idris

273

276

274− game : { [MYSTERY (Running (S g) w), STDIO] ==>

277+ game : Eff () [MYSTERY (Running (S g) w), STDIO]

275− [MYSTERY NotRunning, STDIO] } Eff ()

278+ [MYSTERY NotRunning, STDIO]

276 game {w=Z} = Won

279 game {w=Z} = Won

277 game {w=S _}

280 game {w=S _}

278− = do putStrLn !StrState

281+ = do putStrLn !Get

279 putStr "Enter guess: "

282 putStr "Enter guess: "

280 let guess = trim !getStr

283 let guess = trim !getStr

281 case choose (not (guess == "")) of

284 case choose (not (guess == "")) of

@@ -283,9 +286,8 @@ presented below:

283 (Right p) => do putStrLn "Invalid input!"

286 (Right p) => do putStrLn "Invalid input!"

284 game

287 game

285 where

288 where

286− processGuess : Char -> { [MYSTERY (Running (S g) (S w)), STDIO] ==>

289+ processGuess : Char -> Eff () [MYSTERY (Running (S g) (S w)), STDIO]

287− [MYSTERY NotRunning, STDIO] }

290+ [MYSTERY NotRunning, STDIO]

288− Eff ()

289 processGuess {g} {w} c

291 processGuess {g} {w} c

290 = case !(Main.Guess c) of

292 = case !(Main.Guess c) of

291 True => do putStrLn "Good guess!"

293 True => do putStrLn "Good guess!"

@@ -315,16 +317,11 @@ transitions for ``MysteryRules``. Then, when implementing ``game`` at

315first, any incorrect assumption was caught as a type error. The

317first, any incorrect assumption was caught as a type error. The

316following errors were caught during development:

318following errors were caught during development:

317

319

318−- Not realising that allowing ``NewWord`` to be an arbitrary string

320+- Not realising that allowing ``NewWord`` to be an arbitrary string would mean that ``game`` would have to deal with a zero-length word as a starting state.

319− would mean that ``game`` would have to deal with a zero-length word

320− as a starting state.

321

322−- Forgetting to check whether a game was won before recursively

323− calling ``processGuess``, thus accidentally continuing a finished

322+- Forgetting to check whether a game was won before recursively calling ``processGuess``, thus accidentally continuing a finished game.

324− game.

325

323

326−- Accidentally checking the number of missing letters, rather than the

324+- Accidentally checking the number of missing letters, rather than the number of remaining guesses, when checking if a game was lost.

327− number of remaining guesses, when checking if a game was lost.

328

325

329These are, of course, simple errors, but were caught by the type

326These are, of course, simple errors, but were caught by the type

330checker before any testing of the game.

327checker before any testing of the game.

docs/effects/impleff.rst+62−51

@@ -23,24 +23,11 @@ available. Stateful operations are described as follows:

23.. code-block:: idris

25 data State : Effect where

26− Get : { a } State a

26+ Get : State a a (\x => a)

27− Put : b -> { a ==> b } State ()

27+ Put : b -> State () a (\x => b)

29−Each effect is associated with a *resource*, the type of which is

30−given with the notation ``{ x ==> x’ }``. This notation gives the

31−resource type expected by each operation, and how it updates when the

32−operation is run. Here, it means:

33−

34−- ``Get`` takes no arguments. It has a resource of type ``a``, which

35− is not updated, and running the ``Get`` operation returns something

36− of type ``a``.

37−

38−- ``Put`` takes a ``b`` as an argument. It has a resource of type

39− ``a`` on input, which is updated to a resource of type

40− ``b``. Running the ``Put`` operation returns the element of the

41− unit type.

42−

43−``Effect`` itself is a type synonym, declared as follows:

29+``Effect`` itself is a type synonym, giving the required type for an

30+effect signature:

45.. code-block:: idris

32.. code-block:: idris

@@ -49,18 +36,41 @@ operation is run. Here, it means:

49 (input_resource : Type) ->

36 (input_resource : Type) ->

50 (output_resource : result -> Type) -> Type

37 (output_resource : result -> Type) -> Type

52−That is, an effectful operation returns something of type ``result``,

39+Each effect is associated with a *resource*. The second argument to

53−has an input resource of type ``input_resource``, and a function

40+an effect signature is the resource type on *input* to an operation,

54−``output_resource`` which computes the output resource type from the

41+and the third is a function which computes the resource type on

55−result. We use the same syntactic sugar as with ``Eff`` to make effect

42+*output*. Here, it means:

56−declarations more readable. It is defined as follows in the library:

43+

44+- ``Get`` takes no arguments. It has a resource of type ``a``, which is not updated, and running the ``Get`` operation returns something of type ``a``.

45+

46+- ``Put`` takes a ``b`` as an argument. It has a resource of type ``a`` on input, which is updated to a resource of type ``b``. Running the ``Put`` operation returns the element of the unit type.

47+

48+The effects library provides an overloaded function ``sig``

49+which can make effect signatures more concise, particularly when the

50+result has no effect on the resource type. For ``State``, we can

51+write:

58.. code-block:: idris

53.. code-block:: idris

60− syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

55+ data State : Effect where

61− syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

56+ Get : sig State a a

62− = eff inst (\b => outst)

57+ Put : b -> sig State () a b

63− syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

58+

59+There are four versions of ``sig``, depending on whether we

60+are interested in the resource type, and whether we are updating the

61+resource. Idris will infer the appropriate version from usage.

62+

63+.. code-block:: idris

64+

65+ NoResourceEffect.sig : Effect -> Type -> Type

66+ NoUpdateEffect.sig : Effect -> (ret : Type) ->

67+ (resource : Type) -> Type

68+ UpdateEffect.sig : Effect -> (ret : Type) ->

69+ (resource_in : Type) ->

70+ (resource_out : Type) -> Type

71+ DepUpdateEffect.sig : Effect -> (ret : Type) ->

72+ (resource_in : Type) ->

73+ (resource_out : ret -> Type) -> Type

65In order to convert ``State`` (of type ``Effect``) into something

75In order to convert ``State`` (of type ``Effect``) into something

66usable in an effects list, of type ``EFFECT``, we write the following:

76usable in an effects list, of type ``EFFECT``, we write the following:

@@ -96,13 +106,11 @@ summaries in Section :ref:`sect-simpleff`. An instance of ``Handler e

96m`` means that the effect declared with signature ``e`` can be run in

106m`` means that the effect declared with signature ``e`` can be run in

97computation context ``m``. The ``handle`` function takes:

107computation context ``m``. The ``handle`` function takes:

108

99−- The ``resource`` on input (so, the current value of the state for

109+- The ``resource`` on input (so, the current value of the state for ``State``)

100− ``State``)

101

110

102- The effectful operation (either ``Get`` or ``Put x`` for ``State``)

111- The effectful operation (either ``Get`` or ``Put x`` for ``State``)

103

112

104−- A *continuation*, which we conventionally call ``k``, and should be

105− passed the result value of the operation, and an updated resource.

113+- A *continuation*, which we conventionally call ``k``, and should be passed the result value of the operation, and an updated resource.

106

114

107There are two reasons for taking a continuation here: firstly, this is

115There are two reasons for taking a continuation here: firstly, this is

108neater because there are multiple return values (a new resource and

116neater because there are multiple return values (a new resource and

@@ -125,13 +133,13 @@ functions in ``Eff``, as follows:

125

133

126.. code-block:: idris

134.. code-block:: idris

127

135

128− get : { [STATE x] } Eff x

136+ get : Eff x [STATE x]

129 get = call Get

137 get = call Get

130

138

131− put : x -> { [STATE x] } Eff ()

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

132 put val = call (Put val)

140 put val = call (Put val)

133

141

134− putM : y -> { [STATE x] ==> [STATE y] } Eff ()

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

135 putM val = call (Put val)

143 putM val = call (Put val)

136

144

137**An implementation detail (aside):** The ``call`` function converts

145**An implementation detail (aside):** The ``call`` function converts

@@ -162,8 +170,8 @@ The following listing summarises what is required to define the

162.. code-block:: idris

170.. code-block:: idris

163

171

164 data State : Effect where

172 data State : Effect where

165− Get : { a } State a

173+ Get : sig State a a

166− Put : b -> { a ==> b } State ()

174+ Put : b -> sig State () a b

167

175

168 STATE : Type -> EFFECT

176 STATE : Type -> EFFECT

169 STATE t = MkEff t State

177 STATE t = MkEff t State

@@ -172,13 +180,13 @@ The following listing summarises what is required to define the

172 handle st Get k = k st st

180 handle st Get k = k st st

173 handle st (Put n) k = k () n

181 handle st (Put n) k = k () n

174

182

175− get : { [STATE x] } Eff x

183+ get : Eff x [STATE x]

176 get = call Get

184 get = call Get

177

185

178− put : x -> { [STATE x] } Eff ()

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

179 put val = call (Put val)

187 put val = call (Put val)

180

188

181− putM : y -> { [STATE x] ==> [STATE y] } Eff ()

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

182 putM val = call (Put val)

190 putM val = call (Put val)

183

191

184

192

@@ -198,10 +206,10 @@ directly.

198.. code-block:: idris

206.. code-block:: idris

199

207

200 data StdIO : Effect where

208 data StdIO : Effect where

201− PutStr : String -> { () } StdIO ()

209+ PutStr : String -> sig StdIO ()

202− GetStr : { () } StdIO String

210+ GetStr : sig StdIO String

203− PutCh : Char -> { () } StdIO ()

211+ PutCh : Char -> sig StdIO ()

204− GetCh : { () } StdIO Char

212+ GetCh : sig StdIO Char

205

213

206 instance Handler StdIO IO where

214 instance Handler StdIO IO where

207 handle () (PutStr s) k = do putStr s; k () ()

215 handle () (PutStr s) k = do putStr s; k () ()

@@ -231,7 +239,7 @@ error.

231.. code-block:: idris

239.. code-block:: idris

232

240

233 data Exception : Type -> Effect where

241 data Exception : Type -> Effect where

234− Raise : a -> { () } Exception a b

242+ Raise : a -> sig (Exception a) b

235

243

236 instance Handler (Exception a) Maybe where

244 instance Handler (Exception a) Maybe where

237 handle _ (Raise e) k = Nothing

245 handle _ (Raise e) k = Nothing

@@ -255,7 +263,7 @@ value.

255.. code-block:: idris

263.. code-block:: idris

256

264

257 data Selection : Effect where

265 data Selection : Effect where

258− Select : List a -> { () } Selection a

266+ Select : List a -> sig Selection a

259

267

260 instance Handler Selection Maybe where

268 instance Handler Selection Maybe where

261 handle _ (Select xs) k = tryAll xs where

269 handle _ (Select xs) k = tryAll xs where

@@ -289,13 +297,16 @@ the equivalent ``Eff`` programs.

289.. code-block:: idris

297.. code-block:: idris

290

298

291 data FileIO : Effect where

299 data FileIO : Effect where

292− Open : String -> (m : Mode) ->

300+ Open : (fname: String)

293− {() ==> {res} if res then OpenFile m else ()} FileIO Bool

301+ -> (m : Mode)

294− Close : {OpenFile m ==> ()} FileIO ()

302+ -> sig FileIO Bool () (\res => case res of

295−

303+ True => OpenFile m

304+ False => ())

305+ Close : sig FileIO () (OpenFile m)

306+

296− ReadLine : {OpenFile Read} FileIO String

307+ ReadLine : sig FileIO String (OpenFile Read)

297− WriteLine : String -> {OpenFile Write} FileIO ()

308+ WriteLine : String -> sig FileIO () (OpenFile Write)

298− EOF : {OpenFile Read} FileIO Bool

309+ EOF : sig FileIO Bool (OpenFile Read)

299

310

300 instance Handler FileIO IO where

311 instance Handler FileIO IO where

301 handle () (Open fname m) k = do h <- openFile fname m

312 handle () (Open fname m) k = do h <- openFile fname m

docs/effects/introduction.rst+4−8

@@ -37,11 +37,9 @@ introductory tutorials, is “How do I turn this into a program?” That is,

37given some lists entered by a user, how do we get into a position to be

38able to apply the ``vadd`` function? Before doing so, we will have to:

40−- Read user input, either from the keyboard, a file, or some other

40+- Read user input, either from the keyboard, a file, or some other input device.

41− input device.

43−- Check that the user inputs are valid, i.e. contain only ``Int`` s

42+- Check that the user inputs are valid, i.e. contain only ``Int`` and are the same length, and report an error if not.

44− and are the same length, and report an error if not.

46- Write output

44- Write output

@@ -66,7 +64,7 @@ library:

66 import Effects

64 import Effects

67 import Effect.StdIO

65 import Effect.StdIO

69− hello : {[STDIO]} Eff ()

67+ hello : Eff () [STDIO]

70 hello = putStrLn “Hello world!”

68 hello = putStrLn “Hello world!”

72 main : IO ()

70 main : IO ()

@@ -108,6 +106,4 @@ accurately. References to further reading are given in Section

108:ref:`sect-further`.

106:ref:`sect-further`.

109

107

110.. [1]

108.. [1]

111− You do not, however, need to know what a monad is. A correctness

109+ You do not, however, need to know what a monad is!

112− property of this tutorial is that the word “monad” should appear

113− exactly twice, both in this footnote.

docs/effects/simpleeff.rst+33−33

@@ -14,10 +14,10 @@ in a module ``Effect.State``

15 STATE : Type -> EFFECT

17− get : { [STATE x] } Eff x

17+ get : Eff x [STATE x]

18− put : x -> { [STATE x] } Eff ()

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

19− putM : y -> { [STATE x] ==> [STATE y] } Eff ()

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

20− update : (x -> x) -> { [STATE x] } Eff ()

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

22 instance Handler State m

@@ -56,12 +56,12 @@ can perform (or at the very least simulate) console I/O:

57 STDIO : EFFECT

59− putChar : Char -> { [STDIO] } Eff ()

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

60− putStr : String -> { [STDIO] } Eff ()

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

61− putStrLn : String -> { [STDIO] } Eff ()

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

63− getStr : { [STDIO] } Eff String

63+ getStr : Eff String [STDIO]

64− getChar : { [STDIO] } Eff Char

64+ getChar : Eff Char [STDIO]

66 instance Handler StdIO IO

67 instance Handler StdIO (IOExcept a)

@@ -74,7 +74,7 @@ as follows:

75.. code-block:: idris

77− hello : { [STDIO] } Eff ()

77+ hello : Eff () [STDIO]

78 hello = do putStr "Name? "

79 x <- getStr

80 putStrLn ("Hello " ++ trim x ++ "!")

@@ -94,7 +94,7 @@ getStr``, since we only use the string that is read once:

95.. code-block:: idris

97− hello : { [STDIO] } Eff ()

97+ hello : Eff () [STDIO]

98 hello = do putStr "Name? "

99 putStrLn ("Hello " ++ trim !getStr ++ "!")

100

@@ -104,7 +104,7 @@ said hello to:

104

105.. code-block:: idris

106

107− hello : { [STATE Int, STDIO] } Eff ()

107+ hello : Eff () [STATE Int, STDIO]

108 hello = do putStr "Name? "

109 putStrLn ("Hello " ++ trim !getStr ++ "!")

110 update (+1)

@@ -146,7 +146,7 @@ generally:

146

147 EXCEPTION : Type -> EFFECT

148

149− raise : a -> { [EXCEPTION a ] } Eff b

149+ raise : a -> Eff b [EXCEPTION a]

150

151 instance Handler (Exception a) Maybe

152 instance Handler (Exception a) List

@@ -167,7 +167,7 @@ paramaterised by an error type:

167

168 data Err = NotANumber | OutOfRange

169

170− parseNumber : Int -> String -> { [EXCEPTION Err] } Eff Int

170+ parseNumber : Int -> String -> Eff Int [EXCEPTION Err]

171 parseNumber num str

172 = if all isDigit (unpack str)

173 then let x = cast str in

@@ -222,7 +222,7 @@ the boundedness proof:

222

223.. code-block:: idris

224

225− parseNumber : (x : Int) -> String -> { [EXCEPTION Err] } Eff (Bounded x)

225+ parseNumber : (x : Int) -> String -> Eff (Bounded x) [EXCEPTION Err]

226 parseNumber x str

227 = if all isDigit (unpack str)

228 then let num = cast str in

@@ -243,9 +243,9 @@ Random number generation is also implemented by the library, in module

243

244 RND : EFFECT

245

246− srand : Integer -> { [RND] } Eff ()

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

247− rndInt : Integer -> Integer -> { [RND] } Eff Integer

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

248− rndFin : (k : Nat) -> { [RND] } Eff (Fin (S k))

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

249

250 instance Handler Random m

251

@@ -272,14 +272,14 @@ correct:

272

273.. code-block:: idris

274

275− guess : Int -> { [STDIO] } Eff ()

275+ guess : Int -> Eff () [STDIO]

276

277For reference, the code for ``guess`` is given below:

278

279.. _eff-game:

280.. code-block:: idris

281

282− guess : Int -> { [STDIO] } Eff ()

282+ guess : Int -> Eff () [STDIO]

283 guess target

284 = do putStr "Guess: "

285 case run {m=Maybe} (parseNumber 100 (trim !getStr)) of

@@ -303,7 +303,7 @@ having set up the random number generator with a seed, then run

303

304.. code-block:: idris

305

306− game : { [RND, STDIO] } Eff ()

306+ game : Eff () [RND, STDIO]

307 game = do srand 123456789

308 guess (fromInteger !(rndInt 0 100))

309

@@ -331,7 +331,7 @@ succeeds:

331

332 SELECT : EFFECT

333

334− select : List a -> { [SELECT] } Eff a

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

335

336 instance Handler Selection Maybe

337 instance Handler Selection List

@@ -346,7 +346,7 @@ of values which does not satisfy the constraint:

346

347.. code-block:: idris

348

349− triple : Int -> { [SELECT, EXCEPTION String] } Eff (Int, Int, Int)

349+ triple : Int -> Eff (Int, Int, Int) [SELECT, EXCEPTION String]

350 triple max = do z <- select [1..max]

351 y <- select [1..z]

352 x <- select [1..y]

@@ -396,7 +396,7 @@ they are equal:

396.. code-block:: idris

397

398 vadd_check : Vect n Int -> Vect m Int ->

399− { [EXCEPTION String] } Eff (Vect m Int)

399+ Eff (Vect m Int) [EXCEPTION String]

400 vadd_check {n} {m} xs ys with (decEq n m)

401 vadd_check {n} {m=n} xs ys | (Yes Refl) = pure (vadd xs ys)

402 vadd_check {n} {m} xs ys | (No contra) = raise "Length mismatch"

@@ -406,7 +406,7 @@ following type:

406

407.. code-block:: idris

408

409− read_vec : { [STDIO] } Eff (p ** Vect p Int)

409+ read_vec : Eff (p ** Vect p Int) [STDIO]

410

411This returns a dependent pair of a length, and a vector of that

412length, because we cannot know in advance how many integers the user

@@ -421,7 +421,7 @@ inputs are of differing lengths:

421

422.. code-block:: idris

423

424− do_vadd : { [STDIO, EXCEPTION String] } Eff ()

424+ do_vadd : Eff () [STDIO, EXCEPTION String]

425 do_vadd = do putStrLn "Vector 1"

426 (_ ** xs) <- read_vec

427 putStrLn "Vector 2"

@@ -436,7 +436,7 @@ with gracefully.

436

437.. code-block:: idris

438

439− read_vec : { [STDIO] } Eff (p ** Vect p Int)

439+ read_vec : Eff (p ** Vect p Int) [STDIO]

440 read_vec = do putStr "Number (-1 when done): "

441 case run (parseNumber (trim !getStr)) of

442 Nothing => do putStrLn "Input error"

@@ -446,7 +446,7 @@ with gracefully.

446 pure (_ ** v :: xs)

447 else pure (_ ** [])

448 where

449− parseNumber : String -> { [EXCEPTION String] } Eff Int

449+ parseNumber : String -> Eff Int [EXCEPTION String]

450 parseNumber str

451 = if all (\x => isDigit x || x == '-') (unpack str)

452 then pure (cast str)

@@ -493,7 +493,7 @@ values:

493 Env : Type

494 Env = List (String, Integer)

495

496− eval : Expr -> { [EXCEPTION String, STATE Env] } Eff Integer

496+ eval : Expr -> Eff Integer [EXCEPTION String, STATE Env]

497 eval (Val x) = return x

498 eval (Add l r) = return $ !(eval l) + !(eval r)

499

@@ -520,7 +520,7 @@ sets the state then invokes ``eval``:

520

521 runEval : List (String, Integer) -> Expr -> Maybe Integer

522 runEval args expr = run (eval' expr)

523− where eval' : Expr -> { [EXCEPTION String, STATE Env] } Eff Integer

523+ where eval' : Expr -> Eff Integer [EXCEPTION String, STATE Env]

524 eval' e = do put args

525 eval e

526

@@ -547,7 +547,7 @@ appears in the list, as long as it is present:

547

548.. code-block:: idris

549

550− eval : Expr -> { [EXCEPTION String, RND, STATE Env] } Eff Integer

550+ eval : Expr -> Eff Integer [EXCEPTION String, RND, STATE Env]

551

552 eval (Random upper) = rndInt 0 upper

553

@@ -575,7 +575,7 @@ this simply by updating the type of ``eval`` to include ``STDIO``.

575

576.. code-block:: idris

577

578− eval : Expr -> { [STDIO, EXCEPTION String, RND, STATE Env] } Eff Integer

578+ eval : Expr -> Eff Integer [STDIO, EXCEPTION String, RND, STATE Env]

579

580Note that using ``STDIO`` will restrict the number of contexts in

581which ``eval`` can be ``run`` to those which support ``STDIO``, such

@@ -587,6 +587,6 @@ types are first class in Idris:

587.. code-block:: idris

588

589 EvalEff : Type -> Type

590− EvalEff t = { [STDIO, EXCEPTION String, RND, STATE Env] } Eff t

590+ EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]

591

592 eval : Expr -> EvalEff Integer

docs/effects/state.rst+55−47

@@ -83,7 +83,7 @@ effectful program ``f`` has a type of the following form:

84.. code-block:: idris

86− f : (x1 : a1) -> (x2 : a2) -> ... -> { effs } Eff t

86+ f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs

88That is, the return type gives the effects that ``f`` supports

89(``effs``, of type ``List EFFECT``) and the type the computation

@@ -92,7 +92,7 @@ following type:

93.. code-block:: idris

95− treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))

95+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]

97That is, ``treeTagAux`` has access to an integer state, because the

98list of available effects includes ``STATE Int``. ``STATE`` is

@@ -141,8 +141,8 @@ following types, polymorphic in the state ``t`` they manage:

141

142.. code-block:: idris

143

144− get : { [STATE t] } Eff t

144+ get : Eff t [STATE t]

145− put : t -> { [STATE t] } Eff ()

145+ put : t -> Eff () [STATE t]

146

147A program in ``Eff`` can call any other function in ``Eff`` provided

148that the calling function supports at least the effects required by

@@ -168,7 +168,7 @@ instead of ``runPure``:

168

169.. code-block:: idris

170

171− treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))

171+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]

172 ...

173

174 treeTag : (i : Int) -> BTree a -> IO (BTree (Int, a))

@@ -202,7 +202,7 @@ shown in Listing [introprog].

202 "Sheila"

203 (Node Leaf "Bob" Leaf))

204

205− treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))

205+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]

206 treeTagAux Leaf = pure Leaf

207 treeTagAux (Node l x r) = do l' <- treeTagAux l

208 i <- get

@@ -227,8 +227,8 @@ here for illustrative purposes):

227

228.. code-block:: idris

229

230− runPure : {env : Env id xs} -> { xs } Eff a -> a

230+ runPure : {env : Env id xs} -> Eff a xs -> a

231− run : Applicative m => {env : Env m xs} -> { xs } Eff a -> m a

231+ run : Applicative m => {env : Env m xs} -> Eff a xs -> m a

232

233The ``env`` argument is implicit, and initialised automatically where

234possible using default values given by instances of the following type

@@ -248,8 +248,8 @@ using one of the following functions:

248

249.. code-block:: idris

250

251− runPureInit : Env id xs -> { xs } Eff a -> a

251+ runPureInit : Env id xs -> Eff a xs -> a

252− runInit : Applicative m => Env m xs -> { xs } Eff a -> m a

252+ runInit : Applicative m => Env m xs -> Eff a xs -> m a

253

254To be well-typed, the environment must contain resources corresponding

255exactly to the effects in ``xs``. For example, we could also have

@@ -272,8 +272,7 @@ captured both of these values, e.g.:

272

273.. code-block:: idris

274

275− treeTagAux : BTree a

275+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE (Int, Int)]

276− -> { [STATE (Int, Int)] } Eff (BTree (Int, a))

277

276

278Doing this, however, ties the two states together throughout (as well

277Doing this, however, ties the two states together throughout (as well

279as not indicating which integer is which). It would be nice to be able

278as not indicating which integer is which). It would be nice to be able

@@ -288,9 +287,9 @@ leaves and update the tag separately, by labelling them as follows:

288

287

289.. code-block:: idris

288.. code-block:: idris

290

289

291− treeTagAux : BTree a

290+ treeTagAux : BTree a -> Eff (BTree (Int, a))

292− -> {['Tag ::: STATE Int,

291+ ['Tag ::: STATE Int,

293− 'Leaves ::: STATE Int]} Eff (BTree (Int, a))

292+ 'Leaves ::: STATE Int]

294

293

295The ``:::`` operator allows an arbitrary label to be given to an

294The ``:::`` operator allows an arbitrary label to be given to an

296effect. This label can be any type—it is simply used to identify an

295effect. This label can be any type—it is simply used to identify an

@@ -320,7 +319,7 @@ applying a function to the current state.

320

319

321.. code-block:: idris

320.. code-block:: idris

322

321

323− update : (x -> x) -> { [STATE x] } Eff ()

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

324

323

325Finally, our top level ``treeTag`` function now returns a pair of the

324Finally, our top level ``treeTag`` function now returns a pair of the

326number of leaves, and the new tree. Resources for labelled effects are

325number of leaves, and the new tree. Resources for labelled effects are

@@ -339,8 +338,7 @@ To summarise, we have:

339

338

340- ``:::`` to convert an effect to a labelled effect.

339- ``:::`` to convert an effect to a labelled effect.

341

340

342−- ``:-`` to convert an effectful operation to a labelled effectful

341+- ``:-`` to convert an effectful operation to a labelled effectful operation.

343− operation.

344

342

345- ``:=`` to initialise a resource for a labelled effect.

343- ``:=`` to initialise a resource for a labelled effect.

346

344

@@ -350,7 +348,7 @@ only for the situation where available effects are not updated):

350.. code-block:: idris

348.. code-block:: idris

351

349

352 (:::) : lbl -> EFFECT -> EFFECT

350 (:::) : lbl -> EFFECT -> EFFECT

353− (:-) : (l : lbl) -> { [x] } Eff a -> { [l ::: x] } Eff a

351+ (:-) : (l : lbl) -> Eff a [x] -> Eff a [l ::: x]

354 (:=) : (l : lbl) -> res -> LRes l res

352 (:=) : (l : lbl) -> res -> LRes l res

355

353

356Here, ``LRes`` is simply the resource type associated with a labelled

354Here, ``LRes`` is simply the resource type associated with a labelled

@@ -367,7 +365,7 @@ immediately. The following program returns the length of the

367

365

368.. code-block:: idris

366.. code-block:: idris

369

367

370− stateLength : { [STATE String] } Eff Nat

368+ stateLength : Eff Nat [STATE String]

371 stateLength = do x <- get

369 stateLength = do x <- get

372 pure (length x)

370 pure (length x)

373

371

@@ -377,7 +375,7 @@ this. The above program can be written instead as:

377

375

378.. code-block:: idris

376.. code-block:: idris

379

377

380− stateLength : { [STATE String] } Eff Nat

378+ stateLength : Eff Nat [STATE String]

381 stateLength = pure (length !get)

379 stateLength = pure (length !get)

382

380

383The notation ``!expr`` means that the expression ``expr`` should be

381The notation ``!expr`` means that the expression ``expr`` should be

@@ -386,7 +384,7 @@ evaluated and then implicitly bound. Conceptually, we can think of

386

384

387.. code-block:: idris

385.. code-block:: idris

388

386

389− (!) : { xs } Eff a -> a

387+ (!) : Eff a xs -> a

390

388

391Note, however, that it is not really a function, merely syntax! In

389Note, however, that it is not really a function, merely syntax! In

392practice, a subexpression ``!expr`` will lift ``expr`` as high as

390practice, a subexpression ``!expr`` will lift ``expr`` as high as

@@ -411,22 +409,22 @@ is lifted to:

411 g' <- g y' x'

409 g' <- g y' x'

412 f g'

410 f g'

413

411

414−Syntactic Sugar and ``Eff``

412+The Type ``Eff``

415−===========================

413+================

416

414

417−By now, you may be wondering about the syntax we are using for

415+Underneath, ``Eff`` is an overloaded function which translates to an

418−``Eff``, because it doesn’t look like a normal type! (If not, you may

416+underlying type ``EffM``:

419−safely skip this section and return to it later.) In fact, the type of

420−``Eff`` is the following:

421

417

422.. code-block:: idris

418.. code-block:: idris

423

419

424− Eff : (x : Type) ->

420+ EffM : (m : Type -> Type) -> (t : Type)

421+ -> (List EFFECT)

425− List EFFECT -> (x -> List EFFECT) -> Type

422+ -> (t -> List EFFECT) -> Type

426

423

427This is more general than the types we have been writing so far. It is

424This is more general than the types we have been writing so far. It is

425+parameterised over an underying computation context ``m``, a

428−parameterised over a result type ``x``, as we have already seen, but

426+result type ``t`` as we have already seen, as well as a ``List EFFECT`` and a

429−also a ``List EFFECT`` and a function type ``x -> List EFFECT``.

427+function type ``t -> List EFFECT``.

430

428

431These additional parameters are the list of *input* effects, and a

429These additional parameters are the list of *input* effects, and a

432list of *output* effects, computed from the result of an effectful

430list of *output* effects, computed from the result of an effectful

@@ -435,8 +433,7 @@ of effects available! This is a particularly powerful idea, and we

435will see its consequences in more detail later. Some examples of

433will see its consequences in more detail later. Some examples of

436operations which can change the set of available effects are:

434operations which can change the set of available effects are:

437

435

438−- Updating a state containing a dependent type (for example adding an

436+- Updating a state containing a dependent type (for example adding an element to a vector).

439− element to a vector).

440

437

441- Opening a file for reading is an effect, but whether the file really

438- Opening a file for reading is an effect, but whether the file really

442 *is* open afterwards depends on whether the file was successfully

439 *is* open afterwards depends on whether the file was successfully

@@ -445,19 +442,25 @@ operations which can change the set of available effects are:

445- Closing a file means that reading from the file should no longer be

442- Closing a file means that reading from the file should no longer be

446 possible.

443 possible.

447

444

448−While powerful, this can make uses of the ``Eff`` type hard to read.

445+While powerful, this can make uses of the ``EffM`` type hard to read.

449−Therefore, the library provides syntactic sugar which is translated

446+Therefore the library provides an overloaded function ``Eff``

450−such that:

447+There are the following three versions:

451

448

452.. code-block:: idris

449.. code-block:: idris

453

450

454− { xs } Eff a

451+ SimpleEff.Eff : (t : Type) -> (input_effs : List EFFECT) -> Type

452+ TransEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->

453+ (output_effs : List EFFECT) -> Type

454+ DepEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->

455+ (output_effs_fn : x -> List EFFECT) -> Type

455

456

456−is expanded to

457+So far, we have used only the first version, ``SimpleEff.Eff``, which

458+is defined as follows:

457

459

458.. code-block:: idris

460.. code-block:: idris

459

461

460− Eff a xs (\_ => xs)

462+ Eff : (x : Type) -> (es : List EFFECT) -> Type

463+ Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)

461

464

462i.e. the set of effects remains the same on output. This suffices for

465i.e. the set of effects remains the same on output. This suffices for

463the ``STATE`` example we have seen so far, and for many useful

466the ``STATE`` example we have seen so far, and for many useful

@@ -467,19 +470,19 @@ with the expanded type:

467.. code-block:: idris

470.. code-block:: idris

468

471

469 treeTagAux : BTree a ->

472 treeTagAux : BTree a ->

470− Eff (BTree (Int, a)) [STATE Int] (\x => [STATE Int])

473+ EffM m (BTree (Int, a)) [STATE Int] (\x => [STATE Int])

471

474

472Later, we will see programs which update effects:

475Later, we will see programs which update effects:

473

476

474.. code-block:: idris

477.. code-block:: idris

475

478

476− { xs ==> xs' } Eff a

479+ Eff a xs xs'

477

480

478which is expanded to

481which is expanded to

479

482

480.. code-block:: idris

483.. code-block:: idris

481

484

482− Eff a xs (\_ => xs')

485+ EffM m a xs (\_ => xs')

483

486

484i.e. the set of effects is updated to ``xs’`` (think of a transition

487i.e. the set of effects is updated to ``xs’`` (think of a transition

485in a state machine). There is, for example, a version of ``put`` which

488in a state machine). There is, for example, a version of ``put`` which

@@ -487,22 +490,27 @@ updates the type of the state:

487

490

488.. code-block:: idris

491.. code-block:: idris

489

492

490− putM : y -> { [STATE x] ==> [STATE y] } Eff ()

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

491

494

492Also, we have:

495Also, we have:

493

496

494.. code-block:: idris

497.. code-block:: idris

495

498

496− { xs ==> {res} xs' } Eff a

499+ Eff t xs (\res => xs')

497

500

498which is expanded to

501which is expanded to

499

502

500.. code-block:: idris

503.. code-block:: idris

501

504

502− Eff a xs (\res => xs')

505+ EffM m t xs (\res => xs')

503

506

504i.e. the set of effects is updated according to the result of the

507i.e. the set of effects is updated according to the result of the

505−operation ``res``.

508+operation ``res``, of type ``t``.

509+

510+Parameterising ``EffM`` over an underlying computation context allows us

511+to write effectful programs which are specific to one context, and in some

512+cases to write programs which *extend* the list of effects available using

513+the ``new`` function, though this is beyond the scope of this tutorial.

506

514

507.. [1] The earlier paper [3]_ describes the essential implementation

515.. [1] The earlier paper [3]_ describes the essential implementation

508 details, although the library presented there is an earlier version

516 details, although the library presented there is an earlier version