35958e3 · Idris-dev · git.iko.soy

docs/effects/depeff.rst+1−1

compare with master

unifiedsplit

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

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

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

185

186− instance Handler FileIO IO

186+ Handler FileIO IO where { ... }

187

188In particular, consider the type of ``open``:

189

docs/effects/hangman.rst+1−1

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

193

194.. code-block:: idris

195

196− instance Handler MysteryRules m where

196+ Handler MysteryRules m where

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

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

199

docs/effects/impleff.rst+13−13

@@ -93,16 +93,16 @@ Recall that to run an effectful program in ``Eff``, we use one of the

93``run`` family of functions to run the program in a particular

94computation context ``m``. For each effect, therefore, we must explain

95how it is executed in a particular computation context for ``run`` to

96−work in that context. This is achieved with the following type class:

96+work in that context. This is achieved with the following interface:

97

98.. code-block:: idris

99

100− class Handler (e : Effect) (m : Type -> Type) where

100+ interface Handler (e : Effect) (m : Type -> Type) where

101 handle : resource -> (eff : e t resource resource') ->

102 ((x : t) -> resource' x -> m a) -> m a

103

104−We have already seen some instance declarations in the effect

104+We have already seen some implementation declarations in the effect

105−summaries in Section :ref:`sect-simpleff`. An instance of ``Handler e

105+summaries in Section :ref:`sect-simpleff`. An implementation of ``Handler e

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

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

108

@@ -123,7 +123,7 @@ in the case of ``Get``, or passes on a new state, in the case of

123

124.. code-block:: idris

125

126− instance Handler State m where

126+ Handler State m where

127 handle st Get k = k st st

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

129

@@ -176,7 +176,7 @@ The following listing summarises what is required to define the

176 STATE : Type -> EFFECT

177 STATE t = MkEff t State

178

179− instance Handler State m where

179+ Handler State m where

180 handle st Get k = k st st

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

182

@@ -211,13 +211,13 @@ directly.

211 PutCh : Char -> sig StdIO ()

212 GetCh : sig StdIO Char

213

214− instance Handler StdIO IO where

214+ Handler StdIO IO where

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

216 handle () GetStr k = do x <- getLine; k x ()

217 handle () (PutCh c) k = do putChar c; k () ()

218 handle () GetCh k = do x <- getChar; k x ()

219

220− instance Handler StdIO (IOExcept a) where

220+ Handler StdIO (IOExcept a) where

221 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

222 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

223 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

@@ -241,10 +241,10 @@ error.

241 data Exception : Type -> Effect where

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

243

244− instance Handler (Exception a) Maybe where

244+ Handler (Exception a) Maybe where

245 handle _ (Raise e) k = Nothing

246

247− instance Handler (Exception a) List where

247+ Handler (Exception a) List where

248 handle _ (Raise e) k = []

249

250 EXCEPTION : Type -> EFFECT

@@ -265,14 +265,14 @@ value.

265 data Selection : Effect where

266 Select : List a -> sig Selection a

267

268− instance Handler Selection Maybe where

268+ Handler Selection Maybe where

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

270 tryAll [] = Nothing

271 tryAll (x :: xs) = case k x () of

272 Nothing => tryAll xs

273 Just v => Just v

274

275− instance Handler Selection List where

275+ Handler Selection List where

276 handle r (Select xs) k = concatMap (\x => k x r) xs

277

278 SELECT : EFFECT

@@ -308,7 +308,7 @@ the equivalent ``Eff`` programs.

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

309 EOF : sig FileIO Bool (OpenFile Read)

310

311− instance Handler FileIO IO where

311+ Handler FileIO IO where

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

313 if !(validFile h)

314 then k True (FH h)

docs/effects/simpleeff.rst+12−12

@@ -19,9 +19,9 @@ in a module ``Effect.State``

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

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

21

22− instance Handler State m

22+ Handler State m where { ... }

23

24−The last line, ``instance Handler State m``, means that the ``STATE``

24+The last line, ``Handler State m where { ... }``, means that the ``STATE``

25effect is usable in any computation context ``m``. That is, a program

26which uses this effect and returns something of type ``a`` can be

27evaluated to something of type ``m a`` using ``run``, for any

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

63 getStr : Eff String [STDIO]

64 getChar : Eff Char [STDIO]

65

66− instance Handler StdIO IO

66+ Handler StdIO IO where { ... }

67− instance Handler StdIO (IOExcept a)

67+ Handler StdIO (IOExcept a) where { ... }

68

69Examples

70--------

@@ -148,11 +148,11 @@ generally:

148

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

150

151− instance Handler (Exception a) Maybe

151+ Handler (Exception a) Maybe where { ... }

152− instance Handler (Exception a) List

152+ Handler (Exception a) List where { ... }

153− instance Handler (Exception a) (Either a)

153+ Handler (Exception a) (Either a) where { ... }

154− instance Handler (Exception a) (IOExcept a)

154+ Handler (Exception a) (IOExcept a) where { ... }

155− instance Show a => Handler (Exception a) IO

155+ Show a => Handler (Exception a) IO where { ... }

156

157Example

158-------

@@ -247,7 +247,7 @@ Random number generation is also implemented by the library, in module

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

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

249

250− instance Handler Random m

250+ Handler Random m where { ... }

251

252Random number generation is considered side-effecting because its

253implementation generally relies on some external source of randomness.

@@ -333,8 +333,8 @@ succeeds:

333

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

335

336− instance Handler Selection Maybe

336+ Handler Selection Maybe where { ... }

337− instance Handler Selection List

337+ Handler Selection List where { ... }

338

339Example

340-------

docs/effects/state.rst+6−6

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

189 data BTree a = Leaf

190 | Node (BTree a) a (BTree a)

191

192− instance Show a => Show (BTree a) where

192+ Show a => Show (BTree a) where

193 show Leaf = "[]"

194 show (Node l x r) = "[" ++ show l ++ " "

195 ++ show x ++ " "

@@ -231,19 +231,19 @@ here for illustrative purposes):

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

232

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

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

234+possible using default values given by implementations of the following

235−class:

235+interface:

236

237.. code-block:: idris

238

239− class Default a where

239+ interface Default a where

240 default : a

241

242−Instances of ``Default`` are defined for all primitive types, and many

242+Implementations of ``Default`` are defined for all primitive types, and many

243library types such as ``List``, ``Vect``, ``Maybe``, pairs, etc.

244However, where no default value exists for a resource type (for

245example, you may want a ``STATE`` type for which there is no

246−``Default`` instance) the resource environment can be given explicitly

246+``Default`` implementation) the resource environment can be given explicitly

