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

git.iko.soy/Idris-dev

class->interface change in rest of tutorial

Including effects/tactics

commit35958e38c145a0c825e41c0b0576629269918a6a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 20 Jan 2016, 15:32 (11 years ago) parent23a2bfb

10 files changed+52−52

compare with master

unifiedsplit

docs/effects/depeff.rst+1−1 docs/effects/hangman.rst+1−1 docs/effects/impleff.rst+13−13 docs/effects/simpleeff.rst+12−12 docs/effects/state.rst+6−6 docs/effects/summary.rst+14−14 docs/faq/faq.rst+1−1 docs/proofs/patterns.rst+2−2 docs/proofs/pluscomm.rst+1−1 docs/reference/language-features.rst+1−1

docs/effects/depeff.rst+1−1

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

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

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

185185

186− instance Handler FileIO IO

186+ Handler FileIO IO where { ... }

187187

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

189189

docs/effects/hangman.rst+1−1

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

193193

194194.. code-block:: idris

195195

196− instance Handler MysteryRules m where

196+ Handler MysteryRules m where

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

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

199199

docs/effects/impleff.rst+13−13

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

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

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

9595how 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:

9797

9898.. code-block:: idris

9999

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

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

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

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

103103

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

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

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

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

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

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

108108

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

123123

124124.. code-block:: idris

125125

126− instance Handler State m where

126+ Handler State m where

127127 handle st Get k = k st st

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

129129

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

176176 STATE : Type -> EFFECT

177177 STATE t = MkEff t State

178178

179− instance Handler State m where

179+ Handler State m where

180180 handle st Get k = k st st

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

182182

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

211211 PutCh : Char -> sig StdIO ()

212212 GetCh : sig StdIO Char

213213

214− instance Handler StdIO IO where

214+ Handler StdIO IO where

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

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

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

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

219219

220− instance Handler StdIO (IOExcept a) where

220+ Handler StdIO (IOExcept a) where

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

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

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

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

241241 data Exception : Type -> Effect where

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

243243

244− instance Handler (Exception a) Maybe where

244+ Handler (Exception a) Maybe where

245245 handle _ (Raise e) k = Nothing

246246

247− instance Handler (Exception a) List where

247+ Handler (Exception a) List where

248248 handle _ (Raise e) k = []

249249

250250 EXCEPTION : Type -> EFFECT

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

265265 data Selection : Effect where

266266 Select : List a -> sig Selection a

267267

268− instance Handler Selection Maybe where

268+ Handler Selection Maybe where

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

270270 tryAll [] = Nothing

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

272272 Nothing => tryAll xs

273273 Just v => Just v

274274

275− instance Handler Selection List where

275+ Handler Selection List where

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

277277

278278 SELECT : EFFECT

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

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

309309 EOF : sig FileIO Bool (OpenFile Read)

310310

311− instance Handler FileIO IO where

311+ Handler FileIO IO where

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

313313 if !(validFile h)

314314 then k True (FH h)

docs/effects/simpleeff.rst+12−12

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

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

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

2121

22− instance Handler State m

22+ Handler State m where { ... }

2323

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

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

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

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

2727evaluated 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:

6363 getStr : Eff String [STDIO]

6464 getChar : Eff Char [STDIO]

6565

66− instance Handler StdIO IO

67− instance Handler StdIO (IOExcept a)

66+ Handler StdIO IO where { ... }

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

6868

6969Examples

7070--------

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

148148

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

150150

151− instance Handler (Exception a) Maybe

152− instance Handler (Exception a) List

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

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

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

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

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

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

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

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

156156

157157Example

158158-------

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

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

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

249249

250− instance Handler Random m

250+ Handler Random m where { ... }

251251

252252Random number generation is considered side-effecting because its

253253implementation generally relies on some external source of randomness.

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

333333

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

335335

336− instance Handler Selection Maybe

337− instance Handler Selection List

336+ Handler Selection Maybe where { ... }

337+ Handler Selection List where { ... }

338338

339339Example

340340-------

docs/effects/state.rst+6−6

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

189189 data BTree a = Leaf

190190 | Node (BTree a) a (BTree a)

191191

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

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

193193 show Leaf = "[]"

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

195195 ++ show x ++ " "

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

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

232232

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

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

235−class:

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

235+interface:

236236

237237.. code-block:: idris

238238

239− class Default a where

239+ interface Default a where

240240 default : a

241241

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

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

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

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

245245example, 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

247247using one of the following functions:

248248

249249.. code-block:: idris

docs/effects/summary.rst+14−14

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

2222

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

2424

25− instance Handler (Exception a) Maybe

26− instance Handler (Exception a) List

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

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

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

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

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

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

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

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

3030

3131FILE\_IO

3232========

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

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

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

5656

57− instance Handler FileIO IO

57+ Handler FileIO IO where { ... }

5858

5959RND

6060===

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

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

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

7575

76− instance Handler Random m

76+ Handler Random m where { ... }

7777

7878SELECT

7979======

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

8888

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

9090

91− instance Handler Selection Maybe

92− instance Handler Selection List

91+ Handler Selection Maybe where { ... }

92+ Handler Selection List where { ... }

9393

9494STATE

9595=====

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

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

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

109109

110− instance Handler State m

110+ Handler State m where { ... }

111111

112112STDIO

113113=====

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

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

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

130130

131− instance Handler StdIO IO

132− instance Handler StdIO (IOExcept a)

131+ Handler StdIO IO where { ... }

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

133133

134134SYSTEM

135135======

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

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

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

150150

151− instance Handler System IO

152− instance Handler System (IOExcept a)

151+ Handler System IO where { ... }

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

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

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

1313domain 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.

1515

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

1717ability 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:

181181 --------------------------------------

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

183183

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

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

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

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

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

187187

188188To 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:

177177

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

179179addition 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

181181``plusCommutative`` and ``plusAssociative`` respectively.

182182

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

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

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

2727- Heterogeneous equality

2828- ``do`` notation

2929- Idiom brackets

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

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

3131 methods

3232- ``rewrite`` prf ``in`` expr

3333- Metavariables