247using one of the following functions:

248

249.. code-block:: idris

docs/effects/summary.rst+14−14

@@ -22,11 +22,11 @@ EXCEPTION

22

23 raise : a -> Eff b [EXCEPTION a]

24

25− instance Handler (Exception a) Maybe

25+ Handler (Exception a) Maybe where { ... }

26− instance Handler (Exception a) List

26+ Handler (Exception a) List where { ... }

27− instance Handler (Exception a) (Either a)

27+ Handler (Exception a) (Either a) where { ... }

28− instance Handler (Exception a) (IOExcept a)

28+ Handler (Exception a) (IOExcept a) where { ... }

29− instance Show a => Handler (Exception a) IO

29+ Show a => Handler (Exception a) IO where { ... }

30

31FILE\_IO

32========

@@ -54,7 +54,7 @@ FILE\_IO

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

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

56

57− instance Handler FileIO IO

57+ Handler FileIO IO where { ... }

58

59RND

60===

@@ -73,7 +73,7 @@ RND

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

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

75

76− instance Handler Random m

76+ Handler Random m where { ... }

77

78SELECT

79======

@@ -88,8 +88,8 @@ SELECT

88

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

90

91− instance Handler Selection Maybe

91+ Handler Selection Maybe where { ... }

92− instance Handler Selection List

92+ Handler Selection List where { ... }

93

94STATE

95=====

@@ -107,7 +107,7 @@ STATE

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

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

109

110− instance Handler State m

110+ Handler State m where { ... }

111

112STDIO

113=====

@@ -128,8 +128,8 @@ STDIO

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

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

130

131− instance Handler StdIO IO

131+ Handler StdIO IO where { ... }

132− instance Handler StdIO (IOExcept a)

132+ Handler StdIO (IOExcept a) where { ... }

133

134SYSTEM

135======

@@ -148,5 +148,5 @@ SYSTEM

148 time : Handler System e => Eff e Int [SYSTEM]

149 getEnv : Handler System e => String -> Eff e (Maybe String) [SYSTEM]

150

151− instance Handler System IO

151+ Handler System IO where { ... }

152− instance Handler System (IOExcept a)

152+ Handler System (IOExcept a) where { ... }

docs/faq/faq.rst+1−1

@@ -11,7 +11,7 @@ However, Idris has been designed from the start to emphasise general purpose

11programming rather than theorem proving. As such, it supports interoperability

12with systems libraries and C programs, and language constructs for

13domain specific language implementation. It also includes higher level

14−programming constructs such as type classes and do notation.

14+programming constructs such as interfaces (similar to type classes) and do notation.

15

16Idris supports multiple back ends (C and JavaScript by default, with the

17ability to add more via plugins) and has a reference run time system, written

docs/proofs/patterns.rst+2−2

@@ -181,8 +181,8 @@ For ``plus_commutes_Z_rhs_2``, we now see:

181 --------------------------------------

182 plus_commutes_Z_rhs_2 : S k = S (plus k 0)

183

184−Again, the ``fromInteger 0`` is merely due to ``Nat`` being an instance

184+Again, the ``fromInteger 0`` is merely due to ``Nat`` having an implementation

185−of the ``Num`` typeclass. So we know that ``k = plus k 0``, but how do

185+of the ``Num`` interface. So we know that ``k = plus k 0``, but how do

186we use this to update the goal to ``S k = S k``?

187

188To achieve this, Idris provides a ``replace`` function as part of the

docs/proofs/pluscomm.rst+1−1

@@ -177,7 +177,7 @@ given above as Idris type declarations:

177

178Both of these properties (and many others) are proved for natural number

179addition in the Idris standard library, using ``(+)`` from the ``Num``

180−type class rather than using ``plus`` directly. They have the names

180+interface rather than using ``plus`` directly. They have the names

181``plusCommutative`` and ``plusAssociative`` respectively.

182

183In the remainder of this tutorial, we will explore several different

docs/reference/language-features.rst+1−1

@@ -27,7 +27,7 @@ Core Language Features

27- Heterogeneous equality

28- ``do`` notation

29- Idiom brackets

30−- Type classes, supporting default methods and dependencies between

30+- Interfaces (like type classes), supporting default methods and dependencies between

31 methods

32- ``rewrite`` prf ``in`` expr

33- Metavariables