ef50150 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Updates

ef50150Jan de Muijnck-Hughes12 years ago

docs/effects/conclusions.rst+11−10

compare with master

unifiedsplit

@@ -5,12 +5,13 @@ Further Reading

5===============

7This tutorial has given an introduction to writing and reasoning about

8−side-effecting programs in , using the library. More details about the

8+side-effecting programs in ``Idris``, using the ``Effects`` library.

9−*implementation* of the library, such as how ``run`` works, how handlers

9+More details about the *implementation* of the library, such as how

10−are invoked, etc, are given in a separate paper [1]_.

10+``run`` works, how handlers are invoked, etc, are given in a separate

11+paper [1]_.

12−Some libraries and programs which use can be found in the following

13+Some libraries and programs which use ``Effects`` can be found in the

13−places:

14+following places:

15- http://github.com/edwinb/SDL-idris — some bindings for the SDL media

16- http://github.com/edwinb/SDL-idris — some bindings for the SDL media

16 library, supporting graphics in particular.

17 library, supporting graphics in particular.

@@ -25,11 +26,11 @@ places:

25- http://github.com/edwinb/Protocols — a high level communication

26- http://github.com/edwinb/Protocols — a high level communication

26 protocol description language.

27 protocol description language.

28−The inspiration for the library was Bauer and Pretnar’s Eff language

29+The inspiration for the ``Effects`` library was Bauer and Pretnar’s

29−[2]_, which describes a langauge based on algebraic effects and

30+Eff language [2]_, which describes a langauge based on algebraic

30−handlers. Other recent languages and libraries have also been built

31+effects and handlers. Other recent languages and libraries have also

31−on this ideas, e.g. [3]_, [4]_. The theoretical foundations are also

32+been built on this ideas, for example [3]_ and [4]_. The theoretical

32−well-studied [5]_, [6]_, [7]_, [8]_.

33+foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.

docs/effects/depeff.rst+12−10

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

80Unfortunately, this will not type check because the vector does not get

81extended in both branches of the ``case``!

83−.. code-block:: idris

83+::

85 MutState.idr:18:19:When elaborating right hand side of Main.case

86 block in readInt:

@@ -127,10 +127,11 @@ many values still need to be read into the vector. What this means in

127practice is that the type system has verified that a necessary dynamic

128check (i.e. whether reading a value succeeded) has indeed been done.

129

130+.. note::

130−**Aside:** Only ``case`` will work here. We cannot use ``if/then/else``

131+ Only ``case`` will work here. We cannot use ``if/then/else``

131−because the ``then`` and ``else`` branches must have the same type. The

132+ because the ``then`` and ``else`` branches must have the same

132−``case`` construct, however, abstracts over the value being inspected in

133+ type. The ``case`` construct, however, abstracts over the value

133−the type of each branch.

134+ being inspected in the type of each branch.

134

135

135File Management

136File Management

136---------------

137---------------

@@ -231,7 +232,7 @@ for writing) then we will get a compile-time error. For example,

231changing ``open name Read`` to ``open name Write`` yields a compile-time

232changing ``open name Read`` to ``open name Write`` yields a compile-time

232error of the following form:

233error of the following form:

233

234

234−.. code-block:: idris

235+::

235

236

236 FileTest.idr:16:18:When elaborating right hand side of Main.case

237 FileTest.idr:16:18:When elaborating right hand side of Main.case

237 block in testFile:

238 block in testFile:

@@ -275,14 +276,14 @@ example, we could write:

275 close

276 close

276

277

277This is exactly equivalent to the definition with the explicit ``case``.

278This is exactly equivalent to the definition with the explicit ``case``.

278−In general, in a ``do``-block, the syntax…

279+In general, in a ``do``-block, the syntax:

279

280

280.. code-block:: idris

281.. code-block:: idris

281

282

282 do pat <- val | <alternatives>

283 do pat <- val | <alternatives>

283 p

284 p

284

285

285−...is desugared to...

286+is desugared to

286

287

287.. code-block:: idris

288.. code-block:: idris

288

289

@@ -292,8 +293,9 @@ In general, in a ``do``-block, the syntax…

292 <alternatives>

293 <alternatives>

293

294

294There can be several ``alternatives``, separated by a vertical bar

295There can be several ``alternatives``, separated by a vertical bar

295−``|``. For example, there is a ``SYSTEM`` effect which supports reading

296+``|``. For example, there is a ``SYSTEM`` effect which supports

297+reading command line arguments, among other things (see Appendix

296−command line arguments, among other things (see Appendix :ref:`sect-appendix`). To read command line arguments, we can use

298+:ref:`sect-appendix`). To read command line arguments, we can use

297``getArgs``:

299``getArgs``:

298

300

299.. code-block:: idris

301.. code-block:: idris

docs/effects/hangman.rst+30−27

@@ -231,8 +231,8 @@ presented in Listing :ref:`mword`.

231Note that the type of ``game`` makes no assumption that there are

232letters to be guessed in the given word (i.e. it is ``w`` rather than

233``S w``). This is because we will be choosing a word at random from a

234−vector of ``String``\ s, and at no point have we made it explicit that

234+vector of ``String``, and at no point have we made it explicit that

235−those ``String``\ s are non-empty.

235+those ``String`` are non-empty.

236

237Finally, we need to initialise the game by picking a word at random from

238a list of candidates, setting it as the target using ``NewWord``, then

@@ -248,9 +248,9 @@ running ``game``:

248 putStrLn !StrState

249

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

251−Appendix :ref:`sect-appendix`) to initialise the random number generator,

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

252−then pick a random ``Fin`` to index into a list of ``words``. For

252+generator, then pick a random ``Fin`` to index into a list of

253−example, we could initialise a word list as follows:

253+``words``. For example, we could initialise a word list as follows:

254

255.. code-block:: idris

256

@@ -261,10 +261,11 @@ example, we could initialise a word list as follows:

261

262 wtype = proof search

263

264+.. note::

264−**Aside:** Rather than have to explicitly declare a type with the

265+ Rather than have to explicitly declare a type with the vector’s

265−vector’s length, it is convenient to give a metavariable ``?wtype`` and

266+ length, it is convenient to give a metavariable ``?wtype`` and let

266−let ``Idris``’s proof search mechanism find the type. This is a limited form of

267+ ``Idris``’s proof search mechanism find the type. This is a

267−type inference, but very useful in practice.

268+ limited form of type inference, but very useful in practice.

268

269

270

270.. _mword:

271.. _mword:

@@ -300,32 +301,34 @@ type inference, but very useful in practice.

300Discussion

301Discussion

301----------

302----------

302

303

303−Writing the rules separately as an effect, then an implementation which

304+Writing the rules separately as an effect, then an implementation

304−uses that effect, ensures that the implementation must follow the rules.

305+which uses that effect, ensures that the implementation must follow

305−This has practical applications in more serious contexts;

306+the rules. This has practical applications in more serious contexts;

306−``MysteryRules`` for example can be though of as describing a *protocol*

307+``MysteryRules`` for example can be though of as describing a

307−that a game player most follow, or alternative a *precisely-typed API*.

308+*protocol* that a game player most follow, or alternative a

309+*precisely-typed API*.

308

310

309In practice, we wouldn’t really expect to write rules first then

311In practice, we wouldn’t really expect to write rules first then

310−implement the game once the rules were complete. Indeed, I didn’t do so

312+implement the game once the rules were complete. Indeed, I didn’t do

311−when constructing this example! Rather, I wrote down a set of likely

313+so when constructing this example! Rather, I wrote down a set of

312−rules making any assumptions *explicit* in the state transitions for

314+likely rules making any assumptions *explicit* in the state

313−``MysteryRules``. Then, when implementing ``game`` at first, any

315+transitions for ``MysteryRules``. Then, when implementing ``game`` at

314−incorrect assumption was caught as a type error. The following errors

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

315−were caught during development:

317+following errors were caught during development:

316−

318+

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

319+- Not realising that allowing ``NewWord`` to be an arbitrary string

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

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

319 as a starting state.

321 as a starting state.

320

322

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

323+- Forgetting to check whether a game was won before recursively

322− ``processGuess``, thus accidentally continuing a finished game.

324+ calling ``processGuess``, thus accidentally continuing a finished

325+ game.

323

326

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

327+- Accidentally checking the number of missing letters, rather than the

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

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

326

329

327−These are, of course, simple errors, but were caught by the type checker

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

328−before any testing of the game.

331+checker before any testing of the game.

329

332

330.. [1]

333.. [1]

331 Readers may recognise this game by the name “Hangman.”

334 Readers may recognise this game by the name “Hangman.”

docs/effects/impleff.rst+53−51

@@ -16,9 +16,9 @@ effectful operations may be provided.

16State

17-----

19−Effects are described by *algebraic data types*, where the constructors

19+Effects are described by *algebraic data types*, where the

20−describe the operations provided when the effect is available. Stateful

20+constructors describe the operations provided when the effect is

21−operations are described as follows:

21+available. Stateful operations are described as follows:

23.. code-block:: idris

@@ -26,18 +26,19 @@ operations are described as follows:

26 Get : { a } State a

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

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

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

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

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

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

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

32−is run. Here, it means:

32+operation is run. Here, it means:

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

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

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

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

36− type ``a``.

36+ of type ``a``.

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

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

39− on input, which is updated to a resource of type ``b``. Running the

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

40− ``Put`` operation returns the element of the unit type.

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

41+ unit type.

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

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

@@ -61,8 +62,8 @@ declarations more readable. It is defined as follows in the library:

61 = eff inst (\b => outst)

62 = eff inst (\b => outst)

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

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

64−In order to convert ``State`` (of type ``Effect``) into something usable

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

65−in an effects list, of type ``EFFECT``, we write the following:

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

67.. code-block:: idris

68.. code-block:: idris

@@ -70,8 +71,8 @@ in an effects list, of type ``EFFECT``, we write the following:

70 STATE t = MkEff t State

71 STATE t = MkEff t State

72``MkEff`` constructs an ``EFFECT`` by taking the resource type (here,

73``MkEff`` constructs an ``EFFECT`` by taking the resource type (here,

73−the ``t`` which parameterises ``STATE``) and the effect signature (here,

74+the ``t`` which parameterises ``STATE``) and the effect signature

74−``State``). For reference, ``EFFECT`` is declared as follows:

75+(here, ``State``). For reference, ``EFFECT`` is declared as follows:

76.. code-block:: idris

77.. code-block:: idris

@@ -90,27 +91,27 @@ work in that context. This is achieved with the following type class:

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

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

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

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

93−We have already seen some instance declarations in the effect summaries

94+We have already seen some instance declarations in the effect

94−in Section [sect:simpleff]. An instance of ``Handler e m`` means that

95+summaries in Section :ref:`sect-simpleff`. An instance of ``Handler e

95−the effect declared with signature ``e`` can be run in computation

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

96−context ``m``. The ``handle`` function takes:

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

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

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

99 ``State``)

100 ``State``)

100

101

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

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

102

103

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

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

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

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

105

106

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

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

107−neater because there are multiple return values (a new resource and the

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

108−result of the operation); secondly, and more importantly, the

109+the result of the operation); secondly, and more importantly, the

109continuation can be called zero or more times.

110continuation can be called zero or more times.

110

111

111−A ``Handler`` for ``State`` simply passes on the value of the state, in

112+A ``Handler`` for ``State`` simply passes on the value of the state,

112−the case of ``Get``, or passes on a new state, in the case of ``Put``.

113+in the case of ``Get``, or passes on a new state, in the case of

113−It is defined the same way for all computation contexts:

114+``Put``. It is defined the same way for all computation contexts:

114

115

115.. code-block:: idris

116.. code-block:: idris

116

117

@@ -133,10 +134,10 @@ functions in ``Eff``, as follows:

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

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

134 putM val = call (Put val)

135 putM val = call (Put val)

135

136

136−**An implementation detail (aside):** The ``call`` function converts an

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

137−``Effect`` to a function in ``Eff``, given a proof that the effect is

138+an ``Effect`` to a function in ``Eff``, given a proof that the effect

138−available. This proof can be constructed automatically by , since it is

139+is available. This proof can be constructed automatically by , since

139−essentially an index into a statically known list of effects:

140+it is essentially an index into a statically known list of effects:

140

141

141.. code-block:: idris

142.. code-block:: idris

142

143

@@ -144,10 +145,10 @@ essentially an index into a statically known list of effects:

144 (eff : e t a b) -> {auto prf : EffElem e a xs} ->

145 (eff : e t a b) -> {auto prf : EffElem e a xs} ->

145 Eff t xs (\v => updateResTy v xs prf eff)

146 Eff t xs (\v => updateResTy v xs prf eff)

146

147

147−This is the reason for the ``Can’t solve goal`` error when an effect is

148+This is the reason for the ``Can’t solve goal`` error when an effect

148−not available: the implicit proof ``prf`` has not been solved

149+is not available: the implicit proof ``prf`` has not been solved

149−automatically because the required effect is not in the list of effects

150+automatically because the required effect is not in the list of

150−``xs``.

151+effects ``xs``.

151

152

152Such details are not important for using the library, or even writing

153Such details are not important for using the library, or even writing

153new effects, however.

154new effects, however.

@@ -186,10 +187,10 @@ Listing :ref:`eff-statedef` summarises what is required to define the

186Console I/O

187Console I/O

187-----------

188-----------

188

189

189−Listing :ref:`eff-stdiodef` gives the definition of the ``STDIO`` effect,

190+Listing :ref:`eff-stdiodef` gives the definition of the ``STDIO``

190−including handlers for ``IO`` and ``IOExcept``. We omit the definition

191+effect, including handlers for ``IO`` and ``IOExcept``. We omit the

191−of the top level ``Eff`` functions, as this merely invoke the effects

192+definition of the top level ``Eff`` functions, as this merely invoke

192−``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.

193+the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.

193

194

194Note that in this case, the resource is the unit type in every case,

195Note that in this case, the resource is the unit type in every case,

195since the handlers merely apply the ``IO`` equivalents of the effects

196since the handlers merely apply the ``IO`` equivalents of the effects

@@ -269,10 +270,11 @@ Non-determinism

269 SELECT : EFFECT

270 SELECT : EFFECT

270 SELECT = MkEff () Selection

271 SELECT = MkEff () Selection

271

272

272−Listing :ref:`eff-selectdef` gives the definition of the ``Select`` effect

273+Listing :ref:`eff-selectdef` gives the definition of the ``Select``

273−for writing non-deterministic programs, including a handler for ``List``

274+effect for writing non-deterministic programs, including a handler for

274−context which returns all possible successful values, and a handler for

275+``List`` context which returns all possible successful values, and a

275−``Maybe`` context which returns the first successful value.

276+handler for ``Maybe`` context which returns the first successful

277+value.

276

278

277Here, the continuation is called multiple times in each handler, for

279Here, the continuation is called multiple times in each handler, for

278each value in the list of possible values. In the ``List`` handler, we

280each value in the list of possible values. In the ``List`` handler, we

@@ -282,12 +284,12 @@ the first value in the last, and try later values only if that fails.

282File Management

284File Management

283---------------

285---------------

284

286

285−Result-dependent effects are no different from non-dependent effects in

287+Result-dependent effects are no different from non-dependent effects

286−the way they are implemented. Listing :ref:`eff-filedef` illustrates this for

288+in the way they are implemented. Listing :ref:`eff-filedef`

287−the ``FILE_IO`` effect. The syntax for state transitions

289+illustrates this for the ``FILE_IO`` effect. The syntax for state

288−``{ x ==> {res} x’ }``, where the result state ``x’`` is computed from

290+transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is

289−the result of the operation ``res``, follows that for the equivalent

291+computed from the result of the operation ``res``, follows that for

290−``Eff`` programs.

292+the equivalent ``Eff`` programs.

291

293

292Note that in the handler for ``Open``, the types passed to the

294Note that in the handler for ``Open``, the types passed to the

293continuation ``k`` are different depending on whether the result is

295continuation ``k`` are different depending on whether the result is

docs/effects/introduction.rst+34−32

@@ -2,15 +2,15 @@

2Introduction

3============

5−Pure functional languages with dependent types such as

5+Pure functional languages with dependent types such as `Idris

6−(http://idris-lang.org/) support reasoning about programs directly in

6+<http://idris-lang.org/>`_ support reasoning about programs directly

7−the type system, promising that we can *know* a program will run

7+in the type system, promising that we can *know* a program will run

8correctly (i.e. according to the specification in its type) simply

9because it compiles. Realistically, though, things are not so simple:

10−programs have to interact with the outside world, with user input, input

10+programs have to interact with the outside world, with user input,

11−from a network, mutable state, and so on. In this tutorial I will

11+input from a network, mutable state, and so on. In this tutorial I

12−introduce the library, which is included with the distribution and

12+will introduce the library, which is included with the distribution

13−supports programming and reasoning with side-effecting programs,

13+and supports programming and reasoning with side-effecting programs,

14supporting mutable state, interaction with the outside world,

15exceptions, and verified resource management.

@@ -37,13 +37,13 @@ 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

41 input device.

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

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

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

46−- Write output

46+- Write output

48The complete program will include side-effects for I/O and error

49handling, before we can get to the pure core functionality. In this

@@ -56,7 +56,8 @@ Hello world

56===========

58To give an idea of how programs with effects look in , here is the

59−ubiquitous “Hello world” program, written using the ``Effects`` library:

59+ubiquitous “Hello world” program, written using the ``Effects``

60+library:

61.. code-block:: idris

62.. code-block:: idris

@@ -70,14 +71,14 @@ ubiquitous “Hello world” program, written using the ``Effects`` library:

70 main : IO ()

71 main : IO ()

71 main = run hello

72 main = run hello

73−As usual, the entry point is ``main``. All ``main`` has to do is invoke

74+As usual, the entry point is ``main``. All ``main`` has to do is

74−the ``hello`` function which supports the ``STDIO`` effect for console

75+invoke the ``hello`` function which supports the ``STDIO`` effect for

75−I/O, and returns the unit value. The details of the ``Eff`` type will be

76+console I/O, and returns the unit value. The details of the ``Eff``

76−presented in the remainder of this tutorial.

77+type will be presented in the remainder of this tutorial.

78−To compile and run this program, ``Idris`` needs to be told to include the

79+To compile and run this program, ``Idris`` needs to be told to include

79−``Effects`` package, using the ``-p effects`` flag (this flag is required for all examples

80+the ``Effects`` package, using the ``-p effects`` flag (this flag is

80−in this tutorial):

81+required for all examples in this tutorial):

82.. code-block:: sh

83.. code-block:: sh

@@ -87,20 +88,21 @@ in this tutorial):

87Outline

88Outline

88=======

89=======

90−The tutorial is structured as follows: first, in :ref:`sect-state`, we

91+The tutorial is structured as follows: first, in Section

91−will discuss state management, describing why it is important and

92+:ref:`sect-state`, we will discuss state management, describing why it

92−introducing the ``effects`` library to show how it can be used to

93+is important and introducing the ``effects`` library to show how it

93−manage state. This section also gives an overview of the syntax of

94+can be used to manage state. This section also gives an overview of

94−effectful programs. :ref:`sect-simpleff` then introduces a number of

95+the syntax of effectful programs. Section :ref:`sect-simpleff` then

95−other effects a program may have: I/O; Exceptions; Random Numbers; and

96+introduces a number of other effects a program may have: I/O;

96−Non-determinism, giving examples for each, and an extended example

97+Exceptions; Random Numbers; and Non-determinism, giving examples for

97−combining several effects in one complete program. :ref:`sect-depeff`

98+each, and an extended example combining several effects in one

99+complete program. Section :ref:`sect-depeff` introduces *dependent*

98−introduces *dependent* effects, showing how states and resources can

100+effects, showing how states and resources can be managed in

99−be managed in types. :ref:`sect-impleff` shows how new effects can be

101+types. Section :ref:`sect-impleff` shows how new effects can be

100−implemented. :ref:`sect-hangman` gives an extended example showing

102+implemented. Section :ref:`sect-hangman` gives an extended example

101−how to implement a “mystery word” guessing game, using effects to

103+showing how to implement a “mystery word” guessing game, using effects

102−describe the rules of the game and ensure they are implemented

104+to describe the rules of the game and ensure they are implemented

103−accurately. References to further reading are given in

105+accurately. References to further reading are given in Section

104:ref:`sect-further`.

106:ref:`sect-further`.

105

107

106.. [1]

108.. [1]

docs/effects/simpleeff.rst+109−102

@@ -5,8 +5,8 @@ Simple Effects

5==============

7So far we have seen how to write programs with locally mutable state

8−using the ``STATE`` effect. To recap, we have the definitions in Listing

8+using the ``STATE`` effect. To recap, we have the definitions in

9−:ref:`eff-state` in a module ``Effect.State``.

9+Listing :ref:`eff-state` in a module ``Effect.State``.

11.. _eff-state:

12.. code-block:: idris

@@ -26,17 +26,17 @@ using the ``STATE`` effect. To recap, we have the definitions in Listing

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

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

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

29−evaluated to something of type ``m a`` using ``run``, for any ``m``. The

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

30−lower case ``State`` is a data type describing the operations which make

30+``m``. The lower case ``State`` is a data type describing the

31−up the ``STATE`` effect itself—we will go into more detail about this in

31+operations which make up the ``STATE`` effect itself—we will go into

32−:ref:`sect-impleff`.

32+more detail about this in Section :ref:`sect-impleff`.

34In this section, we will introduce some other supported effects,

35allowing console I/O, exceptions, random number generation and

36non-deterministic programming. For each effect we introduce, we will

37begin with a summary of the effect, its supported operations, and the

38−contexts in which it may be used, like that above for ``STATE``, and go

38+contexts in which it may be used, like that above for ``STATE``, and

39−on to present some simple examples. At the end, we will see some

39+go on to present some simple examples. At the end, we will see some

40examples of programs which combine multiple effects.

42All of the effects in the library, including those described in this

@@ -48,9 +48,9 @@ Console I/O

48Console I/O (Listing :ref:`eff-stdio`) is supported with the ``STDIO``

49effect, which allows reading and writing characters and strings to and

50from standard input and standard output. Notice that there is a

51−constraint here on the computation context ``m``, because it only makes

51+constraint here on the computation context ``m``, because it only

52−sense to support console I/O operations in a context where we can

52+makes sense to support console I/O operations in a context where we

53−perform (or at the very least simulate) console I/O.

53+can perform (or at the very least simulate) console I/O.

55.. _eff-stdio:

56.. code-block:: idris

@@ -83,17 +83,18 @@ as follows:

83 x <- getStr

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

86−We use ``trim`` here to remove the trailing newline from the input. The

86+We use ``trim`` here to remove the trailing newline from the

87−resource associated with ``STDIO`` is simply the empty tuple, which has

87+input. The resource associated with ``STDIO`` is simply the empty

88−a default value ``()``, so we can run this as follows:

88+tuple, which has a default value ``()``, so we can run this as

89+follows:

90.. code-block:: idris

91.. code-block:: idris

92 main : IO ()

93 main : IO ()

93 main = run hello

94 main = run hello

95−In ``hello`` we could also use ``!``-notation instead of

96+In ``hello`` we could also use ``!``-notation instead of ``x <-

96−``x <- getStr``, since we only use the string that is read once:

97+getStr``, since we only use the string that is read once:

98.. code-block:: idris

99.. code-block:: idris

100

@@ -101,8 +102,9 @@ In ``hello`` we could also use ``!``-notation instead of

101 hello = do putStr "Name? "

102 hello = do putStr "Name? "

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

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

103

104

104−More interestingly, we can combine multiple effects in one program. For

105+More interestingly, we can combine multiple effects in one

105−example, we can loop, counting the number of people we’ve said hello to:

106+program. For example, we can loop, counting the number of people we’ve

107+said hello to:

106

108

107.. code-block:: idris

109.. code-block:: idris

108

110

@@ -113,18 +115,18 @@ example, we can loop, counting the number of people we’ve said hello to:

113 putStrLn ("I've said hello to: " ++ show !get ++ " people")

115 putStrLn ("I've said hello to: " ++ show !get ++ " people")

114 hello

116 hello

115

117

116−The list of effects given in ``hello`` means that the function can call

118+The list of effects given in ``hello`` means that the function can

117−``get`` and ``put`` on an integer state, and any functions which read

119+call ``get`` and ``put`` on an integer state, and any functions which

118−and write from the console. To run this, ``main`` does not need to be

120+read and write from the console. To run this, ``main`` does not need

119−changed.

121+to be changed.

120

122

121Aside: Resource Types

123Aside: Resource Types

122~~~~~~~~~~~~~~~~~~~~~

124~~~~~~~~~~~~~~~~~~~~~

123

125

124−To find out the resource type of an effect, if necessary (for example if

126+To find out the resource type of an effect, if necessary (for example

125−we want to initialise a resource explicitiy with ``runInit`` rather than

127+if we want to initialise a resource explicitiy with ``runInit`` rather

126−using a default value with ``run``) we can run the ``resourceType``

128+than using a default value with ``run``) we can run the

127−function at the REPL:

129+``resourceType`` function at the REPL:

128

130

129.. code-block:: idris

131.. code-block:: idris

130

132

@@ -137,8 +139,9 @@ Exceptions

137----------

139----------

138

140

139Listing :ref:`eff-exception` gives the definition of the ``EXCEPTION``

141Listing :ref:`eff-exception` gives the definition of the ``EXCEPTION``

140−effect, declared in module ``Effect.Exception``. This allows programs to

142+effect, declared in module ``Effect.Exception``. This allows programs

141−exit immediately with an error, or errors to be handled more generally.

143+to exit immediately with an error, or errors to be handled more

144+generally.

142

145

143.. _eff-exception:

146.. _eff-exception:

144.. code-block:: idris

147.. code-block:: idris

@@ -180,8 +183,8 @@ paramaterised by an error type:

180

183

181Programs which support the ``EXCEPTION`` effect can be run in any

184Programs which support the ``EXCEPTION`` effect can be run in any

182context which has some way of throwing errors, for example, we can run

185context which has some way of throwing errors, for example, we can run

183−``parseNumber`` in the ``Either Err`` context. It returns a value of the

186+``parseNumber`` in the ``Either Err`` context. It returns a value of

184−form ``Right x`` if successful:

187+the form ``Right x`` if successful:

185

188

186.. code-block:: idris

189.. code-block:: idris

187

190

@@ -198,19 +201,19 @@ Or ``Left e`` on failure, carrying the appropriate exception:

198 *Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")

201 *Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")

199 Left NotANumber : Either Err Int

202 Left NotANumber : Either Err Int

200

203

201−In fact, we can do a little bit better with ``parseNumber``, and have it

204+In fact, we can do a little bit better with ``parseNumber``, and have

202−return a *proof* that the integer is in the required range along with

205+it return a *proof* that the integer is in the required range along

203−the integer itself. One way to do this is define a type of bounded

206+with the integer itself. One way to do this is define a type of

204−integers, ``Bounded``:

207+bounded integers, ``Bounded``:

205

208

206.. code-block:: idris

209.. code-block:: idris

207

210

208 Bounded : Int -> Type

211 Bounded : Int -> Type

209 Bounded x = (n : Int ** So (n >= 0 && n <= x))

212 Bounded x = (n : Int ** So (n >= 0 && n <= x))

210

213

211−Recall that ``So`` is parameterised by a ``Bool``, and only ``So True``

214+Recall that ``So`` is parameterised by a ``Bool``, and only ``So

212−is inhabited. We can use ``choose`` to construct such a value from the

215+True`` is inhabited. We can use ``choose`` to construct such a value

213−result of a dynamic check:

216+from the result of a dynamic check:

214

217

215.. code-block:: idris

218.. code-block:: idris

216

219

@@ -260,32 +263,33 @@ be set with ``srand``. A specific seed will lead to a predictable,

260repeatable sequence of random numbers. There are two functions which

263repeatable sequence of random numbers. There are two functions which

261produce a random number:

264produce a random number:

262

265

263−- ``rndInt``, which returns a random integer between the given lower

266+- ``rndInt``, which returns a random integer between the given lower

264 and upper bounds.

267 and upper bounds.

265

268

266−- ``rndFin``, which returns a random element of a finite set

269+- ``rndFin``, which returns a random element of a finite set

267 (essentially a number with an upper bound given in its type).

270 (essentially a number with an upper bound given in its type).

268

271

269Example

272Example

270~~~~~~~

273~~~~~~~

271

274

272We can use the ``RND`` effect to implement a simple guessing game. The

275We can use the ``RND`` effect to implement a simple guessing game. The

273−``guess`` function, given a target number, will repeatedly ask the user

276+``guess`` function, given a target number, will repeatedly ask the

274−for a guess, and state whether the guess is too high, too low, or

277+user for a guess, and state whether the guess is too high, too low, or

275correct:

278correct:

276

279

277.. code-block:: idris

280.. code-block:: idris

278

281

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

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

280

283

281−For reference, the code for ``guess`` is given in Listing :ref:`eff-game`.

284+For reference, the code for ``guess`` is given in Listing

282−Note that we use ``parseNumber`` as defined previously to read user

285+:ref:`eff-game`. Note that we use ``parseNumber`` as defined

286+previously to read user input, but we don’t need to list the

283−input, but we don’t need to list the ``EXCEPTION`` effect because we use

287+``EXCEPTION`` effect because we use a nested ``run`` to invoke

284−a nested ``run`` to invoke ``parseNumber``, independently of the calling

288+``parseNumber``, independently of the calling effectful program.

285−effectful program.

286

289

287−To invoke these, we pick a random number within the range 0–100, having

290+To invoke these, we pick a random number within the range 0–100,

288−set up the random number generator with a seed, then run ``guess``:

291+having set up the random number generator with a seed, then run

292+``guess``:

289

293

290.. code-block:: idris

294.. code-block:: idris

291

295

@@ -322,9 +326,9 @@ do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.

322Non-determinism

326Non-determinism

323---------------

327---------------

324

328

325−Listing :ref:`eff-select` gives the definition of the non-determinism effect,

329+Listing :ref:`eff-select` gives the definition of the non-determinism

326−which allows a program to choose a value non-deterministically from a

330+effect, which allows a program to choose a value non-deterministically

327−list of possibilities in such a way that the entire computation

331+from a list of possibilities in such a way that the entire computation

328succeeds.

332succeeds.

329

333

330.. _eff-select:

334.. _eff-select:

@@ -344,10 +348,10 @@ succeeds.

344Example

348Example

345~~~~~~~

349~~~~~~~

346

350

347−The ``SELECT`` effect can be used to solve constraint problems, such as

351+The ``SELECT`` effect can be used to solve constraint problems, such

348−finding Pythagorean triples. The idea is to use ``select`` to give a set

352+as finding Pythagorean triples. The idea is to use ``select`` to give

349−of candidate values, then throw an exception for any combination of

353+a set of candidate values, then throw an exception for any combination

350−values which does not satisfy the constraint:

354+of values which does not satisfy the constraint:

351

355

352.. code-block:: idris

356.. code-block:: idris

353

357

@@ -362,14 +366,14 @@ values which does not satisfy the constraint:

362This program chooses a value for ``z`` between ``1`` and ``max``, then

366This program chooses a value for ``z`` between ``1`` and ``max``, then

363values for ``y`` and ``x``. In operation, after a ``select``, the

367values for ``y`` and ``x``. In operation, after a ``select``, the

364program executes the rest of the ``do``-block for every possible

368program executes the rest of the ``do``-block for every possible

365−assignment, effectively searching depth-first. If the list is empty (or

369+assignment, effectively searching depth-first. If the list is empty

366−an exception is thrown) execution fails.

370+(or an exception is thrown) execution fails.

367

371

368There are handlers defined for ``Maybe`` and ``List`` contexts, i.e.

372There are handlers defined for ``Maybe`` and ``List`` contexts, i.e.

369contexts which can capture failure. Depending on the context ``m``,

373contexts which can capture failure. Depending on the context ``m``,

370−``triple`` will either return the first triple it finds (if in ``Maybe``

374+``triple`` will either return the first triple it finds (if in

371−context) or all triples in the range (if in ``List`` context). We can

375+``Maybe`` context) or all triples in the range (if in ``List``

372−try this as follows:

376+context). We can try this as follows:

373

377

374.. code-block:: idris

378.. code-block:: idris

375

379

@@ -391,11 +395,12 @@ definition:

391

395

392Using , we can set up a program so that it reads input from a user,

396Using , we can set up a program so that it reads input from a user,

393checks that the input is valid (i.e both vectors contain integers, and

397checks that the input is valid (i.e both vectors contain integers, and

394−are the same length) and if so, pass it on to ``vadd``. First, we write

398+are the same length) and if so, pass it on to ``vadd``. First, we

395−a wrapper for ``vadd`` which checks the lengths and throw an exception

399+write a wrapper for ``vadd`` which checks the lengths and throw an

396−if they are not equal. We can do this for input vectors of length ``n``

400+exception if they are not equal. We can do this for input vectors of

397−and ``m`` by matching on the implicit arguments ``n`` and ``m`` and

401+length ``n`` and ``m`` by matching on the implicit arguments ``n`` and

398−using ``decEq`` to produce a proof of their equality, if they are equal:

402+``m`` and using ``decEq`` to produce a proof of their equality, if

403+they are equal:

399

404

400.. code-block:: idris

405.. code-block:: idris

401

406

@@ -412,15 +417,16 @@ following type:

412

417

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

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

414

419

415−This returns a dependent pair of a length, and a vector of that length,

420+This returns a dependent pair of a length, and a vector of that

416−because we cannot know in advance how many integers the user is going to

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

417−input. One way to implement this function, using ``-1`` to indicate the

422+is going to input. One way to implement this function, using ``-1`` to

418−end of input, is shown in Listing [readvec]. This uses a variation on

423+indicate the end of input, is shown in Listing [readvec]. This uses a

419−``parseNumber`` which does not require a number to be within range.

424+variation on ``parseNumber`` which does not require a number to be

425+within range.

420

426

421Finally, we write a program which reads two vectors and prints the

427Finally, we write a program which reads two vectors and prints the

422−result of pairwise addition of them, throwing an exception if the inputs

428+result of pairwise addition of them, throwing an exception if the

423−are of differing lengths:

429+inputs are of differing lengths:

424

430

425.. code-block:: idris

431.. code-block:: idris

426

432

@@ -431,11 +437,11 @@ are of differing lengths:

431 (_ ** ys) <- read_vec

437 (_ ** ys) <- read_vec

432 putStrLn (show !(vadd_check xs ys))

438 putStrLn (show !(vadd_check xs ys))

433

439

434−By having explicit lengths in the type, we can be sure that ``vadd`` is

440+By having explicit lengths in the type, we can be sure that ``vadd``

435−only being used where the lengths of inputs are guaranteed to be equal.

441+is only being used where the lengths of inputs are guaranteed to be

436−This does not stop us reading vectors from user input, but it does

442+equal. This does not stop us reading vectors from user input, but it

437−require that the lengths are checked and any discrepancy is dealt with

443+does require that the lengths are checked and any discrepancy is dealt

438−gracefully.

444+with gracefully.

439

445

440.. code-block:: idris

446.. code-block:: idris

441 :caption: Reading a vector from the console.

447 :caption: Reading a vector from the console.

@@ -459,16 +465,17 @@ gracefully.

459Example: An Expression Calculator

465Example: An Expression Calculator

460---------------------------------

466---------------------------------

461

467

462−To show how these effects can fit together, let us consider an evaluator

468+To show how these effects can fit together, let us consider an

463−for a simple expression language, with addition and integer values.

469+evaluator for a simple expression language, with addition and integer

470+values.

464

471

465.. code-block:: idris

472.. code-block:: idris

466

473

467 data Expr = Val Integer

474 data Expr = Val Integer

468 | Add Expr Expr

475 | Add Expr Expr

469

476

470−An evaluator for this language always returns an ``Integer``, and there

477+An evaluator for this language always returns an ``Integer``, and

471−are no situations in which it can fail!

478+there are no situations in which it can fail!

472

479

473.. code-block:: idris

480.. code-block:: idris

474

481

@@ -476,9 +483,9 @@ are no situations in which it can fail!

476 eval (Val x) = x

483 eval (Val x) = x

477 eval (Add l r) = eval l + eval r

484 eval (Add l r) = eval l + eval r

478

485

479−If we add variables, however, things get more interesting. The evaluator

486+If we add variables, however, things get more interesting. The

480−will need to be able to access the values stored in variables, and

487+evaluator will need to be able to access the values stored in

481−variables may be undefined.

488+variables, and variables may be undefined.

482

489

483.. code-block:: idris

490.. code-block:: idris

484

491

@@ -488,7 +495,7 @@ variables may be undefined.

488

495

489To start, we will change the type of ``eval`` so that it is effectful,

496To start, we will change the type of ``eval`` so that it is effectful,

490and supports an exception effect for throwing errors, and a state

497and supports an exception effect for throwing errors, and a state

491−containing a mapping from variable names (as ``String``\ s) to their

498+containing a mapping from variable names (as ``String``) to their

492values:

499values:

493

500

494.. code-block:: idris

501.. code-block:: idris

@@ -527,15 +534,15 @@ sets the state then invokes ``eval``:

527 eval' e = do put args

534 eval' e = do put args

528 eval e

535 eval e

529

536

530−We have picked ``Maybe`` as a computation context here; it needs to be a

537+We have picked ``Maybe`` as a computation context here; it needs to be

531−context which is available for every effect supported by ``eval``. In

538+a context which is available for every effect supported by

532−particular, because we have exceptions, it needs to be a context which

539+``eval``. In particular, because we have exceptions, it needs to be a

533−supports exceptions. Alternatively, ``Either String`` or ``IO`` would be

540+context which supports exceptions. Alternatively, ``Either String`` or

534−fine, for example.

541+``IO`` would be fine, for example.

535

542

536What if we want to extend the evaluator further, with random number

543What if we want to extend the evaluator further, with random number

537−generation? To achieve this, we add a new constructor to ``Expr``, which

544+generation? To achieve this, we add a new constructor to ``Expr``,

538−gives a random number up to a maximum value:

545+which gives a random number up to a maximum value:

539

546

540.. code-block:: idris

547.. code-block:: idris

541

548

@@ -544,8 +551,8 @@ gives a random number up to a maximum value:

544 | Add Expr Expr

551 | Add Expr Expr

545 | Random Integer

552 | Random Integer

546

553

547−Then, we need to deal with the new case, making sure that we extend the

554+Then, we need to deal with the new case, making sure that we extend

548−list of events to include ``RND``. It doen’t matter where ``RND``

555+the list of events to include ``RND``. It doen’t matter where ``RND``

549appears in the list, as long as it is present:

556appears in the list, as long as it is present:

550

557

551.. code-block:: idris

558.. code-block:: idris

@@ -563,10 +570,10 @@ has been generated:

563 putStrLn (show val)

570 putStrLn (show val)

564 return val

571 return val

565

572

566−If we try this without extending the effects list, we would see an error

573+If we try this without extending the effects list, we would see an

567−something like the following:

574+error something like the following:

568

575

569−.. code-block:: idris

576+::

570

577

571 Expr.idr:28:6:When elaborating right hand side of eval:

578 Expr.idr:28:6:When elaborating right hand side of eval:

572 Can't solve goal

579 Can't solve goal

@@ -580,12 +587,12 @@ this simply by updating the type of ``eval`` to include ``STDIO``.

580

587

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

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

582

589

583−Note that using ``STDIO`` will restrict the number of contexts in which

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

584−``eval`` can be ``run`` to those which support ``STDIO``, such as

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

585−``IO``. Once effect lists get longer, it can be a good idea instead to

592+as ``IO``. Once effect lists get longer, it can be a good idea instead

586−encapsulate sets of effects in a type synonym. This is achieved as

593+to encapsulate sets of effects in a type synonym. This is achieved as

587follows, simply by defining a function which computes a type, since

594follows, simply by defining a function which computes a type, since

588−types are first class in :

595+types are first class in ``Idris``:

589

596

590.. code-block:: idris

597.. code-block:: idris

591

598

docs/effects/state.rst+109−109

@@ -5,14 +5,14 @@ State

5=====

7Many programs, even pure programs, can benefit from locally mutable

8−state. For example, consider a program which tags binary tree nodes with

8+state. For example, consider a program which tags binary tree nodes

9−a counter, by an inorder traversal (i.e. counting depth first, left to

9+with a counter, by an inorder traversal (i.e. counting depth first,

10−right). This would perform something like the following:

10+left to right). This would perform something like the following:

12|image|

14−We can describe binary trees with the following data type ``BTree`` and

14+We can describe binary trees with the following data type ``BTree``

15−``testTree`` to represent the example input above:

15+and ``testTree`` to represent the example input above:

17.. code-block:: idris

@@ -26,8 +26,8 @@ We can describe binary trees with the following data type ``BTree`` and

26 "Sheila"

27 (Node Leaf "Bob" Leaf))

29−Then our function to implement tagging, beginning to tag with a specific

29+Then our function to implement tagging, beginning to tag with a

30−value ``i``, has the following type:

30+specific value ``i``, has the following type:

32.. code-block:: idris

@@ -36,9 +36,9 @@ value ``i``, has the following type:

36First attempt

37-------------

39−Naïvely, we can implement ``treeTag`` by implementing a helper function

39+Naïvely, we can implement ``treeTag`` by implementing a helper

40−which propagates a counter, returning the result of the count for each

40+function which propagates a counter, returning the result of the count

41−subtree:

41+for each subtree:

43.. code-block:: idris

@@ -70,8 +70,9 @@ ensure that state is propagated correctly to the recursive calls (i.e.

70passing the appropriate ``i`` or ``i’``). It is hard to read, because

71the functional details are obscured by the state propagation. Perhaps

72most importantly, there is a common programming pattern here which

73−should be abstracted but instead has been implemented by hand. There is

73+should be abstracted but instead has been implemented by hand. There

74−local mutable state (the counter) which we have had to make explicit.

74+is local mutable state (the counter) which we have had to make

75+explicit.

76Introducing ``Effects``

77Introducing ``Effects``

77-----------------------

78-----------------------

@@ -85,27 +86,27 @@ effectful program ``f`` has a type of the following form:

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

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

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

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

88−(``effs``, of type ``List EFFECT``) and the type the computation returns

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

89−``t``. So, our ``treeTagAux`` helper could be written with the following

90+returns ``t``. So, our ``treeTagAux`` helper could be written with the

90−type:

91+following type:

92.. code-block:: idris

93.. code-block:: idris

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

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

96−That is, ``treeTagAux`` has access to an integer state, because the list

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

97−of available effects includes ``STATE Int``. ``STATE`` is declared as

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

98−follows in the module ``Effect.State`` (that is, we must

99+declared as follows in the module ``Effect.State`` (that is, we must

99``import Effect.State`` to be able to use it):

100``import Effect.State`` to be able to use it):

100

101

101.. code-block:: idris

102.. code-block:: idris

102

103

103 STATE : Type -> EFFECT

104 STATE : Type -> EFFECT

104

105

105−It is an effect parameterised by a type (by convention, we write effects

106+It is an effect parameterised by a type (by convention, we write

106−in all capitals). The ``treeTagAux`` function is an effectful program

107+effects in all capitals). The ``treeTagAux`` function is an effectful

107−which builds a new tree tagged with ``Ints``, and is implemented as

108+program which builds a new tree tagged with ``Ints``, and is

108−follows:

109+implemented as follows:

109

110

110.. code-block:: idris

111.. code-block:: idris

111

112

@@ -118,25 +119,25 @@ follows:

118 pure (Node l' (i, x) r')

119 pure (Node l' (i, x) r')

119

120

120There are several remarks to be made about this implementation.

121There are several remarks to be made about this implementation.

121−Essentially, it hides the state, which can be accessed using ``get`` and

122+Essentially, it hides the state, which can be accessed using ``get``

122−updated using ``put``, but it introduces several new features.

123+and updated using ``put``, but it introduces several new features.

123Specifically, it uses ``do``-notation, binding variables with ``<-``,

124Specifically, it uses ``do``-notation, binding variables with ``<-``,

124−and a ``pure`` function. There is much to be said about these features,

125+and a ``pure`` function. There is much to be said about these

125−but for our purposes, it suffices to know the following:

126+features, but for our purposes, it suffices to know the following:

126

127

127−- ``do`` blocks allow effectful operations to be sequenced.

128+- ``do`` blocks allow effectful operations to be sequenced.

128

129

129−- ``x <- e`` binds the result of an effectful operation ``e`` to a

130+- ``x <- e`` binds the result of an effectful operation ``e`` to a

130 variable ``x``. For example, in the above code, ``treeTagAux l`` is

131 variable ``x``. For example, in the above code, ``treeTagAux l`` is

131− an effectful operation returning a pair ``(Int, BTree a)``, so ``l’``

132+ an effectful operation returning a pair ``(Int, BTree a)``, so

132− has type ``(Int, BTree a)``.

133+ ``l’`` has type ``(Int, BTree a)``.

133

134

134−- ``pure e`` turns a pure value ``e`` into the result of an effectful

135+- ``pure e`` turns a pure value ``e`` into the result of an effectful

135 operation.

136 operation.

136

137

137−The ``get`` and ``put`` functions read and write a state ``t``, assuming

138+The ``get`` and ``put`` functions read and write a state ``t``,

138−that the ``STATE t`` effect is available. They have the following types,

139+assuming that the ``STATE t`` effect is available. They have the

139−polymorphic in the state ``t`` they manage:

140+following types, polymorphic in the state ``t`` they manage:

140

141

141.. code-block:: idris

142.. code-block:: idris

142

143

@@ -144,15 +145,16 @@ polymorphic in the state ``t`` they manage:

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

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

145

146

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

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

147−that the calling function supports at least the effects required by the

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

148−called function. In this case, it is valid for ``treeTagAux`` to call

149+the called function. In this case, it is valid for ``treeTagAux`` to

149−both ``get`` and ``put`` because all three functions support the

150+call both ``get`` and ``put`` because all three functions support the

150``STATE Int`` effect.

151``STATE Int`` effect.

151

152

152Programs in ``Eff`` are run in some underlying *computation context*,

153Programs in ``Eff`` are run in some underlying *computation context*,

153−using the ``run`` or ``runPure`` function. Using ``runPure``, which runs

154+using the ``run`` or ``runPure`` function. Using ``runPure``, which

154−an effectful program in the identity context, we can write the

155+runs an effectful program in the identity context, we can write the

155−``treeTag`` function as follows, using ``put`` to initialise the state:

156+``treeTag`` function as follows, using ``put`` to initialise the

157+state:

156

158

157.. code-block:: idris

159.. code-block:: idris

158

160

@@ -216,11 +218,11 @@ shown in Listing [introprog].

216Effects and Resources

218Effects and Resources

217---------------------

219---------------------

218

220

219−Each effect is associated with a *resource*, which is initialised before

221+Each effect is associated with a *resource*, which is initialised

220−an effectful program can be run. For example, in the case of

222+before an effectful program can be run. For example, in the case of

221``STATE Int`` the corresponding resource is the integer state itself.

223``STATE Int`` the corresponding resource is the integer state itself.

222−The types of ``runPure`` and ``run`` show this (slightly simplified here

224+The types of ``runPure`` and ``run`` show this (slightly simplified

223−for illustrative purposes):

225+here for illustrative purposes):

224

226

225.. code-block:: idris

227.. code-block:: idris

226

228

@@ -238,10 +240,10 @@ class:

238

240

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

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

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

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

241−However, where no default value exists for a resource type (for example,

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

242−you may want a ``STATE`` type for which there is no ``Default``

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

243−instance) the resource environment can be given explicitly using one of

245+``Default`` instance) the resource environment can be given explicitly

244−the following functions:

246+using one of the following functions:

245

247

246.. code-block:: idris

248.. code-block:: idris

247

249

@@ -263,8 +265,8 @@ Labelled Effects

263What if we have more than one state, especially more than one state of

265What if we have more than one state, especially more than one state of

264the same type? How would ``get`` and ``put`` know which state they

266the same type? How would ``get`` and ``put`` know which state they

265should be referring to? For example, how could we extend the tree

267should be referring to? For example, how could we extend the tree

266−tagging example such that it additionally counts the number of leaves in

268+tagging example such that it additionally counts the number of leaves

267−the tree? One possibility would be to change the state so that it

269+in the tree? One possibility would be to change the state so that it

268captured both of these values, e.g.:

270captured both of these values, e.g.:

269

271

270.. code-block:: idris

272.. code-block:: idris

@@ -272,16 +274,16 @@ captured both of these values, e.g.:

272 treeTagAux : BTree a

274 treeTagAux : BTree a

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

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

274

276

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

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

276−not indicating which integer is which). It would be nice to be able to

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

277−call effectful programs which guaranteed only to access one of the

279+to call effectful programs which guaranteed only to access one of the

278−states, for example. In a larger application, this becomes particularly

280+states, for example. In a larger application, this becomes

279−important.

281+particularly important.

280

282

281−The library therefore allows effects in general to be *labelled* so that

283+The library therefore allows effects in general to be *labelled* so

282−they can be referred to explicitly by a particular name. This allows

284+that they can be referred to explicitly by a particular name. This

283−multiple effects of the same type to be included. We can count leaves

285+allows multiple effects of the same type to be included. We can count

284−and update the tag separately, by labelling them as follows:

286+leaves and update the tag separately, by labelling them as follows:

285

287

286.. code-block:: idris

288.. code-block:: idris

287

289

@@ -289,16 +291,16 @@ and update the tag separately, by labelling them as follows:

289 -> {['Tag ::: STATE Int,

291 -> {['Tag ::: STATE Int,

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

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

291

293

292−The ``:::`` operator allows an arbitrary label to be given to an effect.

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

293−This label can be any type—it is simply used to identify an effect

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

294−uniquely. Here, we have used a symbol type. In general ``’name``

296+effect uniquely. Here, we have used a symbol type. In general

295−introduces a new symbol, the only purpose of which is to disambiguate

297+``’name`` introduces a new symbol, the only purpose of which is to

296−values [2]_.

298+disambiguate values [2]_.

297

299

298When an effect is labelled, its operations are also labelled using the

300When an effect is labelled, its operations are also labelled using the

299−``:-`` operator. In this way, we can say explicitly which state we mean

301+``:-`` operator. In this way, we can say explicitly which state we

300−when using ``get`` and ``put``. The tree tagging program which also

302+mean when using ``get`` and ``put``. The tree tagging program which

301−counts leaves can be written as follows:

303+also counts leaves can be written as follows:

302

304

303.. code-block:: idris

305.. code-block:: idris

304

306

@@ -334,15 +336,15 @@ imperative language):

334

336

335To summarise, we have:

337To summarise, we have:

336

338

337−- ``:::`` to convert an effect to a labelled effect.

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

338

340

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

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

340 operation.

342 operation.

341

343

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

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

343

345

344−Or, more formally with their types (slightly simplified to account only

346+Or, more formally with their types (slightly simplified to account

345−for the situation where available effects are not updated):

347+only for the situation where available effects are not updated):

346

348

347.. code-block:: idris

349.. code-block:: idris

348

350

@@ -359,8 +361,8 @@ Hence, a label can be anything—a string, an integer, a type, etc.

359

361

360In many cases, using ``do``-notation can make programs unnecessarily

362In many cases, using ``do``-notation can make programs unnecessarily

361verbose, particularly in cases where the value bound is used once,

363verbose, particularly in cases where the value bound is used once,

362−immediately. The following program returns the length of the ``String``

364+immediately. The following program returns the length of the

363−stored in the state, for example:

365+``String`` stored in the state, for example:

364

366

365.. code-block:: idris

367.. code-block:: idris

366

368

@@ -378,8 +380,8 @@ this. The above program can be written instead as:

378 stateLength = pure (length !get)

380 stateLength = pure (length !get)

379

381

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

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

381−evaluated and then implicitly bound. Conceptually, we can think of ``!``

383+evaluated and then implicitly bound. Conceptually, we can think of

382−as being a prefix function with the following type:

384+``!`` as being a prefix function with the following type:

383

385

384.. code-block:: idris

386.. code-block:: idris

385

387

@@ -393,13 +395,13 @@ to right. In practice, ``!``-notation allows us to program in a more

393direct style, while still giving a notational clue as to which

395direct style, while still giving a notational clue as to which

394expressions are effectful.

396expressions are effectful.

395

397

396−For example, the expression…

398+For example, the expression:

397

399

398.. code-block:: idris

400.. code-block:: idris

399

401

400 let y = 42 in f !(g !(print y) !x)

402 let y = 42 in f !(g !(print y) !x)

401

403

402−…is lifted to:

404+is lifted to:

403

405

404.. code-block:: idris

406.. code-block:: idris

405

407

@@ -411,10 +413,10 @@ For example, the expression…

411Syntactic Sugar and ``Eff``

413Syntactic Sugar and ``Eff``

412---------------------------

414---------------------------

413

415

414−By now, you may be wondering about the syntax we are using for ``Eff``,

416+By now, you may be wondering about the syntax we are using for

415−because it doesn’t look like a normal type! (If not, you may safely skip

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

416−this section and return to it later.) In fact, the type of ``Eff`` is

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

417−the following:

419+``Eff`` is the following:

418

420

419.. code-block:: idris

421.. code-block:: idris

420

422

@@ -425,32 +427,32 @@ This is more general than the types we have been writing so far. It is

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

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

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

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

427

429

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

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

429−of *output* effects, computed from the result of an effectful operation.

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

430−That is: running an effectful program can change the set of effects

432+operation. That is: running an effectful program can change the set

431−available! This is a particularly powerful idea, and we will see its

433+of effects available! This is a particularly powerful idea, and we

432−consequences in more detail later. Some examples of operations which can

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

433−change the set of available effects are:

435+operations which can change the set of available effects are:

434

436

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

437+- Updating a state containing a dependent type (for example adding an

436 element to a vector).

438 element to a vector).

437

439

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

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

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

441+ *is* open afterwards depends on whether the file was successfully

440− opened.

442+ opened.

441

443

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

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

443− possible.

445+ possible.

444

446

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

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

446−Therefore, the library provides syntactic sugar which is translated such

448+Therefore, the library provides syntactic sugar which is translated

447−that…

449+such that:

448

450

449.. code-block:: idris

451.. code-block:: idris

450

452

451 { xs } Eff a

453 { xs } Eff a

452

454

453−…is expanded to …

455+is expanded to

454

456

455.. code-block:: idris

457.. code-block:: idris

456

458

@@ -458,8 +460,8 @@ that…

458

460

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

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

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

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

461−side-effecting programs. We could also have written ``treeTagAux`` with

463+side-effecting programs. We could also have written ``treeTagAux``

462−the expanded type:

464+with the expanded type:

463

465

464.. code-block:: idris

466.. code-block:: idris

465

467

@@ -472,14 +474,14 @@ Later, we will see programs which update effects:

472

474

473 { xs ==> xs' } Eff a

475 { xs ==> xs' } Eff a

474

476

475−…which is expanded to …

477+which is expanded to

476

478

477.. code-block:: idris

479.. code-block:: idris

478

480

479 Eff a xs (\_ => xs')

481 Eff a xs (\_ => xs')

480

482

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

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

482−a state machine). There is, for example, a version of ``put`` which

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

483updates the type of the state:

485updates the type of the state:

484

486

485.. code-block:: idris

487.. code-block:: idris

@@ -492,7 +494,7 @@ Also, we have:

492

494

493 { xs ==> {res} xs' } Eff a

495 { xs ==> {res} xs' } Eff a

494

496

495−…which is expanded to …

497+which is expanded to

496

498

497.. code-block:: idris

499.. code-block:: idris

498

500

@@ -501,13 +503,11 @@ Also, we have:

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

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

502operation ``res``.

504operation ``res``.

503

505

504−.. [1]

505− The earlier paper [3]_ describes the essential implementation details,

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

506− although the library presented there is an earlier version which is

507+ details, although the library presented there is an earlier version

507− less powerful than that presented in this tutorial.

508+ which is less powerful than that presented in this tutorial.

508

509

509−.. [2]

510− In practice, ``’name`` simply introduces a new empty type

510+.. [2] In practice, ``’name`` simply introduces a new empty type

511

512.. [3] Edwin Brady. 2013. Programming and reasoning with algebraic

513 effects and dependent types. SIGPLAN Not. 48, 9 (September

docs/guides/type-providers-ffi.rst+56−55

@@ -1,34 +1,33 @@

1Type Providers in Idris

2=======================

4−.. sectionauthor:: David Christiansen

5−

6−`Type providers in

4+`Type providers in Idris

7−Idris <http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

5+<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

8are simple enough, but there are a few caveats to using them that it

6are simple enough, but there are a few caveats to using them that it

9would be worthwhile to go through the basic steps. We also go over

7would be worthwhile to go through the basic steps. We also go over

10−foreign functions, because these will often be used with type providers.

8+foreign functions, because these will often be used with type

9+providers.

12The use case

11The use case

13------------

12------------

15−First, let's talk about *why* we might want type providers. There are a

14+First, let's talk about *why* we might want type providers. There are

16−number of reasons to use them and there are other examples available

15+a number of reasons to use them and there are other examples available

17around the net, but in this tutorial we'll be using them to port C's

16around the net, but in this tutorial we'll be using them to port C's

18``struct stat`` to Idris.

17``struct stat`` to Idris.

20−Why do we need type providers? Well, Idris's FFI needs to know the types

19+Why do we need type providers? Well, Idris's FFI needs to know the

21−of the things it passes to and from C, but the fields of a

20+types of the things it passes to and from C, but the fields of a

22−``struct stat`` are implementation-dependent types that cannot be relied

21+``struct stat`` are implementation-dependent types that cannot be

23−upon. We don't just want to hard-code these types into our program... so

22+relied upon. We don't just want to hard-code these types into our

24−we'll use a type provider to find them at compile time!

23+program... so we'll use a type provider to find them at compile time!

26A simple example

25A simple example

27----------------

26----------------

29First, let's go over a basic usage of type providers, because foreign

28First, let's go over a basic usage of type providers, because foreign

30−functions can be confusing but it's important to remember that providers

29+functions can be confusing but it's important to remember that

31−themselves are simple.

30+providers themselves are simple.

33A type provider is simply an IO action that returns a value of this

32A type provider is simply an IO action that returns a value of this

34type:

33type:

@@ -58,11 +57,11 @@ actions. Let's write a simple one now:

58 -- the readInt function is left as an exercise

57 -- the readInt function is left as an exercise

60We assume that whoever's compiling the library knows the size of

59We assume that whoever's compiling the library knows the size of

61−size\_t, so we'll just ask them! (Don't worry, we'll get it ourselves

60+``size_t``, so we'll just ask them! (Don't worry, we'll get it

62−later.) Then, if their response can be converted to an integer, we

61+ourselves later.) Then, if their response can be converted to an

63−present ``Provide sizeTSize`` as the result of our IO action; or if it

62+integer, we present ``Provide sizeTSize`` as the result of our IO

64−can't, we signal a failure. (This will then become a compile-time

63+action; or if it can't, we signal a failure. (This will then become a

65−error.)

64+compile-time error.)

67Now we can use this IO action as a type provider:

66Now we can use this IO action as a type provider:

@@ -88,8 +87,8 @@ Now we can use this IO action as a type provider:

88 putStr " bytes!"

87 putStr " bytes!"

90Yay! We... asked the user something at compile time? That's not very

89Yay! We... asked the user something at compile time? That's not very

91−good, actually. Our library is going to be difficult to compile! This is

90+good, actually. Our library is going to be difficult to compile! This

92−hardly a step up from having them edit in the size of ``size_t``

91+is hardly a step up from having them edit in the size of ``size_t``

93themselves!

92themselves!

95Don't worry, there's a better way.

94Don't worry, there's a better way.

@@ -98,18 +97,18 @@ Foreign Functions

98-----------------

97-----------------

100It's actually pretty easy to write a C function that figures out the

99It's actually pretty easy to write a C function that figures out the

101−size of size\_t:

100+size of ``size_t``:

102

101

103.. code:: c

102.. code:: c

104

103

105 int sizeof_size_t() { return sizeof(size_t); }

104 int sizeof_size_t() { return sizeof(size_t); }

106

105

107−(Why an int and not a size\_t? The FFI needs to know how to receive the

106+(Why an int and not a ``size_t``? The FFI needs to know how to receive

108−return value of this function and translate it into an Idris value. If

107+the return value of this function and translate it into an Idris

109−we knew how to do this for values of C type size\_t, we wouldn't need to

108+value. If we knew how to do this for values of C type ``size_t``, we

110−write this function at all! If we really wanted to be safe from

109+wouldn't need to write this function at all! If we really wanted to be

111−overflow, we could use an array of multiple integers, but the SIZE of

110+safe from overflow, we could use an array of multiple integers, but

112−size\_t is never going to be a 65535 byte integer.)

111+the SIZE of ``size_t`` is never going to be a 65535 byte integer.)

113

112

114So now we can get the size of ``size_t`` as long as we're in C code.

113So now we can get the size of ``size_t`` as long as we're in C code.

115We'd like to be able to use this from Idris. Can we do this? It turns

114We'd like to be able to use this from Idris. Can we do this? It turns

@@ -128,24 +127,24 @@ like this:

128

127

129Pretty simple. ``mkForeign`` takes a specification of what function it

128Pretty simple. ``mkForeign`` takes a specification of what function it

130needs to call, and we construct this specification with ``FFun``. And

129needs to call, and we construct this specification with ``FFun``. And

131−``FFun`` just takes a name, a list of argument types (we have none), and

130+``FFun`` just takes a name, a list of argument types (we have none),

132−a return type.

131+and a return type.

133

132

134One thing you might want to note: the return type we've specified is

133One thing you might want to note: the return type we've specified is

135``FInt``, not ``Int``. That's because ``Int`` is an idris type and C

134``FInt``, not ``Int``. That's because ``Int`` is an idris type and C

136functions don't return idris types. ``FInt`` is not an idris type, but

135functions don't return idris types. ``FInt`` is not an idris type, but

137−is just the representation of the type of a C int. It tells the compiler

136+is just the representation of the type of a C int. It tells the

138−"Treat the return value of this C function like it's a C int, and when

137+compiler "Treat the return value of this C function like it's a C int,

139−you pass it back into Idris, convert it to an Idris int."

138+and when you pass it back into Idris, convert it to an Idris int."

140

139

141Caveats of mkForeign

140Caveats of mkForeign

142^^^^^^^^^^^^^^^^^^^^

141^^^^^^^^^^^^^^^^^^^^

143

142

144First and foremost: ``mkForeign`` is not actually a function. It is

143First and foremost: ``mkForeign`` is not actually a function. It is

145−treated specially by the compiler, and there are certain rules you need

144+treated specially by the compiler, and there are certain rules you

146−to follow when using it.

145+need to follow when using it.

147

146

148−- Rule 1: the name string must be a literal or constant

147+- Rule 1: the name string must be a literal or constant

149

148

150This does not work:

149This does not work:

151

150

@@ -155,14 +154,15 @@ This does not work:

155 intIntToInt name = mkForeign (FFun name [FInt, FInt] FInt)

154 intIntToInt name = mkForeign (FFun name [FInt, FInt] FInt)

156

155

157You'll just have to bite the bullet and write out the whole

156You'll just have to bite the bullet and write out the whole

158−``mkForeign`` and ``FFun`` expression each time. \* Rule 2: the "call"

157+``mkForeign`` and ``FFun`` expression each time.

158+

159−to ``mkForeign`` must be fully applied

159+- Rule 2: the "call" to ``mkForeign`` must be fully applied

160

161This just means that every argument appearing in the list of argument

162types must be applied wherever you write ``mkForeign``. The arguments

163−don't have to be literals or even known at compile time; they just have

163+don't have to be literals or even known at compile time; they just

164−to be there. For example, if we have ``strlen : String -> IO Int``, then

164+have to be there. For example, if we have ``strlen : String -> IO

165−this is fine:

165+Int``, then this is fine:

166

167.. code-block:: idris

168

@@ -181,7 +181,8 @@ applied. This is okay:

181

182.. code-block:: idris

183

184+ lengths : IO [Int]

184− lengths : IO [Int] lengths = mapM strlen listOfStrings

185+ lengths = mapM strlen listOfStrings

185

186

186Running foreign functions

187Running foreign functions

187~~~~~~~~~~~~~~~~~~~~~~~~~

188~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -194,8 +195,8 @@ our code.

194In the interpreter

195In the interpreter

195^^^^^^^^^^^^^^^^^^

196^^^^^^^^^^^^^^^^^^

196

197

197−If we want to call our foreign functions from interpreted code (such as

198+If we want to call our foreign functions from interpreted code (such

198−the REPL or a type provider), we need to dynamically link a library

199+as the REPL or a type provider), we need to dynamically link a library

199containing the symbols we need. This is pretty easy to do with the

200containing the symbols we need. This is pretty easy to do with the

200``%dynamic`` directive:

201``%dynamic`` directive:

201

202

@@ -204,10 +205,10 @@ containing the symbols we need. This is pretty easy to do with the

204 %dynamic "./filename.so"

205 %dynamic "./filename.so"

205

206

206Note that the leading "./" is important: currently, the string you

207Note that the leading "./" is important: currently, the string you

207−provide is interpreted as by dlopen(), which on Unix does not search in

208+provide is interpreted as by ``dlopen()``, which on Unix does not search

208−the current directory by default. If you use the "./", the library will

209+in the current directory by default. If you use the "./", the library

209−be searched for in the directory from which you run idris (*not* the

210+will be searched for in the directory from which you run idris (*not*

210−location of the file you're running!). Of course, if you're using

211+the location of the file you're running!). Of course, if you're using

211functions from an installed library rather than something you wrote

212functions from an installed library rather than something you wrote

212yourself, the "./" is not necessary.

213yourself, the "./" is not necessary.

213

214

@@ -222,18 +223,18 @@ instead. We'll use the ``%include`` and ``%link`` directives:

222 %include C "filename.h"

223 %include C "filename.h"

223 %link C "filename.o"

224 %link C "filename.o"

224

225

225−Note the extra argument to the directive! We specify that we're linking

226+Note the extra argument to the directive! We specify that we're

226−a C header and library. Also, unlike ``%dynamic``, these directives

227+linking a C header and library. Also, unlike ``%dynamic``, these

227−search in the current directory by default. (That is, the directory from

228+directives search in the current directory by default. (That is, the

228−which we run idris.)

229+directory from which we run idris.)

229

230

230Putting it all together

231Putting it all together

231-----------------------

232-----------------------

232

233

233So, at the beginning of this article I said we'd use type providers to

234So, at the beginning of this article I said we'd use type providers to

234−port ``struct stat`` to Idris. The relevant part is just translating all

235+port ``struct stat`` to Idris. The relevant part is just translating

235−the mysterious typedef'd C types into Idris types, and that's what we'll

236+all the mysterious typedef'd C types into Idris types, and that's what

236−do here.

237+we'll do here.

237

238

238First, let's write a C file containing functions that we'll bind to.

239First, let's write a C file containing functions that we'll bind to.

239

240

docs/reference/documenting.rst+21−18

@@ -4,9 +4,9 @@

4Documenting Idris Code

5======================

7−Idris documentation comes in two major forms: comments, which exist for

7+Idris documentation comes in two major forms: comments, which exist

8−a reader’s edification and are ignored by the compiler, and inline API

8+for a reader’s edification and are ignored by the compiler, and inline

9−documentation, which the compiler parses and stores for future

9+API documentation, which the compiler parses and stores for future

10reference. To consult the documentation for a declaration ``f``, write

11``:doc f`` at the REPL or use the appropriate command in your editor

12(``C-c C-d`` in Emacs, in Vim).

@@ -14,12 +14,12 @@ reference. To consult the documentation for a declaration ``f``, write

14Comments

15--------

17−Use comments to explain why code is written the way that it is. Idris’s

17+Use comments to explain why code is written the way that it

18−comment syntax is the same as that of Haskell: lines beginning with

18+is. Idris’s comment syntax is the same as that of Haskell: lines

19−``--`` are comments, and regions bracketed by ``{-`` and ``-}`` are

19+beginning with ``--`` are comments, and regions bracketed by ``{-``

20−comments even if they extend across multiple lines. These can be used to

20+and ``-}`` are comments even if they extend across multiple

21−comment out lines of code or provide simple documentation for the

21+lines. These can be used to comment out lines of code or provide

22−readers of Idris code.

22+simple documentation for the readers of Idris code.

24Inline Documentation

25--------------------

@@ -36,15 +36,16 @@ constructors, or functions can be associated with these arguments using

36their names.

38The inline documentation for a declaration is an unbroken string of

39−lines, each of which begins with ``|||`` (three pipe symbols). The first

39+lines, each of which begins with ``|||`` (three pipe symbols). The

40−paragraph of the documentation is taken to be an overview, and in some

40+first paragraph of the documentation is taken to be an overview, and

41−contexts, only this overview will be shown. After the documentation for

41+in some contexts, only this overview will be shown. After the

42−the declaration as a whole, it is possible to associate documetation

42+documentation for the declaration as a whole, it is possible to

43−with specific named parameters, which can either be explicitly name or

43+associate documetation with specific named parameters, which can

44−the results of converting free variables to implicit parameters.

44+either be explicitly name or the results of converting free variables

45−Annotations are the same as with Javadoc annotations, that is for the

45+to implicit parameters. Annotations are the same as with Javadoc

46+annotations, that is for the named parameter ``(n : T)``, the

46−named parameter ``(n : T)``, the corresponding annotation is

47+corresponding annotation is ``||| @ n Some description`` that is

47−``||| @ n Some description`` that is placed before the declaration.

48+placed before the declaration.

49Documentation is written in Markdown, though not all contexts will

50Documentation is written in Markdown, though not all contexts will

50display all possible formatting (for example, images are not displayed

51display all possible formatting (for example, images are not displayed

@@ -53,6 +54,8 @@ italics correctly). A comprehensive set of examples is given below.

54.. code-block:: idris

55.. code-block:: idris

57+

58+ ||| Modules can also be documented.

56 module Docs

59 module Docs

58 ||| Add some numbers.

61 ||| Add some numbers.

docs/reference/erasure.rst+121−139

@@ -1,45 +1,17 @@

1Erasure By Usage Analysis

2=========================

4−.. sectionauthor:: Matus Tejiscak

5−

6−Outline

7−-------

8−

9−- `Motivation <#motivation>`__

10−- `Binary numbers <#binary-numbers>`__

11−- `U-views of lists <#u-views-of-lists>`__

12−- `Changes to Idris <#changes-to-idris>`__

13−- `Changes to the language <#changes-to-the-language>`__

14−- `What it means <#what-it-means>`__

15−- `How to use it <#how-to-use-it>`__

16−- `Benchmarks <#benchmarks>`__

17−- `Shortcomings <#shortcomings>`__

18−- `Planned features <#planned-features>`__

19−- `Troubleshooting <#troubleshooting>`__

20−- `My program is slower <#my-program-is-slower>`__

21−- `Usage warnings are unhelpful <#usage-warnings-are-unhelpful>`__

22−- `There should be no warnings in this

23− function <#there-should-be-no-warnings-in-this-function>`__

24−- `The compiler refuses to recognise this thing as

25− erased <#the-compiler-refuses-to-recognise-this-thing-as-erased>`__

26−- `How to read and resolve erasure

27− warnings <#how-to-read-and-resolve-erasure-warnings>`__

28−- `Example 1 <#example-1>`__

29−- `Example 2 <#example-2>`__

30−- `References <#references>`__

31−

32−This work stems from this `feature

4+This work stems from this `feature proposal

33−proposal <https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__

5+<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__

34−(obsoleted by this page). Beware that the information in the proposal is

6+(obsoleted by this page). Beware that the information in the proposal

35−out of date — and sometimes even in direct contradiction with the

7+is out of date — and sometimes even in direct contradiction with the

36eventual implementation.

8eventual implementation.

38Motivation

10Motivation

39----------

11----------

41−Traditional dependently typed languages (Agda, Coq) are good at erasing

13+Traditional dependently typed languages (Agda, Coq) are good at

42−*proofs* (either via irrelevance or an extra universe).

14+erasing *proofs* (either via irrelevance or an extra universe).

44.. code-block:: idris

16.. code-block:: idris

@@ -47,16 +19,16 @@ Traditional dependently typed languages (Agda, Coq) are good at erasing

47 half Z EZ = Z

19 half Z EZ = Z

48 half (S (S n)) (ES pf) = S (half n pf)

20 half (S (S n)) (ES pf) = S (half n pf)

50−For example, in the above snippet, the second argument is a proof, which

22+For example, in the above snippet, the second argument is a proof,

51−is used only to convince the compiler that the function is total. This

23+which is used only to convince the compiler that the function is

52−proof is never inspected at runtime and thus can be erased. In this

24+total. This proof is never inspected at runtime and thus can be

53−case, the mere existence of the proof is sufficient and we can use

25+erased. In this case, the mere existence of the proof is sufficient

54−irrelevance-related methods to achieve erasure.

26+and we can use irrelevance-related methods to achieve erasure.

56However, sometimes we want to erase *indices* and this is where the

28However, sometimes we want to erase *indices* and this is where the

57traditional approaches stop being useful, mainly for reasons described

29traditional approaches stop being useful, mainly for reasons described

58−in the `original

30+in the `original proposal

59−proposal <https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.

31+<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.

61.. code-block:: idris

33.. code-block:: idris

@@ -66,11 +38,11 @@ proposal <https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annot

66 | (xs, ys) = (x :: xs, y :: ys)

38 | (xs, ys) = (x :: xs, y :: ys)

68Notice that in this case, the second argument is the important one and

40Notice that in this case, the second argument is the important one and

69−we would like to get rid of the ``n`` instead, although the shape of the

41+we would like to get rid of the ``n`` instead, although the shape of

70−program is generally the same as in the previous case.

42+the program is generally the same as in the previous case.

72−There are methods described by Brady, McBride and McKinna in [BMM04] to

44+There are methods described by Brady, McBride and McKinna in [BMM04]_

73−remove the indices from data structures, exploiting the fact that

45+to remove the indices from data structures, exploiting the fact that

74functions operating on them either already have a copy of the

46functions operating on them either already have a copy of the

75appropriate index or the index can be quickly reconstructed if needed.

47appropriate index or the index can be quickly reconstructed if needed.

76However, we often want to erase the indices altogether, from the whole

48However, we often want to erase the indices altogether, from the whole

@@ -82,7 +54,7 @@ the runtime performance asymptotically.

82Binary numbers

54Binary numbers

83~~~~~~~~~~~~~~

55~~~~~~~~~~~~~~

85−- O(n) instead of O(log n)

57+- O(n) instead of O(log n)

87Consider the following ``Nat``-indexed type family representing binary

59Consider the following ``Nat``-indexed type family representing binary

88numbers:

60numbers:

@@ -99,10 +71,10 @@ memory-efficient because their size is logarithmic compared to the

99numbers they represent.

71numbers they represent.

100

101Unfortunately this is not the case. The problem is that these binary

73Unfortunately this is not the case. The problem is that these binary

102−numbers still carry the *unary* indices with them, performing arithmetic

74+numbers still carry the *unary* indices with them, performing

103−on the indices whenever arithmetic is done on the binary numbers

75+arithmetic on the indices whenever arithmetic is done on the binary

104−themselves. Hence the real representation of the number 15 looks like

76+numbers themselves. Hence the real representation of the number 15

105−this:

77+looks like this:

106

107::

79::

108

@@ -119,13 +91,16 @@ this:

119The used memory is actually *linear*, not logarithmic and therefore we

91The used memory is actually *linear*, not logarithmic and therefore we

120cannot get below O(n) with time complexities.

92cannot get below O(n) with time complexities.

121

122−One could argue that Idris in fact compiles ``Nat``\ s via GMP but

94+One could argue that Idris in fact compiles ``Nat`` via GMP but

123−that's a moot point for two reasons: \* First, whenever we try to index

95+that's a moot point for two reasons:

124−our datastructures with anything else than ``Nat``\ s, the compiler is

125−not going to come to the rescue. \* Second, even with ``Nat``\ s, the

126−GMP integers are *still* there and they slow the runtime down.

127

97+* First, whenever we try to index our datastructures with anything

98+else than ``Nat``, the compiler is not going to come to the rescue.

99+

100+* Second, even with ``Nat``, the GMP integers are *still* there and

101+they slow the runtime down.

102+

128−This ought not to be the case since the ``Nat``\ s are never used at

103+This ought not to be the case since the ``Nat`` are never used at

129runtime and they are only there for typechecking purposes. Hence we

104runtime and they are only there for typechecking purposes. Hence we

130should get rid of them and get runtime code similar to what a idris

105should get rid of them and get runtime code similar to what a idris

131programmer would write.

106programmer would write.

@@ -155,22 +130,22 @@ For better intuition, the shape of the U-view of

155 z (one)

130 z (one)

156

131

157When recursing over this structure, the values of ``xs`` range over

132When recursing over this structure, the values of ``xs`` range over

158−``[x0,x1,x2,z,y2,y1,y0]``, ``[x1,x2,z,y2,y1]``, ``[x2,z,y2]``, ``[z]``.

133+``[x0,x1,x2,z,y2,y1,y0]``, ``[x1,x2,z,y2,y1]``, ``[x2,z,y2]``,

159−No matter whether these lists are stored or built on demand, they take

134+``[z]``. No matter whether these lists are stored or built on demand,

160−up a quadratic amount of memory (because they cannot share nodes), and

135+they take up a quadratic amount of memory (because they cannot share

161−hence it takes a quadratic amount of time just to build values of this

136+nodes), and hence it takes a quadratic amount of time just to build

162−index alone.

137+values of this index alone.

163

138

164But the reasonable expectation is that operations with U-views take

139But the reasonable expectation is that operations with U-views take

165−linear time — so we need to erase the index ``xs`` if we want to achieve

140+linear time — so we need to erase the index ``xs`` if we want to

166−this goal.

141+achieve this goal.

167

142

168Changes to Idris

143Changes to Idris

169----------------

144----------------

170

145

171−Usage analysis is run at every compilation and its outputs are used for

146+Usage analysis is run at every compilation and its outputs are used

172−various purposes. This is actually invisible to the user but it's a

147+for various purposes. This is actually invisible to the user but it's

173−relatively big and important change, which enables the new features.

148+a relatively big and important change, which enables the new features.

174

149

175Everything that is found to be unused is erased. No annotations are

150Everything that is found to be unused is erased. No annotations are

176needed, just don't use the thing and it will vanish from the generated

151needed, just don't use the thing and it will vanish from the generated

@@ -178,25 +153,29 @@ code. However, if you wish, you can use the dot annotations to get a

178warning if the thing is accidentally used.

153warning if the thing is accidentally used.

179

154

180"Being used" in this context means that the value of the "thing" may

155"Being used" in this context means that the value of the "thing" may

181−influence run-time behaviour of the program. (More precisely, it is not

156+influence run-time behaviour of the program. (More precisely, it is

182−found to be irrelevant to the run-time behaviour by the usage analysis

157+not found to be irrelevant to the run-time behaviour by the usage

183−algorithm.)

158+analysis algorithm.)

159+

160+"Things" considered for removal by erasure include:

161+

162+* function arguments

184

163

185−"Things" considered for removal by erasure include: \* function

186−arguments \* data constructor fields (including record fields and

164+* data constructor fields (including record fields and dictionary

187−dictionary fields of class instances)

165+ fields of class instances)

188

166

189For example, ``Either`` often compiles to the same runtime

167For example, ``Either`` often compiles to the same runtime

190−representation as ``Bool``. Constructor field removal sometimes combines

168+representation as ``Bool``. Constructor field removal sometimes

191−with the newtype optimisation to have quite a strong effect.

169+combines with the newtype optimisation to have quite a strong effect.

192

170

193There is a new compiler option ``--warnreach``, which will enable

171There is a new compiler option ``--warnreach``, which will enable

194−warnings coming from erasure. Since we have full usage analysis, we can

172+warnings coming from erasure. Since we have full usage analysis, we

195−compile even those programs that violate erasure annotations -- it's

173+can compile even those programs that violate erasure annotations --

196−just that the binaries may run slower than expected. The warnings will

174+it's just that the binaries may run slower than expected. The warnings

197−be enabled by default in future versions of Idris (and possibly turned

175+will be enabled by default in future versions of Idris (and possibly

198−to errors). However, in this transitional period, we chose to keep them

176+turned to errors). However, in this transitional period, we chose to

199−on-demand to avoid confusion until better documentation is written.

177+keep them on-demand to avoid confusion until better documentation is

178+written.

200

179

201Case-tree elaboration tries to avoid using dotted "things" whenever

180Case-tree elaboration tries to avoid using dotted "things" whenever

202possible. (NB. This is not yet perfect and it's being worked on:

181possible. (NB. This is not yet perfect and it's being worked on:

@@ -218,8 +197,8 @@ runtime.

218 O : .{n : Nat} -> Bin n -> Bin (0 + 2*n)

197 O : .{n : Nat} -> Bin n -> Bin (0 + 2*n)

219 I : .{n : Nat} -> Bin n -> Bin (1 + 2*n)

198 I : .{n : Nat} -> Bin n -> Bin (1 + 2*n)

220

199

221−If these fields are found to be used at runtime, the dots will trigger a

200+If these fields are found to be used at runtime, the dots will trigger

222−warning (with ``--warnreach``).

201+a warning (with ``--warnreach``).

223

202

224Note that free (unbound) implicits are dotted by default so, for

203Note that free (unbound) implicits are dotted by default so, for

225example, the constructor ``O`` can be defined as:

204example, the constructor ``O`` can be defined as:

@@ -244,29 +223,31 @@ and free implicits are automatically dotted here, too.

244What it means

223What it means

245-------------

224-------------

246

225

247−Dot annotations serve two purposes: \* influence case-tree elaboration

226+Dot annotations serve two purposes:

227+

228+* influence case-tree elaboration to avoid dotted variables

229+

248−to avoid dotted variables \* trigger warnings when a dotted variable is

230+* trigger warnings when a dotted variable is used

249−used

250

231

251However, there's no direct connection between being dotted and being

232However, there's no direct connection between being dotted and being

252erased. The compiler erases everything it can, dotted or not. The dots

233erased. The compiler erases everything it can, dotted or not. The dots

253−are there mainly to help the programmer (and the compiler) refrain from

234+are there mainly to help the programmer (and the compiler) refrain

254−using the values they want to erase.

235+from using the values they want to erase.

255

236

256How to use it

237How to use it

257-------------

238-------------

258

239

259−Ideally, few or no extra annotations are needed -- in practice, it turns

240+Ideally, few or no extra annotations are needed -- in practice, it

260−out that having free implicits automatically dotted is enough to get

241+turns out that having free implicits automatically dotted is enough to

261−good erasure.

242+get good erasure.

262

243

263−Therefore, just compile with ``--warnreach`` to see warnings if erasure

244+Therefore, just compile with ``--warnreach`` to see warnings if

264−cannot remove parts of the program.

245+erasure cannot remove parts of the program.

265

246

266−However, those programs that have been written without runtime behaviour

247+However, those programs that have been written without runtime

267−in mind, will need some help to get in the form that compiles to a

248+behaviour in mind, will need some help to get in the form that

268−reasonable binary. Generally, it's sufficient to follow erasure warnings

249+compiles to a reasonable binary. Generally, it's sufficient to follow

269−(which may be sometimes unhelpful at the moment).

250+erasure warnings (which may be sometimes unhelpful at the moment).

270

251

271Benchmarks

252Benchmarks

272----------

253----------

@@ -289,49 +270,50 @@ their names.

289

270

290There is no decent documentation yet. This wiki page is the first one.

271There is no decent documentation yet. This wiki page is the first one.

291

272

292−There is no generally accepted terminology. We switch between "dotted",

273+There is no generally accepted terminology. We switch between

293−"unused", "erased", "irrelevant", "inaccessible", while each has a

274+"dotted", "unused", "erased", "irrelevant", "inaccessible", while each

294−slightly different meaning. We need more consistent and understandable

275+has a slightly different meaning. We need more consistent and

295−naming.

276+understandable naming.

296−

277+

297−If the same type is used in both erased and non-erased context, it will

278+If the same type is used in both erased and non-erased context, it

298−retain its fields to accomodate the least common denominator -- the

279+will retain its fields to accomodate the least common denominator --

299−non-erased context. This is particularly troublesome in the case of the

280+the non-erased context. This is particularly troublesome in the case

300−type of (dependent) pairs, where it actually means that no erasure would

281+of the type of (dependent) pairs, where it actually means that no

301−be performed. We should probably locate disjoint uses of data types and

282+erasure would be performed. We should probably locate disjoint uses of

302−split them into "sub-types". There are three different flavours of

283+data types and split them into "sub-types". There are three different

303−dependent types now: ``Sigma`` (nothing erased), ``Exists`` (first

284+flavours of dependent types now: ``Sigma`` (nothing erased),

304−component erased), ``Subset`` (second component erased).

285+``Exists`` (first component erased), ``Subset`` (second component

286+erased).

305

287

306Case-tree building does not avoid dotted values coming from

288Case-tree building does not avoid dotted values coming from

307pattern-matched constructors (https://gist.github.com/ziman/10458331).

289pattern-matched constructors (https://gist.github.com/ziman/10458331).

308This is to be fixed soon. (Fixed.)

290This is to be fixed soon. (Fixed.)

309

291

310Higher-order function arguments and opaque functional variables are

292Higher-order function arguments and opaque functional variables are

311−considered to be using all their arguments. To work around this, you can

293+considered to be using all their arguments. To work around this, you

312−force erasure via the type system, using the ``Erased`` wrapper:

294+can force erasure via the type system, using the ``Erased`` wrapper:

313https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr

295https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr

314

296

315Typeclass methods are considered to be using the union of all their

297Typeclass methods are considered to be using the union of all their

316−implementations. In other words, an argument of a method is unused only

298+implementations. In other words, an argument of a method is unused

317−if it is unused in every implementation of the method that occurs in the

299+only if it is unused in every implementation of the method that occurs

318−program.

300+in the program.

319

301

320Planned features

302Planned features

321----------------

303----------------

322

304

323−- Fixes to the above shortcomings in general.

305+- Fixes to the above shortcomings in general.

324

306

325−- Improvements to the case-tree elaborator so that it properly avoids

307+- Improvements to the case-tree elaborator so that it properly avoids

326 dotted fields of data constructors. Done.

308 dotted fields of data constructors. Done.

327

309

328−- Compiler pragma ``%default_usage used/unused`` and per-function

310+- Compiler pragma ``%default_usage used/unused`` and per-function

329− overrides ``used`` and ``unused``, which allow the programmer to mark

311+ overrides ``used`` and ``unused``, which allow the programmer to

330− the return value of a function as used, even if the function is not

312+ mark the return value of a function as used, even if the function

331− used in ``main`` (which is the case when writing library code). These

313+ is not used in ``main`` (which is the case when writing library

332− annotations will help library writers discover usage violations in

314+ code). These annotations will help library writers discover usage

333− their code before it is actually published and used in compiled

315+ violations in their code before it is actually published and used

334− programs.

316+ in compiled programs.

335

317

336Troubleshooting

318Troubleshooting

337---------------

319---------------

@@ -366,15 +348,15 @@ There should be no warnings in this function

366A possible cause is non-totality of the function (more precisely,

348A possible cause is non-totality of the function (more precisely,

367non-coverage). If a function is non-covering, the program needs to

349non-coverage). If a function is non-covering, the program needs to

368inspect all arguments in order to detect coverage failures at runtime.

350inspect all arguments in order to detect coverage failures at runtime.

369−Since the function inspects all its arguments, nothing can be erased and

351+Since the function inspects all its arguments, nothing can be erased

370−this may transitively cause usage violations. The solution is to make

352+and this may transitively cause usage violations. The solution is to

371−the function total or accept the fact that it will use its arguments and

353+make the function total or accept the fact that it will use its

372−remove some dots from the appropriate constructor fields and function

354+arguments and remove some dots from the appropriate constructor fields

373−arguments. (Please note that this is not a shortcoming of erasure and

355+and function arguments. (Please note that this is not a shortcoming of

374−there is nothing we can do about it.)

356+erasure and there is nothing we can do about it.)

375−

357+

376−Another possible cause is the currently imperfect case-tree elaboration,

358+Another possible cause is the currently imperfect case-tree

377−which does not avoid dotted constructor fields (see

359+elaboration, which does not avoid dotted constructor fields (see

378https://gist.github.com/ziman/10458331). You can either rephrase the

360https://gist.github.com/ziman/10458331). You can either rephrase the

379function or wait until this is fixed, hopefully soon. Fixed.

361function or wait until this is fixed, hopefully soon. Fixed.

380

362

@@ -496,15 +478,15 @@ We can see that the argument ``n`` of both ``I`` and ``O`` is used in

496the function ``toN``, argument 1.

478the function ``toN``, argument 1.

497

479

498At this stage of development, warnings only contain argument numbers,

480At this stage of development, warnings only contain argument numbers,

499−not names; this will hopefully be fixed. When numbering arguments, we go

481+not names; this will hopefully be fixed. When numbering arguments, we

500−from 0, taking free implicits first, left-to-right; then the bound

482+go from 0, taking free implicits first, left-to-right; then the bound

501arguments. The function ``toN`` has therefore in fact two arguments:

483arguments. The function ``toN`` has therefore in fact two arguments:

502``n`` (argument 0) and ``b`` (argument 1). And indeed, as the warning

484``n`` (argument 0) and ``b`` (argument 1). And indeed, as the warning

503says, we project the dotted field from ``b``.

485says, we project the dotted field from ``b``.

504

486

505Again, one solution is to fix the function ``toN`` to calculate its

487Again, one solution is to fix the function ``toN`` to calculate its

506−result honestly; the other one is to accept that we carry a ``Nat`` with

488+result honestly; the other one is to accept that we carry a ``Nat``

507−every constructor of ``Bin`` and make it a bound implicit:

489+with every constructor of ``Bin`` and make it a bound implicit:

508

490

509.. code-block:: idris

491.. code-block:: idris

510

492

@@ -514,6 +496,6 @@ every constructor of ``Bin`` and make it a bound implicit:

514References

496References

515----------

497----------

516

498

517−[BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive families

499+.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

518−need not store their

500+ families need not store their indices

519−indices <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__

501+ <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__

docs/reference/ffi.rst+59−51

@@ -3,35 +3,36 @@ New Foreign Function Interface

4.. sectionauthor:: Edwin Brady

6−Ever since Idris has had multiple backends compiling to different target

6+Ever since Idris has had multiple backends compiling to different

7−languages on potentially different platforms, we have had the problem

7+target languages on potentially different platforms, we have had the

8−that the foreign function interface (FFI) was written under the

8+problem that the foreign function interface (FFI) was written under

9−assumption of compiling to C. As a result, it has been hard to write

9+the assumption of compiling to C. As a result, it has been hard to

10−generic code for multiple targets, or even to be sure that if code

10+write generic code for multiple targets, or even to be sure that if

11−compiles that it will run on the expected target.

11+code compiles that it will run on the expected target.

13As of 0.9.17, Idris will have a new foreign function interface (FFI)

14which is aware of multiple targets. Users who are working with the

15default code generator can happily continue writing programs as before

16with no changes, but if you are writing bindings for an external

17−library, writing a back end, or working with a non-C back end, there are

17+library, writing a back end, or working with a non-C back end, there

18−some things you will need to be aware of, which this page describes.

18+are some things you will need to be aware of, which this page

19+describes.

20The ``IO'`` monad, and ``main``

21The ``IO'`` monad, and ``main``

21-------------------------------

22-------------------------------

23−The ``IO`` monad exists as before, but is now specific to the C backend

24+The ``IO`` monad exists as before, but is now specific to the C

24−(or, more precisely, any backend whose foreign function calls are

25+backend (or, more precisely, any backend whose foreign function calls

25−compatible with C.) Additionally, there is now an ``IO'`` monad, which

26+are compatible with C.) Additionally, there is now an ``IO'`` monad,

26−is parameterised over a FFI descriptor:

27+which is parameterised over a FFI descriptor:

28.. code-block:: idris

29.. code-block:: idris

30 data IO' : (lang : FFI) -> Type -> Type

31 data IO' : (lang : FFI) -> Type -> Type

32The Prelude defines two FFI descriptors which are imported

33The Prelude defines two FFI descriptors which are imported

33−automatically, for C and JavaScript/Node, and defines ``IO`` to use the

34+automatically, for C and JavaScript/Node, and defines ``IO`` to use

34−C FFI and ``JS_IO`` to use the JavaScript FFI:

35+the C FFI and ``JS_IO`` to use the JavaScript FFI:

36.. code-block:: idris

37.. code-block:: idris

@@ -44,26 +45,27 @@ C FFI and ``JS_IO`` to use the JavaScript FFI:

44 JS_IO : Type -> Type

45 JS_IO : Type -> Type

45 JS_IO a = IO' FFI_JS a

46 JS_IO a = IO' FFI_JS a

47−As before, the entry point to an Idris program is ``main``, but the type

48+As before, the entry point to an Idris program is ``main``, but the

48−of ``main`` can now be any instance of ``IO'``, e.g. the following are

49+type of ``main`` can now be any instance of ``IO'``, e.g. the

49−both valid:

50+following are both valid:

51.. code-block:: idris

52.. code-block:: idris

53 main : IO ()

54 main : IO ()

54 main : JS_IO ()

55 main : JS_IO ()

56−The FFI descriptor includes details about which types can be marshalled

57+The FFI descriptor includes details about which types can be

57−between the foreign language and Idris, and the "target" of a foreign

58+marshalled between the foreign language and Idris, and the "target" of

58−function call (typically just a String representation of the function's

59+a foreign function call (typically just a String representation of the

59−name, but potentially something more complicated such as an external

60+function's name, but potentially something more complicated such as an

60−library file or even a URL).

61+external library file or even a URL).

62FFI descriptors

63FFI descriptors

63---------------

64---------------

65−An FFI descriptor is a record containing a predicate which holds when a

66+An FFI descriptor is a record containing a predicate which holds when

66−type can be marshalled, and the type of the target of a foreign call:

67+a type can be marshalled, and the type of the target of a foreign

68+call:

68.. code-block:: idris

70.. code-block:: idris

@@ -112,12 +114,12 @@ type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function

112type, which gives the expected types of the remaining arguments. Here,

114type, which gives the expected types of the remaining arguments. Here,

113we're calling an external function ``fileOpen`` which takes, in the C, a

115we're calling an external function ``fileOpen`` which takes, in the C, a

114``char*`` file name, a ``char*`` mode, and returns a file pointer. It is

116``char*`` file name, a ``char*`` mode, and returns a file pointer. It is

115−the job of the C back end to convert Idris ``String``\ s to C ``char*``

117+the job of the C back end to convert Idris ``String`` to C ``char*``

116and vice versa.

118and vice versa.

117

119

118The argument types and return type given here must be present in the

120The argument types and return type given here must be present in the

119−``fn_types`` predicate of the ``FFI_C`` description for the foreign call

121+``fn_types`` predicate of the ``FFI_C`` description for the foreign

120−to be valid.

122+call to be valid.

121

123

122**Note** The arguments to ``foreign`` *must* be known at compile time,

124**Note** The arguments to ``foreign`` *must* be known at compile time,

123because the foreign calls are generated statically. The ``%inline``

125because the foreign calls are generated statically. The ``%inline``

@@ -136,14 +138,18 @@ FFI implementation

136

138

137In order to write bindings to external libraries, the details of how

139In order to write bindings to external libraries, the details of how

138``foreign`` works are unnecessary --- you simply need to know that

140``foreign`` works are unnecessary --- you simply need to know that

139−``foreign`` takes an FFI descriptor, the function name, and its type. It

141+``foreign`` takes an FFI descriptor, the function name, and its

140−is instructive to look a little deeper, however:

142+type. It is instructive to look a little deeper, however:

141

143

142The type of ``foreign`` is as follows:

144The type of ``foreign`` is as follows:

143

145

144.. code-block:: idris

146.. code-block:: idris

145

147

148+ foreign : (ffi : FFI)

149+ -> (fname : ffi_fn f)

150+ -> (ty : Type)

146− foreign : (ffi : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy ffi [] ty} -> ty

151+ -> {auto fty : FTy ffi [] ty}

152+ -> ty

147

153

148The important argument here is the implicit ``fty``, which contains a

154The important argument here is the implicit ``fty``, which contains a

149proof (``FTy``) that the given type is valid according to the FFI

155proof (``FTy``) that the given type is valid according to the FFI

@@ -155,10 +161,11 @@ description ``ffi``:

155 FRet : ffi_types f t -> FTy f xs (IO' f t)

161 FRet : ffi_types f t -> FTy f xs (IO' f t)

156 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)

162 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)

157

163

158−Notice that this uses the ``ffi_types`` field of the FFI descriptor ---

164+Notice that this uses the ``ffi_types`` field of the FFI descriptor

159−these arguments to ``FRet`` and ``FFun`` give explicit proofs that the

165+--- these arguments to ``FRet`` and ``FFun`` give explicit proofs that

160−type is valid in this FFI. For example, the above ``do_fopen`` builds

166+the type is valid in this FFI. For example, the above ``do_fopen``

161−the following implicit proof as the ``fty`` argument to ``foreign``:

167+builds the following implicit proof as the ``fty`` argument to

168+``foreign``:

162

169

163.. code-block:: idris

170.. code-block:: idris

164

171

@@ -169,13 +176,13 @@ Compiling foreign calls

169

176

170(This section assumes some knowledge of the Idris internals.)

177(This section assumes some knowledge of the Idris internals.)

171

178

172−When writing a back end, we now need to know how to compile ``foreign``.

179+When writing a back end, we now need to know how to compile

173−We'll skip the details here of how a ``foreign`` call reaches the

180+``foreign``. We'll skip the details here of how a ``foreign`` call

174−intermediate representation (the IR), though you can look in ``IO.idr``

181+reaches the intermediate representation (the IR), though you can look

175−in the ``prelude`` package to see a bit more detail --- a ``foreign``

182+in ``IO.idr`` in the ``prelude`` package to see a bit more detail ---

176−call is implemented by the primitive function ``mkForeignPrim``. The

183+a ``foreign`` call is implemented by the primitive function

177−important part of the IR as defined in ``Lang.hs`` is the following

184+``mkForeignPrim``. The important part of the IR as defined in

178−constructor:

185+``Lang.hs`` is the following constructor:

179

186

180.. code-block:: idris

187.. code-block:: idris

181

188

@@ -186,9 +193,9 @@ constructor:

186

193

187So, a ``foreign`` call appears in the IR as the ``LForeign``

194So, a ``foreign`` call appears in the IR as the ``LForeign``

188constructor, which takes a function descriptor (of a type given by the

195constructor, which takes a function descriptor (of a type given by the

189−``ffi_fn`` field in the FFI descriptor), a return type descriptor (given

196+``ffi_fn`` field in the FFI descriptor), a return type descriptor

190−by an application of ``FTy``), and a list of arguments with type

197+(given by an application of ``FTy``), and a list of arguments with

191−descriptors (also given by an application of ``FTy``).

198+type descriptors (also given by an application of ``FTy``).

192

199

193An ``FDesc`` describes an application of a name to some arguments, and

200An ``FDesc`` describes an application of a name to some arguments, and

194is really just a simplified subset of an ``LExp``:

201is really just a simplified subset of an ``LExp``:

@@ -210,9 +217,9 @@ Our ``do_fopen`` example above arrives in the ``LExp`` form as:

210 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))

217 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))

211 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]

218 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]

212

219

213−(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations of

220+(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations

214−the arguments.) This information should be enough for any back end to

221+of the arguments.) This information should be enough for any back end

215−marshal the arguments and return value appropriately.

222+to marshal the arguments and return value appropriately.

216

223

217.. note::

224.. note::

218

225

@@ -228,7 +235,8 @@ JavaScript FFI descriptor

228~~~~~~~~~~~~~~~~~~~~~~~~~

235~~~~~~~~~~~~~~~~~~~~~~~~~

229

236

230The JavaScript FFI descriptor is a little more complex, because the

237The JavaScript FFI descriptor is a little more complex, because the

231−JavaScript FFI supports marshalling functions. It is defined as follows:

238+JavaScript FFI supports marshalling functions. It is defined as

239+follows:

232

240

233.. code-block:: idris

241.. code-block:: idris

234

242

@@ -255,9 +263,9 @@ JavaScript FFI supports marshalling functions. It is defined as follows:

255The reason for wrapping function types in a ``JsFn`` is to help the

263The reason for wrapping function types in a ``JsFn`` is to help the

256proof search when building ``FTy``. We hope to improve proof search

264proof search when building ``FTy``. We hope to improve proof search

257eventually, but for the moment it works much more reliably if the

265eventually, but for the moment it works much more reliably if the

258−indices are disjoint! An example of using this appears in

266+indices are disjoint! An example of using this appears in `IdrisScript

259−`IdrisScript <https://github.com/idris-hackers/IdrisScript>`__ when

267+<https://github.com/idris-hackers/IdrisScript>`__ when setting

260−setting timeouts:

268+timeouts:

261

269

262.. code-block:: idris

270.. code-block:: idris

263

271

docs/reference/uniqueness-types.rst+49−51

@@ -1,8 +1,6 @@

1Uniqueness Types

2================

4−.. sectionauthor:: Edwin Brady

5−

6Uniqueness Types are an experimental feature available from Idris

4Uniqueness Types are an experimental feature available from Idris

70.9.15. A value with a unique type is guaranteed to have *at most one*

50.9.15. A value with a unique type is guaranteed to have *at most one*

8reference to it at run-time, which means that it can safely be updated

6reference to it at run-time, which means that it can safely be updated

@@ -12,11 +10,11 @@ reactive systems, programs which run in limited memory environments,

12device drivers, and any other system with hard real-time requirements,

10device drivers, and any other system with hard real-time requirements,

13ideally while giving up as little high level conveniences as possible.

11ideally while giving up as little high level conveniences as possible.

15−They are inspired by linear types, `Uniqueness

13+They are inspired by linear types, `Uniqueness Types

16−Types <https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the

14+<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean

17−`Clean <http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

15+<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

18−ownership types and borrowed pointers in the

16+ownership types and borrowed pointers in the `Rust

19−`Rust <http://www.rust-lang.org/>`__ programming language.

17+<http://www.rust-lang.org/>`__ programming language.

21Some things we hope to be able to do eventually with uniqueness types

19Some things we hope to be able to do eventually with uniqueness types

22include:

20include:

@@ -39,11 +37,11 @@ declare the type of unique lists as follows:

39 Nil : UList a

37 Nil : UList a

40 (::) : a -> UList a -> UList a

38 (::) : a -> UList a -> UList a

42−If we have a value ``xs : UList a``, then there is at most one reference

40+If we have a value ``xs : UList a``, then there is at most one

43−to ``xs`` at run-time. The type checker preserves this guarantee by

41+reference to ``xs`` at run-time. The type checker preserves this

44−ensuring that there is at most one reference to any value of a unique

42+guarantee by ensuring that there is at most one reference to any value

45−type in a pattern clause. For example, the following function definition

43+of a unique type in a pattern clause. For example, the following

46−would be valid:

44+function definition would be valid:

48.. code-block:: idris

46.. code-block:: idris

@@ -55,8 +53,8 @@ In the second clause, ``xs`` is a value of a unique type, and only

55appears once on the right hand side, so this clause is valid. Not only

53appears once on the right hand side, so this clause is valid. Not only

56that, since we know there can be no other reference to the ``UList a``

54that, since we know there can be no other reference to the ``UList a``

57argument, we can reuse its space for building the result! The compiler

55argument, we can reuse its space for building the result! The compiler

58−is aware of this, and compiles this definition to an in-place update of

56+is aware of this, and compiles this definition to an in-place update

59−the list.

57+of the list.

61The following function definition would not be valid (even assuming an

59The following function definition would not be valid (even assuming an

62implementation of ``++``), however, since ``xs`` appears twice:

60implementation of ``++``), however, since ``xs`` appears twice:

@@ -84,14 +82,14 @@ If we explicitly copy, however, the typechecker is happy:

84Note that it's fine to use ``x`` twice, because ``a`` is a ``Type``,

82Note that it's fine to use ``x`` twice, because ``a`` is a ``Type``,

85rather than a ``UniqueType``.

83rather than a ``UniqueType``.

87−There are some other restrictions on where a ``UniqueType`` can appear,

85+There are some other restrictions on where a ``UniqueType`` can

88−so that the uniqueness property is preserved. In particular, the type of

86+appear, so that the uniqueness property is preserved. In particular,

89−the function type, ``(x : a) -> b`` depends on the type of ``a`` or

87+the type of the function type, ``(x : a) -> b`` depends on the type of

90−``b`` - if either is a ``UniqueType``, then the function type is also a

88+``a`` or ``b`` - if either is a ``UniqueType``, then the function type

91−``UniqueType``. Then, in a data declaration, if the type constructor

89+is also a ``UniqueType``. Then, in a data declaration, if the type

92−builds a ``Type``, then no constructor can have a ``UniqueType``. For

90+constructor builds a ``Type``, then no constructor can have a

93−example, the following definition is invalid, since it would embed a

91+``UniqueType``. For example, the following definition is invalid,

94−unique value in a possible non-unique value:

92+since it would embed a unique value in a possible non-unique value:

96.. code-block:: idris

94.. code-block:: idris

@@ -127,15 +125,15 @@ composition as follows:

127

125

128The ``Type*`` type stands for either unique or non-unique types. Since

126The ``Type*`` type stands for either unique or non-unique types. Since

129such a function may be passed a ``UniqueType``, any value of type

127such a function may be passed a ``UniqueType``, any value of type

130−``Type*`` must also satisfy the requirement that it appears at most once

128+``Type*`` must also satisfy the requirement that it appears at most

131−on the right hand side.

129+once on the right hand side.

132

130

133Borrowed Types

131Borrowed Types

134~~~~~~~~~~~~~~

132~~~~~~~~~~~~~~

135

133

136It quickly becomes obvious when working with uniqueness types that

134It quickly becomes obvious when working with uniqueness types that

137−having only one reference at a time can be painful. For example, what if

135+having only one reference at a time can be painful. For example, what

138−we want to display a list before updating it?

136+if we want to display a list before updating it?

139

137

140.. code-block:: idris

138.. code-block:: idris

141

139

@@ -158,8 +156,8 @@ the list! So the following function would be invalid:

158

156

159Still, one would hope to be able to display a unique list without

157Still, one would hope to be able to display a unique list without

160problem, since it merely *inspects* the list; there are no updates. We

158problem, since it merely *inspects* the list; there are no updates. We

161−can achieve this, using the notion of *borrowing*. A Borrowed type is a

159+can achieve this, using the notion of *borrowing*. A Borrowed type is

162−Unique type which can be inspected at the top level (by pattern

160+a Unique type which can be inspected at the top level (by pattern

163matching, or by *lending* to another function) but no further. This

161matching, or by *lending* to another function) but no further. This

164ensures that the internals (i.e. the arguments to top level patterns)

162ensures that the internals (i.e. the arguments to top level patterns)

165will not be passed to any function which will update them.

163will not be passed to any function which will update them.

@@ -191,21 +189,21 @@ this, we can write ``showU`` as follows:

191 showU' [x] = show x

189 showU' [x] = show x

192 showU' (Read (x :: xs)) = show x ++ ", " ++ showU' (lend xs)

190 showU' (Read (x :: xs)) = show x ++ ", " ++ showU' (lend xs)

193

191

194−Unlike a unique value, a borrowed value may be referred to as many times

192+Unlike a unique value, a borrowed value may be referred to as many

195−as desired. However, there is a restriction on how a borrowed value can

193+times as desired. However, there is a restriction on how a borrowed

196−be used. After all, much like a library book or your neighbour's

194+value can be used. After all, much like a library book or your

197−lawnmower, if a function borrows a value it is expected to return it in

195+neighbour's lawnmower, if a function borrows a value it is expected to

198−exactly the condition in which it was received!

196+return it in exactly the condition in which it was received!

199

197

200−The restriction is that when a ``Borrowed`` type is matched, any pattern

198+The restriction is that when a ``Borrowed`` type is matched, any

201−variables under the ``Read`` which have a unique type may not be

199+pattern variables under the ``Read`` which have a unique type may not

202−referred to at all on the right hand side (unless they are themselves

200+be referred to at all on the right hand side (unless they are

203−``lent`` to another function).

201+themselves ``lent`` to another function).

204

202

205Uniqueness information is stored in the type, and in particular in

203Uniqueness information is stored in the type, and in particular in

206function types. Once we're in a unique context, any new function which

204function types. Once we're in a unique context, any new function which

207−is constructed will be required to have unique type, which prevents the

205+is constructed will be required to have unique type, which prevents

208−following sort of bad program being implemented:

206+the following sort of bad program being implemented:

209

207

210.. code-block:: idris

208.. code-block:: idris

211

209

@@ -234,20 +232,20 @@ Problems/Disadvantages/Still to do...

234This is a work in progress, there is lots to do. The most obvious

232This is a work in progress, there is lots to do. The most obvious

235problem is the loss of abstraction. On the one hand, we have more

233problem is the loss of abstraction. On the one hand, we have more

236precise control over memory usage with ``UniqueType`` and

234precise control over memory usage with ``UniqueType`` and

237−``BorrowedType``, but they are not in general compatible with functions

235+``BorrowedType``, but they are not in general compatible with

238−polymorphic over ``Type``. In the short term, we can start to write

236+functions polymorphic over ``Type``. In the short term, we can start

239−reactive and low memory systems with this, but longer term it would be

237+to write reactive and low memory systems with this, but longer term it

240−nice to support more abstraction.

238+would be nice to support more abstraction.

241

239

242We also haven't checked any of the metatheory, so this could all be

240We also haven't checked any of the metatheory, so this could all be

243fatally flawed! The implementation is based to a large extent on

241fatally flawed! The implementation is based to a large extent on

244−`Uniqueness Typing

242+`Uniqueness Typing Simplified

245−Simplified <http://lambda-the-ultimate.org/node/2708>`__, by de Vries et

243+<http://lambda-the-ultimate.org/node/2708>`__, by de Vries et al, so

246−al, so there is reason to believe things should be fine, but we still

244+there is reason to believe things should be fine, but we still have to

247−have to do the work.

245+do the work.

248

246

249Much as there are with linear types, there are some annoyances when

247Much as there are with linear types, there are some annoyances when

250−trying to prove properties of functions with unique types (for example,

248+trying to prove properties of functions with unique types (for

251−what counts as a use of a value). Since we require *at most* one use of

249+example, what counts as a use of a value). Since we require *at most*

252−a value, rather than *exactly* one, this seems to be less of an issue in

250+one use of a value, rather than *exactly* one, this seems to be less

253−practice, but still needs thought.

251+of an issue in practice, but still needs thought.

docs/tutorial/classes.rst+63−62

@@ -13,9 +13,9 @@ to display different types in a uniform way.

13To achieve this, we use a feature which has proved to be effective in

14Haskell, namely *type classes*. To define a type class, we provide a

15collection of overloaded operations which describe the interface for

16−*instances* of that class. A simple example is the ``Show`` type class,

16+*instances* of that class. A simple example is the ``Show`` type

17−which is defined in the prelude and provides an interface for converting

17+class, which is defined in the prelude and provides an interface for

18−values to ``String``:

18+converting values to ``String``:

20.. code-block:: idris

@@ -29,9 +29,9 @@ This generates a function of the following type (which we call a

30 show : Show a => a -> String

32−We can read this as: “under the constraint that ``a`` is an instance of

32+We can read this as: “under the constraint that ``a`` is an instance

33−``Show``, take an input ``a`` and return a ``String``.” An instance of a

33+of ``Show``, take an input ``a`` and return a ``String``.” An instance

34−class is defined with an ``instance`` declaration, which provides

34+of a class is defined with an ``instance`` declaration, which provides

35implementations of the function for a specific type. For example, the

36``Show`` instance for ``Nat`` could be defined as:

@@ -41,7 +41,7 @@ implementations of the function for a specific type. For example, the

41 show Z = "Z"

42 show (S k) = "s" ++ show k

44−.. code-block:: idris

44+::

46 Idris> show (S (S (S Z)))

47 "sssZ" : String

@@ -77,8 +77,8 @@ the built-in types:

77 (==) : a -> a -> Bool

78 (/=) : a -> a -> Bool

80−To declare an instance of a type, we have to give definitions of all of

80+To declare an instance of a type, we have to give definitions of all

81−the methods. For example, for an instance of ``Eq`` for ``Nat``:

81+of the methods. For example, for an instance of ``Eq`` for ``Nat``:

83.. code-block:: idris

@@ -92,8 +92,8 @@ the methods. For example, for an instance of ``Eq`` for ``Nat``:

93It is hard to imagine many cases where the ``/=`` method will be

94anything other than the negation of the result of applying the ``==``

95−method. It is therefore convenient to give a default definition for each

95+method. It is therefore convenient to give a default definition for

96−method in the class declaration, in terms of the other method:

96+each method in the class declaration, in terms of the other method:

98.. code-block:: idris

@@ -113,9 +113,9 @@ Extending Classes

113-----------------

114

115Classes can also be extended. A logical next step from an equality

116−relation ``Eq`` is to define an ordering relation ``Ord``. We can define

116+relation ``Eq`` is to define an ordering relation ``Ord``. We can

117−an ``Ord`` class which inherits methods from ``Eq`` as well as defining

117+define an ``Ord`` class which inherits methods from ``Eq`` as well as

118−some of its own:

118+defining some of its own:

119

120.. code-block:: idris

121

@@ -136,18 +136,18 @@ some of its own:

136The ``Ord`` class allows us to compare two values and determine their

137ordering. Only the ``compare`` method is required; every other method

138has a default definition. Using this we can write functions such as

139−``sort``, a function which sorts a list into increasing order, provided

139+``sort``, a function which sorts a list into increasing order,

140−that the element type of the list is in the ``Ord`` class. We give the

140+provided that the element type of the list is in the ``Ord`` class. We

141−constraints on the type variables left of the fat arrow ``=>``, and the

141+give the constraints on the type variables left of the fat arrow

142−function type to the right of the fat arrow:

142+``=>``, and the function type to the right of the fat arrow:

143

144.. code-block:: idris

145

146 sort : Ord a => List a -> List a

147

148−Functions, classes and instances can have multiple constraints. Multiple

148+Functions, classes and instances can have multiple

149−constaints are written in brackets in a comma separated list, for

149+constraints. Multiple constaints are written in brackets in a comma

150−example:

150+separated list, for example:

151

152.. code-block:: idris

153

@@ -159,8 +159,8 @@ Functors and Applicatives

159

160So far, we have seen single parameter type classes, where the parameter

161is of type ``Type``. In general, there can be any number (greater than

162−0) of parameters, and the parameters can have *any* type. If the type of

162+0) of parameters, and the parameters can have *any* type. If the type

163−the parameter is not ``Type``, we need to give an explicit type

163+of the parameter is not ``Type``, we need to give an explicit type

164declaration. For example, the ``Functor`` class is defined in the

165library:

166

@@ -198,7 +198,7 @@ Monads and ``do``-notation

198--------------------------

199

200The ``Monad`` class allows us to encapsulate binding and computation,

201−and is the basis of ``do``-notation introduced in Section

201+and is the basis of ``do``-notation introduced in Section

202:ref:`sect-do`. It extends ``Applicative`` as defined above, and is

203defined as follows:

204

@@ -210,11 +210,11 @@ defined as follows:

210Inside a ``do`` block, the following syntactic transformations are

211applied:

212

213−- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``

213+- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``

214

215−- ``v; e`` becomes ``v >>= (\backslash_ => e)``

215+- ``v; e`` becomes ``v >>= (\backslash_ => e)``

216

217−- ``let x = v; e`` becomes ``let x = v in e``

217+- ``let x = v; e`` becomes ``let x = v in e``

218

219``IO`` is an instance of ``Monad``, defined using primitive functions.

220We can also define an instance for ``Maybe``, as follows:

@@ -226,7 +226,7 @@ We can also define an instance for ``Maybe``, as follows:

226 (Just x) >>= k = k x

227

228Using this we can, for example, define a function which adds two

229−``Maybe Int``\ s, using the monad to encapsulate the error handling:

229+``Maybe Int``, using the monad to encapsulate the error handling:

230

231.. code-block:: idris

232

@@ -235,8 +235,8 @@ Using this we can, for example, define a function which adds two

235 y' <- y -- Extract value from y

236 return (x' + y') -- Add them

237

238−This function will extract the values from ``x`` and ``y``, if they are

238+This function will extract the values from ``x`` and ``y``, if they

239−available, or return ``Nothing`` if they are not. Managing the

239+are available, or return ``Nothing`` if they are not. Managing the

240``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the

241``do`` notation.

242

@@ -252,8 +252,8 @@ available, or return ``Nothing`` if they are not. Managing the

252

253In many cases, using ``do``-notation can make programs unnecessarily

254verbose, particularly in cases such as ``m_add`` above where the value

255−bound is used once, immediately. In these cases, we can use a shorthand

255+bound is used once, immediately. In these cases, we can use a

256−version, as follows:

256+shorthand version, as follows:

257

258.. code-block:: idris

259

@@ -261,8 +261,8 @@ version, as follows:

261 m_add x y = return (!x + !y)

262

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

264−evaluated and then implicitly bound. Conceptually, we can think of ``!``

264+evaluated and then implicitly bound. Conceptually, we can think of

265−as being a prefix function with the following type:

265+``!`` as being a prefix function with the following type:

266

267.. code-block:: idris

268

@@ -276,13 +276,13 @@ to right. In practice, ``!``-notation allows us to program in a more

276direct style, while still giving a notational clue as to which

277expressions are monadic.

278

279−For example, the expression…

279+For example, the expression:

280

281.. code-block:: idris

282

283 let y = 42 in f !(g !(print y) !x)

284

285−…is lifted to:

285+is lifted to:

286

287.. code-block:: idris

288

@@ -294,9 +294,9 @@ For example, the expression…

294Monad comprehensions

295~~~~~~~~~~~~~~~~~~~~

296

297−The list comprehension notation we saw in Section :ref:`sect-more-expr` is more

297+The list comprehension notation we saw in Section

298−general, and applies to anything which is an instance of both ``Monad``

298+:ref:`sect-more-expr` is more general, and applies to anything which

299−and ``Alternative``:

299+is an instance of both ``Monad`` and ``Alternative``:

300

301.. code-block:: idris

302

@@ -304,18 +304,18 @@ and ``Alternative``:

304 empty : f a

305 (<|>) : f a -> f a -> f a

306

307−In general, a comprehension takes the form

307+In general, a comprehension takes the form ``[ exp | qual1, qual2, …,

308−``[ exp | qual1, qual2, …, qualn ]`` where ``quali`` can be one of:

308+qualn ]`` where ``quali`` can be one of:

309

310−- A generator ``x <- e``

310+- A generator ``x <- e``

311

312−- A *guard*, which is an expression of type ``Bool``

312+- A *guard*, which is an expression of type ``Bool``

313

314−- A let binding ``let x = e``

314+- A let binding ``let x = e``

315

316To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first

317−any qualifier ``qual`` which is a *guard* is translated to

317+any qualifier ``qual`` which is a *guard* is translated to ``guard

318−``guard qual``, using the following function:

318+qual``, using the following function:

319

320.. code-block:: idris

321

@@ -338,13 +338,13 @@ would be:

338Idiom brackets

339--------------

340

341−While ``do`` notation gives an alternative meaning to sequencing, idioms

341+While ``do`` notation gives an alternative meaning to sequencing,

342−give an alternative meaning to *application*. The notation and larger

342+idioms give an alternative meaning to *application*. The notation and

343−example in this section is inspired by Conor McBride and Ross Paterson’s

343+larger example in this section is inspired by Conor McBride and Ross

344−paper “Applicative Programming with Effects” [1]_.

344+Paterson’s paper “Applicative Programming with Effects” [1]_.

345

346First, let us revisit ``m_add`` above. All it is really doing is

347−applying an operator to two values extracted from ``Maybe Int``\ ’s. We

347+applying an operator to two values extracted from ``Maybe Int``. We

348could abstract out the application:

349

350.. code-block:: idris

@@ -365,8 +365,8 @@ alternative notion of function application, with explicit calls to

365Rather than having to insert ``m_app`` everywhere there is an

366application, we can use to do the job for us. To do this, we can make

367``Maybe`` an instance of ``Applicative`` as follows, where ``<>`` is

368−defined in the same way as ``m_app`` above (this is defined in the ``Idris``

368+defined in the same way as ``m_app`` above (this is defined in the

369−library):

369+``Idris`` library):

370

371.. code-block:: idris

372

@@ -376,8 +376,9 @@ library):

376 (Just f) <*> (Just a) = Just (f a)

377 _ <*> _ = Nothing

378

379−Using we can use this instance as follows, where a function application

379+Using we can use this instance as follows, where a function

380−``[| f a1 …an |]`` is translated into ``pure f <> a1 <> …<> an``:

380+application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>

381+…<> an``:

381

382

382.. code-block:: idris

383.. code-block:: idris

383

384

@@ -387,9 +388,9 @@ Using we can use this instance as follows, where a function application

387An error-handling interpreter

388An error-handling interpreter

388~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

389~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

389

390

390−Idiom notation is commonly useful when defining evaluators. McBride and

391+Idiom notation is commonly useful when defining evaluators. McBride

391−Paterson describe such an evaluator [1]_, for a language similar to the

392+and Paterson describe such an evaluator [1]_, for a language similar

392−following:

393+to the following:

393

394

394.. code-block:: idris

395.. code-block:: idris

395

396

@@ -423,8 +424,8 @@ retrieve values from the context during evaluation:

423When defining an evaluator for the language, we will be applying

424When defining an evaluator for the language, we will be applying

424functions in the context of an ``Eval``, so it is natural to make

425functions in the context of an ``Eval``, so it is natural to make

425``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an

426``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an

426−instance of ``Applicative`` it is necessary to make ``Eval`` an instance

427+instance of ``Applicative`` it is necessary to make ``Eval`` an

427−of ``Functor``:

428+instance of ``Functor``:

428

429

429.. code-block:: idris

430.. code-block:: idris

430

431

@@ -471,7 +472,7 @@ To achieve this, instances can be *named* as follows:

471This declares an instance as normal, but with an explicit name,

472This declares an instance as normal, but with an explicit name,

472``myord``. The syntax ``compare @{myord}`` gives an explicit instance to

473``myord``. The syntax ``compare @{myord}`` gives an explicit instance to

473``compare``, otherwise it would use the default instance for ``Nat``. We

474``compare``, otherwise it would use the default instance for ``Nat``. We

474−can use this, for example, to sort a list of ``Nat`` s in reverse.

475+can use this, for example, to sort a list of ``Nat`` in reverse.

475Given the following list:

476Given the following list:

476

477

477.. code-block:: idris

478.. code-block:: idris

@@ -479,7 +480,7 @@ Given the following list:

479 testList : List Nat

480 testList : List Nat

480 testList = [3,4,1]

481 testList = [3,4,1]

481

482

482−…e can sort it using the default ``Ord`` instance, then the named

483+We can sort it using the default ``Ord`` instance, then the named

483instance ``myord`` as follows, at the ``Idris`` prompt:

484instance ``myord`` as follows, at the ``Idris`` prompt:

484

485

485::

486::

docs/tutorial/conclusions.rst+5−5

@@ -11,24 +11,24 @@ dependent types in general, can be obtained from various sources:

11 questions on the mailing list.

13- The IRC channel ``#idris``, on

14− `chat.freenode.net <chat.freenode.net>`__.

14+ `chat.freenode.net <http://chat.freenode.net>`__.

16−- The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further

16+- The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further

17 user provided information, in particular:

19 - https://github.com/idris-lang/Idris-dev/wiki/Manual

21 - https://github.com/idris-lang/Idris-dev/wiki/Language-Features

23−- Examining the prelude and exploring the ``samples`` in the

23+- Examining the prelude and exploring the ``samples`` in the

24 distribution. The ``Idris`` source can be found online at:

25 https://github.com/idris-lang/Idris-dev.

27- Existing projects on the ``Idris Hackers`` web space:

28 http://idris-hackers.github.io.

30−- Various papers (e.g. [1]_, [2]_, and [3]_).

30+- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly

31− Although these mostly describe older versions of ``Idris``.

31+ describe older versions of ``Idris``.

33.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems

34 programming with embedded domain specific languages. In

docs/tutorial/interactive.rst+51−45

@@ -5,29 +5,31 @@ Interactive Editing

5===================

7By now, we have seen several examples of how ``Idris``’ dependent type

8−system can give extra confidence in a function’s correctness by giving a

8+system can give extra confidence in a function’s correctness by giving

9−more precise description of its intended behaviour in its *type*. We

9+a more precise description of its intended behaviour in its *type*. We

10have also seen an example of how the type system can help with EDSL

11development by allowing a programmer to describe the type system of an

12object language. However, precise types give us more than verification

13−of programs — we can also exploit types to help write programs which are

13+of programs — we can also exploit types to help write programs which

14−*correct by construction*.

14+are *correct by construction*.

16The ``Idris`` REPL provides several commands for inspecting and

17modifying parts of programs, based on their types, such as case

18−splitting on a pattern variable, inspecting the type of a metavariable,

18+splitting on a pattern variable, inspecting the type of a

19−and even a basic proof search mechanism. In this section, we explain how

19+metavariable, and even a basic proof search mechanism. In this

20−these features can be exploited by a text editor, and specifically how

20+section, we explain how these features can be exploited by a text

21+editor, and specifically how to do so in `Vim

21−to do so in `Vim <https://github.com/idris-hackers/idris-vim>`_. An interactive mode for `Emacs <https://github.com/idris-hackers/idris-emacs>`_ is also

22+<https://github.com/idris-hackers/idris-vim>`_. An interactive mode

23+for `Emacs <https://github.com/idris-hackers/idris-emacs>`_ is also

22available.

24available.

25Editing at the REPL

27Editing at the REPL

26-------------------

28-------------------

28−The REPL provides a number of commands, which we will describe shortly,

30+The REPL provides a number of commands, which we will describe

29−which generate new program fragments based on the currently loaded

31+shortly, which generate new program fragments based on the currently

30−module. These take the general form

32+loaded module. These take the general form

32::

34::

@@ -63,8 +65,8 @@ Editing Commands

63~~~~~~~~~~

65~~~~~~~~~~

65The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a

67The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a

66−template definition for the function named ``f`` declared on line ``n``.

68+template definition for the function named ``f`` declared on line

67−For example, if the code beginning on line 94 contains:

69+``n``. For example, if the code beginning on line 94 contains:

69.. code-block:: idris

71.. code-block:: idris

@@ -111,23 +113,23 @@ then ``:cs 96 xs`` will give:

111

113

112That is, the pattern variable ``xs`` has been split into the two

114That is, the pattern variable ``xs`` has been split into the two

113possible cases ``[]`` and ``x :: xs``. Again, the names are chosen

115possible cases ``[]`` and ``x :: xs``. Again, the names are chosen

114−according to the same heuristic. If we update the file (using ``:cs!``)

116+according to the same heuristic. If we update the file (using

115−then case split on ``ys`` on the same line, we get:

117+``:cs!``) then case split on ``ys`` on the same line, we get:

116

118

117.. code-block:: idris

119.. code-block:: idris

118

120

119 vzipWith f [] [] = ?vzipWith_rhs_3

121 vzipWith f [] [] = ?vzipWith_rhs_3

120

122

121That is, the pattern variable ``ys`` has been split into one case

123That is, the pattern variable ``ys`` has been split into one case

122−``[]``, ``Idris`` having noticed that the other possible case

124+``[]``, ``Idris`` having noticed that the other possible case ``y ::

123−``y :: ys`` would lead to a unification error.

125+ys`` would lead to a unification error.

124

126

125:addmissing

127:addmissing

126~~~~~~~~~~~

128~~~~~~~~~~~

127

129

128The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

130The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

129clauses which are required to make the function ``f`` on line ``n``

131clauses which are required to make the function ``f`` on line ``n``

130−cover all inputs. For example, if the code beginning on line 94 is…

132+cover all inputs. For example, if the code beginning on line 94 is

131

133

132.. code-block:: idris

134.. code-block:: idris

133

135

@@ -168,25 +170,27 @@ then ``:ps 96 vzipWith_rhs_1`` will give

168

170

169 []

171 []

170

172

171−This works because it is searching for a ``Vect`` of length 0, of which

173+This works because it is searching for a ``Vect`` of length 0, of

172−the empty vector is the only possibiliy. Similarly, and perhaps

174+which the empty vector is the only possibiliy. Similarly, and perhaps

173−surprisingly, there is only one possibility if we try to solve

175+surprisingly, there is only one possibility if we try to solve ``:ps

174−``:ps 97 vzipWith_rhs_2``:

176+97 vzipWith_rhs_2``:

175

177

176.. code-block:: idris

178.. code-block:: idris

177

179

178 f x y :: (vzipWith f xs ys)

180 f x y :: (vzipWith f xs ys)

179

181

180−This works because ``vzipWith`` has a precise enough type: The resulting

182+This works because ``vzipWith`` has a precise enough type: The

181−vector has to be non-empty (a ``::``); the first element must have type

183+resulting vector has to be non-empty (a ``::``); the first element

182−``c`` and the only way to get this is to apply ``f`` to ``x`` and ``y``;

184+must have type ``c`` and the only way to get this is to apply ``f`` to

183−finally, the tail of the vector can only be built recursively.

185+``x`` and ``y``; finally, the tail of the vector can only be built

186+recursively.

184

187

185:makewith

188:makewith

186~~~~~~~~~

189~~~~~~~~~

187

190

188−The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a ``with``

191+The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a

189−to a pattern clause. For example, recall ``parity``. If line 10 is:

192+``with`` to a pattern clause. For example, recall ``parity``. If line

193+10 is:

190

194

191.. code-block:: idris

195.. code-block:: idris

192

196

@@ -209,9 +213,10 @@ patterns:

209 parity (S (S (plus n n))) | odd = ?parity_rhs_2

213 parity (S (S (plus n n))) | odd = ?parity_rhs_2

210

214

211Note that case splitting has normalised the patterns here (giving

215Note that case splitting has normalised the patterns here (giving

212−``plus`` rather than ``+``). In any case, we see that using interactive

216+``plus`` rather than ``+``). In any case, we see that using

213−editing significantly simplifies the implementation of dependent pattern

217+interactive editing significantly simplifies the implementation of

214−matching by showing a programmer exactly what the valid patterns are.

218+dependent pattern matching by showing a programmer exactly what the

219+valid patterns are.

215

220

216Interactive Editing in Vim

221Interactive Editing in Vim

217--------------------------

222--------------------------

@@ -221,32 +226,33 @@ interactive editing support using the commands described above.

221Interactive editing is achieved using the following editor commands,

226Interactive editing is achieved using the following editor commands,

222each of which update the buffer directly:

227each of which update the buffer directly:

223

228

224−- ``\d`` adds a template definition for the name declared on the

229+- ``\d`` adds a template definition for the name declared on the

225 current line (using ``:addclause``).

230 current line (using ``:addclause``).

226

231

227−- ``\c`` case splits the variable at the cursor (using ``:casesplit``).

232+- ``\c`` case splits the variable at the cursor (using

233+ ``:casesplit``).

228

234

229−- ``\m`` adds the missing cases for the name at the cursor (using

235+- ``\m`` adds the missing cases for the name at the cursor (using

230 ``:addmissing``).

236 ``:addmissing``).

231

237

232−- ``\w`` adds a ``with`` clause (using ``:makewith``).

238+- ``\w`` adds a ``with`` clause (using ``:makewith``).

233

239

234−- ``\o`` invokes a proof search to solve the metavariable under the

240+- ``\o`` invokes a proof search to solve the metavariable under the

235 cursor (using ``:proofsearch``).

241 cursor (using ``:proofsearch``).

236

242

237−- ``\p`` invokes a proof search with additional hints to solve the

243+- ``\p`` invokes a proof search with additional hints to solve the

238 metavariable under the cursor (using ``:proofsearch``).

244 metavariable under the cursor (using ``:proofsearch``).

239

245

240There are also commands to invoke the type checker and evaluator:

246There are also commands to invoke the type checker and evaluator:

241

247

242−- ``\t`` displays the type of the (globally visible) name under the

248+- ``\t`` displays the type of the (globally visible) name under the

243− cursor. In the case of a metavariable, this displays the context and

249+ cursor. In the case of a metavariable, this displays the context

244− the expected type.

250+ and the expected type.

245

251

246−- ``\e`` prompts for an expression to evaluate.

252+- ``\e`` prompts for an expression to evaluate.

247

253

248−- ``\r`` reloads and type checks the buffer.

254+- ``\r`` reloads and type checks the buffer.

249

255

250−Corresponding commands are also available in the Emacs mode. Support for

256+Corresponding commands are also available in the Emacs mode. Support

251−other editors can be added in a relatively straighforward manner by

257+for other editors can be added in a relatively straighforward manner

252−using ``idris –client``.

258+by using ``idris –client``.

docs/tutorial/interp.rst+31−28

@@ -6,9 +6,10 @@ Example: The Well-Typed Interpreter

7In this section, we’ll use the features we’ve seen so far to write a

8larger example, an interpreter for a simple functional programming

9−language, with variables, function application, binary operators and an

9+language, with variables, function application, binary operators and

10−``if...then...else`` construct. We will use the dependent type system to

10+an ``if...then...else`` construct. We will use the dependent type

11−ensure that any programs which can be represented are well-typed.

11+system to ensure that any programs which can be represented are

12+well-typed.

13Representing Languages

14Representing Languages

14----------------------

15----------------------

@@ -74,8 +75,8 @@ look at each constructor in turn.

75We use a nameless representation for variables — they are *de Bruijn

76We use a nameless representation for variables — they are *de Bruijn

76indexed*. Variables are represented by a proof of their membership in

77indexed*. Variables are represented by a proof of their membership in

77−the context, ``HasType i G T``, which is a proof that variable ``i`` in

78+the context, ``HasType i G T``, which is a proof that variable ``i``

78−context ``G`` has type ``T``. This is defined as follows:

79+in context ``G`` has type ``T``. This is defined as follows:

80.. code-block:: idris

81.. code-block:: idris

@@ -87,17 +88,17 @@ We can treat *Stop* as a proof that the most recently defined variable

87is well-typed, and *Pop n* as a proof that, if the ``n``\ th most

88is well-typed, and *Pop n* as a proof that, if the ``n``\ th most

88recently defined variable is well-typed, so is the ``n+1``\ th. In

89recently defined variable is well-typed, so is the ``n+1``\ th. In

89practice, this means we use ``Stop`` to refer to the most recently

90practice, this means we use ``Stop`` to refer to the most recently

90−defined variable, ``Pop Stop`` to refer to the next, and so on, via the

91+defined variable, ``Pop Stop`` to refer to the next, and so on, via

91−``Var`` constructor:

92+the ``Var`` constructor:

93.. code-block:: idris

94.. code-block:: idris

95 Var : HasType i G t -> Expr G t

96 Var : HasType i G t -> Expr G t

97−So, in an expression ``\x,\y. x y``, the variable ``x`` would have a de

98+So, in an expression ``\x,\y. x y``, the variable ``x`` would have a

98−Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``, represented

99+de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,

99−as ``Stop``. We find these by counting the number of lambdas between the

100+represented as ``Stop``. We find these by counting the number of

100−definition and the use.

101+lambdas between the definition and the use.

101

102

102A value carries a concrete representation of an integer:

103A value carries a concrete representation of an integer:

103

104

@@ -105,9 +106,9 @@ A value carries a concrete representation of an integer:

105

106

106 Val : (x : Int) -> Expr G TyInt

107 Val : (x : Int) -> Expr G TyInt

107

108

108−A lambda creates a function. In the scope of a function of type

109+A lambda creates a function. In the scope of a function of type ``a ->

109−``a -> t``, there is a new local variable of type ``a``, which is

110+t``, there is a new local variable of type ``a``, which is expressed

110−expressed by the context index:

111+by the context index:

111

112

112.. code-block:: idris

113.. code-block:: idris

113

114

@@ -128,9 +129,9 @@ informs what the types of the arguments must be:

128 Op : (interpTy a -> interpTy b -> interpTy c) ->

129 Op : (interpTy a -> interpTy b -> interpTy c) ->

129 Expr G a -> Expr G b -> Expr G c

130 Expr G a -> Expr G b -> Expr G c

130

131

131−Finally, if expressions make a choice given a boolean. Each branch must

132+Finally, if expressions make a choice given a boolean. Each branch

132−have the same type, and we will evaluate the branches lazily so that

133+must have the same type, and we will evaluate the branches lazily so

133−only the branch which is taken need be evaluated:

134+that only the branch which is taken need be evaluated:

134

135

135.. code-block:: idris

136.. code-block:: idris

136

137

@@ -142,13 +143,14 @@ only the branch which is taken need be evaluated:

142Writing the Interpreter

143Writing the Interpreter

143-----------------------

144-----------------------

144

145

145−When we evaluate an ``Expr``, we’ll need to know the values in scope, as

146+When we evaluate an ``Expr``, we’ll need to know the values in scope,

146−well as their types. ``Env`` is an environment, indexed over the types

147+as well as their types. ``Env`` is an environment, indexed over the

147−in scope. Since an environment is just another form of list, albeit with

148+types in scope. Since an environment is just another form of list,

148−a strongly specified connection to the vector of local variable types,

149+albeit with a strongly specified connection to the vector of local

149−we use the usual ``::`` and ``Nil`` constructors so that we can use the

150+variable types, we use the usual ``::`` and ``Nil`` constructors so

150−usual list syntax. Given a proof that a variable is defined in the

151+that we can use the usual list syntax. Given a proof that a variable

151−context, we can then produce a value from the environment:

152+is defined in the context, we can then produce a value from the

153+environment:

152

154

153.. code-block:: idris

155.. code-block:: idris

154

156

@@ -258,10 +260,11 @@ function on user input:

258 x <- getLine

260 x <- getLine

259 print (interp [] fact (cast x))

261 print (interp [] fact (cast x))

260

262

261−Here, ``cast`` is an overloaded function which converts a value from one

263+Here, ``cast`` is an overloaded function which converts a value from

262−type to another if possible. Here, it converts a string to an integer,

264+one type to another if possible. Here, it converts a string to an

263−giving 0 if the input is invalid. An example run of this program at the

265+integer, giving 0 if the input is invalid. An example run of this

264−``Idris`` interactive environment is shown in Listing :ref:`factrun`.

266+program at the ``Idris`` interactive environment is shown in Listing

267+:ref:`factrun`.

265

268

266

269

267.. literalinclude:: ../listing/idris-prompt-interp.txt

270.. literalinclude:: ../listing/idris-prompt-interp.txt

docs/tutorial/introduction.rst+15−12

@@ -1,11 +1,14 @@

1+.. _sect-intro:

1===========

3===========

2Introducton

4Introducton

3===========

5===========

5In conventional programming languages, there is a clear distinction

7In conventional programming languages, there is a clear distinction

6−between *types* and *values*. For example, in `Haskell <http://www.haskell.org>`_, the following

8+between *types* and *values*. For example, in `Haskell

9+<http://www.haskell.org>`_, the following are types, representing

7−are types, representing integers, characters, lists of characters, and

10+integers, characters, lists of characters, and lists of any value

8−lists of any value respectively:

11+respectively:

10- ``Int``, ``Char``, ``[Char]``, ``[a]``

13- ``Int``, ``Char``, ``[Char]``, ``[a]``

@@ -22,11 +25,11 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element

22type and ``n`` is the length of the list and can be an arbitrary term.

25type and ``n`` is the length of the list and can be an arbitrary term.

24When types can contain values, and where those values describe

27When types can contain values, and where those values describe

25−properties (e.g. the length of a list) the type of a function can begin

28+properties (e.g. the length of a list) the type of a function can

26−to describe its own properties. For example, concatenating two lists has

29+begin to describe its own properties. For example, concatenating two

27−the property that the resulting list’s length is the sum of the lengths

30+lists has the property that the resulting list’s length is the sum of

28−of the two input lists. We can therefore give the following type to the

31+the lengths of the two input lists. We can therefore give the

29−``app`` function, which concatenates vectors:

32+following type to the ``app`` function, which concatenates vectors:

31.. code-block:: idris

34.. code-block:: idris

@@ -34,10 +37,10 @@ of the two input lists. We can therefore give the following type to the

35This tutorial introduces ``Idris``, a general purpose functional

38This tutorial introduces ``Idris``, a general purpose functional

36programming language with dependent types. The goal of the ``Idris``

39programming language with dependent types. The goal of the ``Idris``

37−project is to build a dependently typed language suitable for verifiable

40+project is to build a dependently typed language suitable for

38−*systems* programming. To this end, ``Idris`` is a compiled language

41+verifiable *systems* programming. To this end, ``Idris`` is a compiled

39−which aims to generate efficient executable code. It also has a

42+language which aims to generate efficient executable code. It also has

40−lightweight foreign function interface which allows easy interaction

43+a lightweight foreign function interface which allows easy interaction

41with external ``C`` libraries.

44with external ``C`` libraries.

43Intended Audience

46Intended Audience

docs/tutorial/starting.rst+25−24

@@ -7,13 +7,14 @@ Getting Started

7Prerequisites

8-------------

10−Before installing ``Idris``, you will need to make sure you have all of

10+Before installing ``Idris``, you will need to make sure you have all

11−the necessary libraries and tools. You will need:

11+of the necessary libraries and tools. You will need:

13−- A fairly recent Haskell platform. Version 2013.2.0.0 should be

13+- A fairly recent Haskell platform. Version 2013.2.0.0 should be

14− sufficiently recent, though it is better to be completely up to date.

14+ sufficiently recent, though it is better to be completely up to

15+ date.

16−- The *GNU Multiple Precision Arithmetic Library* (GMP) is available

17+- The *GNU Multiple Precision Arithmetic Library* (GMP) is available

17 from MacPorts/Homebrew and all major Linux distributions.

18 from MacPorts/Homebrew and all major Linux distributions.

19Downloading and Installing

20Downloading and Installing

@@ -26,10 +27,10 @@ prerequisites, is to type:

27 cabal update; cabal install idris

28 cabal update; cabal install idris

29−This will install the latest version released on Hackage, along with any

30+This will install the latest version released on Hackage, along with

30−dependencies. If, however, you would like the most up to date

31+any dependencies. If, however, you would like the most up to date

31development version you can find it, as well as build intructions, on

32development version you can find it, as well as build intructions, on

32−GitHub at: https://github.com/edwinb/Idris-dev.

33+GitHub at: https://github.com/idris-lang/Idris-dev.

34To check that installation has succeeded, and to write your first

35To check that installation has succeeded, and to write your first

35``Idris`` program, create a file called “``hello.idr``” containing the

36``Idris`` program, create a file called “``hello.idr``” containing the

@@ -37,9 +38,9 @@ following text:

38If you are familiar with Haskell, it should be fairly clear what the

39If you are familiar with Haskell, it should be fairly clear what the

39program is doing and how it works, but if not, we will explain the

40program is doing and how it works, but if not, we will explain the

40−details later. You can compile the program to an executable by entering

41+details later. You can compile the program to an executable by

41−``idris hello.idr -o hello`` at the shell prompt. This will create an

42+entering ``idris hello.idr -o hello`` at the shell prompt. This will

42−executable called ``hello``, which you can run:

43+create an executable called ``hello``, which you can run:

44::

45::

@@ -49,16 +50,16 @@ executable called ``hello``, which you can run:

50Note that the ``$`` indicates the shell prompt! Should the ``Idris``

51Note that the ``$`` indicates the shell prompt! Should the ``Idris``

51executable not be found please ensure that you have added

52executable not be found please ensure that you have added

52−``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X users

53+``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X

53−may find they need to use ``~/Library/Haskell/bin`` instead. Some useful

54+users may find they need to use ``~/Library/Haskell/bin``

54−options to the ``Idris`` command are:

55+instead. Some useful options to the ``Idris`` command are:

56−- ``-o prog`` to compile to an executable called ``prog``.

57+- ``-o prog`` to compile to an executable called ``prog``.

58−- ``--check`` type check the file and its dependencies without starting

59+- ``--check`` type check the file and its dependencies without

59− the interactive environment.

60+ starting the interactive environment.

61−- ``--help`` display usage summary and command line options

62+- ``--help`` display usage summary and command line options

63The Interactive Environment

64The Interactive Environment

64---------------------------

65---------------------------

@@ -71,12 +72,12 @@ environment. You should see something like the following:

71This gives a ``ghci`` style interface which allows evaluation of, as

72This gives a ``ghci`` style interface which allows evaluation of, as

72well as type checking of, expressions; theorem proving, compilation;

73well as type checking of, expressions; theorem proving, compilation;

73editing; and various other operations. The command ``:?`` gives a list

74editing; and various other operations. The command ``:?`` gives a list

74−of supported commands. Listing :ref:`run1` shows an example run in which

75+of supported commands. Listing :ref:`run1` shows an example run in

75−``hello.idr`` is loaded, the type of ``main`` is checked and then the

76+which ``hello.idr`` is loaded, the type of ``main`` is checked and

76−program is compiled to the executable ``hello``. Type checking a file,

77+then the program is compiled to the executable ``hello``. Type

77−if successful, creates a bytecode version of the file (in this case

78+checking a file, if successful, creates a bytecode version of the file

78−``hello.ibc``) to speed up loading in future. The bytecode is

79+(in this case ``hello.ibc``) to speed up loading in future. The

79−regenerated if the source file changes.

80+bytecode is regenerated if the source file changes.

81.. literalinclude:: ../listing/idris-prompt-helloworld.txt

82.. literalinclude:: ../listing/idris-prompt-helloworld.txt

82 :caption: Sample Interactive Run

83 :caption: Sample Interactive Run

docs/tutorial/syntax.rst+38−39

@@ -2,18 +2,17 @@ Syntax Extensions

2=================

4supports the implementation of *Embedded Domain Specific Languages*

5−(EDSLs) in several ways [1]_. One way, as we have

5+(EDSLs) in several ways [1]_. One way, as we have already seen, is

6−already seen, is through extending ``do`` notation. Another important

6+through extending ``do`` notation. Another important way is to allow

7−way is to allow extension of the core syntax. In this section we

7+extension of the core syntax. In this section we describe two ways of

8−describe two ways of extending the syntax: ``syntax`` rules and ``dsl``

8+extending the syntax: ``syntax`` rules and ``dsl`` notation.

9−notation.

11``syntax`` rules

10``syntax`` rules

12----------------

11----------------

14We have seen ``if...then...else`` expressions, but these are not built

13We have seen ``if...then...else`` expressions, but these are not built

15−in. Instead, we can define a function in the prelude as follows (we have

14+in. Instead, we can define a function in the prelude as follows (we

16−already seen this function in Section :ref:`sect-lazy`):

15+have already seen this function in Section :ref:`sect-lazy`):

18.. code-block:: idris

17.. code-block:: idris

@@ -46,13 +45,13 @@ itself consists of:

46 also be used to include reserved words in syntax rules, such as

45 also be used to include reserved words in syntax rules, such as

47 ``let`` or ``in``.

46 ``let`` or ``in``.

49−The limitations on the form of a syntax rule are that it must include at

48+The limitations on the form of a syntax rule are that it must include

50−least one symbol or keyword, and there must be no repeated variables

49+at least one symbol or keyword, and there must be no repeated

51−standing for non-terminals. Any expression can be used, but if there are

50+variables standing for non-terminals. Any expression can be used, but

52−two non-terminals in a row in a rule, only simple expressions may be

51+if there are two non-terminals in a row in a rule, only simple

53−used (that is, variables, constants, or bracketed expressions). Rules

52+expressions may be used (that is, variables, constants, or bracketed

54−can use previously defined rules, but may not be recursive. The

53+expressions). Rules can use previously defined rules, but may not be

55−following syntax extensions would therefore be valid:

54+recursive. The following syntax extensions would therefore be valid:

57.. code-block:: idris

56.. code-block:: idris

@@ -63,7 +62,7 @@ following syntax extensions would therefore be valid:

64Syntax macros can be further restricted to apply only in patterns (i.e.,

63Syntax macros can be further restricted to apply only in patterns (i.e.,

65only on the left hand side of a pattern match clause) or only in terms

64only on the left hand side of a pattern match clause) or only in terms

66−(i.e. everywhere but the left hand side of a pattern match clause) by

65+(i.e. everywhere but the left hand side of a pattern match clause) by

67being marked as ``pattern`` or ``term`` syntax rules. For example, we

66being marked as ``pattern`` or ``term`` syntax rules. For example, we

68might define an interval as follows, with a static check that the lower

67might define an interval as follows, with a static check that the lower

69bound is below the upper bound using ``so``:

68bound is below the upper bound using ``so``:

@@ -74,8 +73,8 @@ bound is below the upper bound using ``so``:

74 MkInterval : (lower : Float) -> (upper : Float) ->

73 MkInterval : (lower : Float) -> (upper : Float) ->

75 so (lower < upper) -> Interval

74 so (lower < upper) -> Interval

77−We can define a syntax which, in patterns, always matches ``oh`` for the

76+We can define a syntax which, in patterns, always matches ``oh`` for

78−proof argument, and in terms requires a proof term to be provided:

77+the proof argument, and in terms requires a proof term to be provided:

80.. code-block:: idris

79.. code-block:: idris

@@ -97,23 +96,23 @@ forms. For example, a ``for`` loop binds a variable on each iteration:

97 putStrLn ("Number " ++ show x)

96 putStrLn ("Number " ++ show x)

98 putStrLn "Done!"

97 putStrLn "Done!"

100−Note that we have used the ``{x}`` form to state that ``x`` represents a

99+Note that we have used the ``{x}`` form to state that ``x`` represents

101−bound variable, substituted on the right hand side. We have also put

100+a bound variable, substituted on the right hand side. We have also put

102``in`` in quotation marks since it is already a reserved word.

101``in`` in quotation marks since it is already a reserved word.

103

102

104``dsl`` notation

103``dsl`` notation

105----------------

104----------------

106

105

107−The well-typed interpreter in Section :ref:`sect-interp` is a simple example

106+The well-typed interpreter in Section :ref:`sect-interp` is a simple

108−of a common programming pattern with dependent types. Namely: describe

107+example of a common programming pattern with dependent types. Namely:

109−an *object language* and its type system with dependent types to

108+describe an *object language* and its type system with dependent types

110−guarantee that only well-typed programs can be represented, then program

109+to guarantee that only well-typed programs can be represented, then

111−using that representation. Using this approach we can, for example,

110+program using that representation. Using this approach we can, for

112−write programs for serialising binary data [2]_ or running

111+example, write programs for serialising binary data [2]_ or running

113concurrent processes safely [3]_.

112concurrent processes safely [3]_.

114

113

115−Unfortunately, the form of object language programs makes it rather hard

114+Unfortunately, the form of object language programs makes it rather

116−to program this way in practice. Recall the factorial program in

115+hard to program this way in practice. Recall the factorial program in

117``Expr`` for example:

116``Expr`` for example:

118

117

119.. code-block:: idris

118.. code-block:: idris

@@ -124,8 +123,8 @@ to program this way in practice. Recall the factorial program in

124 (Var Stop)))

123 (Var Stop)))

125

124

126Since this is a particularly useful pattern, ``Idris`` provides syntax

125Since this is a particularly useful pattern, ``Idris`` provides syntax

127−overloading [1]_ to make it easier to program in such

126+overloading [1]_ to make it easier to program in such object

128−object languages:

127+languages:

129

128

130.. code-block:: idris

129.. code-block:: idris

131

130

@@ -138,15 +137,15 @@ object languages:

138 index_next = Pop

137 index_next = Pop

139 lambda = mkLam

138 lambda = mkLam

140

139

141−A ``dsl`` block describes how each syntactic construct is represented in

140+A ``dsl`` block describes how each syntactic construct is represented

142−an object language. Here, in the ``expr`` language, any variable is

141+in an object language. Here, in the ``expr`` language, any variable is

143translated to the ``Var`` constructor, using ``Pop`` and ``Stop`` to

142translated to the ``Var`` constructor, using ``Pop`` and ``Stop`` to

144construct the de Bruijn index (i.e., to count how many bindings since

143construct the de Bruijn index (i.e., to count how many bindings since

145the variable itself was bound); and any lambda is translated to a

144the variable itself was bound); and any lambda is translated to a

146``Lam`` constructor. The ``mkLam`` function simply ignores its first

145``Lam`` constructor. The ``mkLam`` function simply ignores its first

147−argument, which is the name that the user chose for the variable. It is

146+argument, which is the name that the user chose for the variable. It

148−also possible to overload ``let`` and dependent function syntax (``pi``)

147+is also possible to overload ``let`` and dependent function syntax

149−in this way. We can now write ``fact`` as follows:

148+(``pi``) in this way. We can now write ``fact`` as follows:

150

149

151.. code-block:: idris

150.. code-block:: idris

152

151

@@ -154,8 +153,8 @@ in this way. We can now write ``fact`` as follows:

154 fact = expr (\x => If (Op (==) x (Val 0))

153 fact = expr (\x => If (Op (==) x (Val 0))

155 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))

154 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))

156

155

157−In this new version, ``expr`` declares that the next expression will be

156+In this new version, ``expr`` declares that the next expression will

158−overloaded. We can take this further, using idiom brackets, by

157+be overloaded. We can take this further, using idiom brackets, by

159declaring:

158declaring:

160

159

161.. code-block:: idris

160.. code-block:: idris

@@ -167,9 +166,9 @@ declaring:

167 pure = id

166 pure = id

168

167

169Note that there is no need for these to be part of an instance of

168Note that there is no need for these to be part of an instance of

170−``Applicative``, since idiom bracket notation translates directly to the

169+``Applicative``, since idiom bracket notation translates directly to

171−names ``<*>`` and ``pure``, and ad-hoc type-directed overloading is

170+the names ``<*>`` and ``pure``, and ad-hoc type-directed overloading

172−allowed. We can now say:

171+is allowed. We can now say:

173

172

174.. code-block:: idris

173.. code-block:: idris

175

174

docs/tutorial/typesfuns.rst+203−188

@@ -1,3 +1,5 @@

1+.. _sect-typefuns:

1===================

3===================

2Types and Functions

4Types and Functions

3===================

5===================

@@ -11,8 +13,8 @@ manipulation, and ``Ptr`` which represents foreign pointers. There are

11also several data types declared in the library, including ``Bool``,

13also several data types declared in the library, including ``Bool``,

12with values ``True`` and ``False``. We can declare some constants with

14with values ``True`` and ``False``. We can declare some constants with

13these types. Enter the following into a file ``prims.idr`` and load it

15these types. Enter the following into a file ``prims.idr`` and load it

14−into the ``Idris`` interactive environment by typing

16+into the ``Idris`` interactive environment by typing ``idris

15−``idris prims.idr``:

17+prims.idr``:

17.. code-block:: idris

19.. code-block:: idris

@@ -34,13 +36,14 @@ An ``Idris`` file consists of an optional module declaration (here

34``module prims``) followed by an optional list of imports (none here,

36``module prims``) followed by an optional list of imports (none here,

35however ``Idris`` programs can consist of several modules, and the

37however ``Idris`` programs can consist of several modules, and the

36definitions in each module each have their own namespace, as we will

38definitions in each module each have their own namespace, as we will

37−discuss in Section :ref:`sect-namespaces`) and a collection of declarations

39+discuss in Section :ref:`sect-namespaces`) and a collection of

38−and definitions. The order of definitions is significant — functions and

40+declarations and definitions. The order of definitions is significant

39−data types must be defined before use. Each definition must have a type

41+— functions and data types must be defined before use. Each definition

40−declaration, for example see ``x : Int``, ``foo : String``, from the

42+must have a type declaration, for example see ``x : Int``, ``foo :

41−above listing. Indentation is significant — a new declaration begins at

43+String``, from the above listing. Indentation is significant — a new

42−the same level of indentation as the preceding declaration.

44+declaration begins at the same level of indentation as the preceding

43−Alternatively, declarations may be terminated with a semicolon.

45+declaration. Alternatively, declarations may be terminated with a

46+semicolon.

45A library module ``prelude`` is automatically imported by every

48A library module ``prelude`` is automatically imported by every

46``Idris`` program, including facilities for IO, arithmetic, data

49``Idris`` program, including facilities for IO, arithmetic, data

@@ -56,10 +59,10 @@ answer. For example:

56 *prims> x == 6*6+6

59 *prims> x == 6*6+6

57 True : Bool

60 True : Bool

59−All of the usual arithmetic and comparison operators are defined for the

62+All of the usual arithmetic and comparison operators are defined for

60−primitive types. They are overloaded using type classes, as we will

63+the primitive types. They are overloaded using type classes, as we

61−discuss in Section :ref:`sect-classes` and can be extended to work on user

64+will discuss in Section :ref:`sect-classes` and can be extended to

62−defined types. Boolean expressions can be tested with the

65+work on user defined types. Boolean expressions can be tested with the

63``if...then...else`` construct:

66``if...then...else`` construct:

65::

68::

@@ -71,8 +74,8 @@ Data Types

71----------

74----------

73Data types are declared in a similar way to Haskell data types, with a

76Data types are declared in a similar way to Haskell data types, with a

74−similar syntax. Natural numbers and lists, for example, can be declared

77+similar syntax. Natural numbers and lists, for example, can be

75−as follows:

78+declared as follows:

77.. code-block:: idris

80.. code-block:: idris

@@ -81,19 +84,21 @@ as follows:

81 data List a = Nil | (::) a (List a) -- Polymorphic lists

84 data List a = Nil | (::) a (List a) -- Polymorphic lists

83The above declarations are taken from the standard library. Unary

86The above declarations are taken from the standard library. Unary

84−natural numbers can be either zero (``Z``), or the successor of another

87+natural numbers can be either zero (``Z``), or the successor of

85−natural number (``S k``). Lists can either be empty (``Nil``) or a value

88+another natural number (``S k``). Lists can either be empty (``Nil``)

86−added to the front of another list (``x :: xs``). In the declaration for

89+or a value added to the front of another list (``x :: xs``). In the

87−``List``, we used an infix operator ``::``. New operators such as this

90+declaration for ``List``, we used an infix operator ``::``. New

88−can be added using a fixity declaration, as follows:

91+operators such as this can be added using a fixity declaration, as

92+follows:

90::

94::

92 infixr 10 ::

96 infixr 10 ::

94Functions, data constructors and type constructors may all be given

98Functions, data constructors and type constructors may all be given

95−infix operators as names. They may be used in prefix form if enclosed in

99+infix operators as names. They may be used in prefix form if enclosed

96−brackets, e.g. \ ``(::)``. Infix operators can use any of the symbols:

100+in brackets, e.g. ``(::)``. Infix operators can use any of the

101+symbols:

102

98::

103::

104

@@ -104,9 +109,10 @@ Functions

104

109

105Functions are implemented by pattern matching, again using a similar

110Functions are implemented by pattern matching, again using a similar

106syntax to Haskell. The main difference is that ``Idris`` requires type

111syntax to Haskell. The main difference is that ``Idris`` requires type

107−declarations for all functions, using a single colon ``:`` (rather than

112+declarations for all functions, using a single colon ``:`` (rather

108−Haskell’s double colon ``::``). Some natural number arithmetic functions

113+than Haskell’s double colon ``::``). Some natural number arithmetic

109−can be defined as follows, again taken from the standard library:

114+functions can be defined as follows, again taken from the standard

115+library:

110

116

111.. code-block:: idris

117.. code-block:: idris

112

118

@@ -123,10 +129,11 @@ can be defined as follows, again taken from the standard library:

123The standard arithmetic operators ``+`` and ``*`` are also overloaded

129The standard arithmetic operators ``+`` and ``*`` are also overloaded

124for use by ``Nat``, and are implemented using the above functions.

130for use by ``Nat``, and are implemented using the above functions.

125Unlike Haskell, there is no restriction on whether types and function

131Unlike Haskell, there is no restriction on whether types and function

126−names must begin with a capital letter or not. Function names (``plus``

132+names must begin with a capital letter or not. Function names

127−and ``mult`` above), data constructors (``Z``, ``S``, ``Nil`` and

133+(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,

128−``::``) and type constructors (``Nat`` and ``List``) are all part of the

134+``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are

129−same namespace. We can test these functions at the ``Idris`` prompt:

135+all part of the same namespace. We can test these functions at the

136+``Idris`` prompt:

130

137

131::

138::

132

139

@@ -135,10 +142,12 @@ same namespace. We can test these functions at the ``Idris`` prompt:

135 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))

142 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))

136 12 : Nat

143 12 : Nat

137

144

145+.. note::

146+

138−**Note:** ``Idris`` automatically desugars the ``Nat`` representation

147+ ``Idris`` automatically desugars the ``Nat`` representation into a

139−into a more human readable format. The result of

148+ more human readable format. The result of ``plus (S (S Z)) (S (S Z))``

140−``plus (S (S Z)) (S (S Z))`` is actually ``(S (S (S (S Z))))`` which is

149+ is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be

141−the Integer 4. This can be checked at the ``Idris`` prompt:

150+ checked at the ``Idris`` prompt:

142

151

143::

152::

144

153

@@ -156,12 +165,12 @@ type classes, meaning that we can also test the functions as follows:

156 12 : Nat

165 12 : Nat

157

166

158You may wonder, by the way, why we have unary natural numbers when our

167You may wonder, by the way, why we have unary natural numbers when our

159−computers have perfectly good integer arithmetic built in. The reason is

168+computers have perfectly good integer arithmetic built in. The reason

160−primarily that unary numbers have a very convenient structure which is

169+is primarily that unary numbers have a very convenient structure which

161−easy to reason about, and easy to relate to other data structures as we

170+is easy to reason about, and easy to relate to other data structures

162−will see later. Nevertheless, we do not want this convenience to be at

171+as we will see later. Nevertheless, we do not want this convenience to

163−the expense of efficiency. Fortunately, ``Idris`` knows about the

172+be at the expense of efficiency. Fortunately, ``Idris`` knows about

164−relationship between ``Nat`` (and similarly structured types) and

173+the relationship between ``Nat`` (and similarly structured types) and

165numbers. This means it can optimise the representation, and functions

174numbers. This means it can optimise the representation, and functions

166such as ``plus`` and ``mult``.

175such as ``plus`` and ``mult``.

167

176

@@ -188,7 +197,7 @@ indented further than the outer function.

188visible in the ``where`` clause (unless they have been redefined, such

197visible in the ``where`` clause (unless they have been redefined, such

189as ``xs`` here). A name which appears only in the type will be in scope

198as ``xs`` here). A name which appears only in the type will be in scope

190in the ``where`` clause if it is a *parameter* to one of the types,

199in the ``where`` clause if it is a *parameter* to one of the types,

191−i.e. it is fixed across the entire structure.

200+i.e. it is fixed across the entire structure.

192

201

193As well as functions, ``where`` blocks can include local data

202As well as functions, ``where`` blocks can include local data

194declarations, such as the following where ``MyLT`` is not accessible

203declarations, such as the following where ``MyLT`` is not accessible

@@ -210,9 +219,9 @@ In general, functions defined in a ``where`` clause need a type

210declaration just like any top level function. However, the type

219declaration just like any top level function. However, the type

211declaration for a function ``f`` *can* be omitted if:

220declaration for a function ``f`` *can* be omitted if:

212

221

213−- ``f`` appears in the right hand side of the top level definition

222+- ``f`` appears in the right hand side of the top level definition

214

223

215−- The type of ``f`` can be completely determined from its first

224+- The type of ``f`` can be completely determined from its first

216 application

225 application

217

226

218So, for example, the following definitions are legal:

227So, for example, the following definitions are legal:

@@ -238,9 +247,9 @@ Vectors

238~~~~~~~

247~~~~~~~

239

248

240A standard example of a dependent type is the type of “lists with

249A standard example of a dependent type is the type of “lists with

241−length”, conventionally called vectors in the dependent type literature.

250+length”, conventionally called vectors in the dependent type

242−They are available as part of the ``Idris`` library, by importing

251+literature. They are available as part of the ``Idris`` library, by

243−``Data.Vect``, or we can declare them as follows:

252+importing ``Data.Vect``, or we can declare them as follows:

244

253

245.. code-block:: idris

254.. code-block:: idris

246

255

@@ -249,28 +258,28 @@ They are available as part of the ``Idris`` library, by importing

249 (::) : a -> Vect k a -> Vect (S k) a

258 (::) : a -> Vect k a -> Vect (S k) a

250

259

251Note that we have used the same constructor names as for ``List``.

260Note that we have used the same constructor names as for ``List``.

252−Ad-hoc name overloading such as this is accepted by ``Idris``, provided

261+Ad-hoc name overloading such as this is accepted by ``Idris``,

253−that the names are declared in different namespaces (in practice,

262+provided that the names are declared in different namespaces (in

254−normally in different modules). Ambiguous constructor names can normally

263+practice, normally in different modules). Ambiguous constructor names

255−be resolved from context.

264+can normally be resolved from context.

256

265

257This declares a family of types, and so the form of the declaration is

266This declares a family of types, and so the form of the declaration is

258−rather different from the simple type declarations above. We explicitly

267+rather different from the simple type declarations above. We

259−state the type of the type constructor ``Vect`` — it takes a ``Nat`` and

268+explicitly state the type of the type constructor ``Vect`` — it takes

260−a type as an argument, where ``Type`` stands for the type of types. We

269+a ``Nat`` and a type as an argument, where ``Type`` stands for the

261−say that ``Vect`` is *indexed* over ``Nat`` and *parameterised* by

270+type of types. We say that ``Vect`` is *indexed* over ``Nat`` and

262−``Type``. Each constructor targets a different part of the family of

271+*parameterised* by ``Type``. Each constructor targets a different part

263−types. ``Nil`` can only be used to construct vectors with zero length,

272+of the family of types. ``Nil`` can only be used to construct vectors

264−and ``::`` to construct vectors with non-zero length. In the type of

273+with zero length, and ``::`` to construct vectors with non-zero

265−``::``, we state explicitly that an element of type ``a`` and a tail of

274+length. In the type of ``::``, we state explicitly that an element of

266−type ``Vect k a`` (i.e., a vector of length ``k``) combine to make a

275+type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length

267−vector of length ``S k``.

276+``k``) combine to make a vector of length ``S k``.

268

277

269We can define functions on dependent types such as ``Vect`` in the same

278We can define functions on dependent types such as ``Vect`` in the same

270way as on simple types such as ``List`` and ``Nat`` above, by pattern

279way as on simple types such as ``List`` and ``Nat`` above, by pattern

271matching. The type of a function over ``Vect`` will describe what

280matching. The type of a function over ``Vect`` will describe what

272happens to the lengths of the vectors involved. For example, ``++``,

281happens to the lengths of the vectors involved. For example, ``++``,

273−defined as follows, appends two ``Vect``\ s:

282+defined as follows, appends two ``Vect``:

274

283

275.. code-block:: idris

284.. code-block:: idris

276

285

@@ -308,9 +317,9 @@ following:

308 with

317 with

309 plus k m

318 plus k m

310

319

311−This error message suggests that there is a length mismatch between two

320+This error message suggests that there is a length mismatch between

312−vectors — we needed a vector of length ``k + m``, but provided a vector

321+two vectors — we needed a vector of length ``k + m``, but provided a

313−of length ``k + k``.

322+vector of length ``k + k``.

314

323

315The Finite Sets

324The Finite Sets

316~~~~~~~~~~~~~~~

325~~~~~~~~~~~~~~~

@@ -332,9 +341,9 @@ of elements in the set. Obviously we can’t construct an element of an

332empty set, so neither constructor targets ``Fin Z``.

341empty set, so neither constructor targets ``Fin Z``.

333

342

334A useful application of the ``Fin`` family is to represent bounded

343A useful application of the ``Fin`` family is to represent bounded

335−natural numbers. Since the first ``n`` natural numbers form a finite set

344+natural numbers. Since the first ``n`` natural numbers form a finite

336−of ``n`` elements, we can treat ``Fin n`` as the set of natural numbers

345+set of ``n`` elements, we can treat ``Fin n`` as the set of natural

337−bounded by ``n``.

346+numbers bounded by ``n``.

338

347

339For example, the following function which looks up an element in a

348For example, the following function which looks up an element in a

340``Vect``, by a bounded index given as a ``Fin n``, is defined in the

349``Vect``, by a bounded index given as a ``Fin n``, is defined in the

@@ -347,15 +356,16 @@ prelude:

347 index (FS k) (x :: xs) = index k xs

356 index (FS k) (x :: xs) = index k xs

348

357

349This function looks up a value at a given location in a vector. The

358This function looks up a value at a given location in a vector. The

350−location is bounded by the length of the vector (``n`` in each case), so

359+location is bounded by the length of the vector (``n`` in each case),

351−there is no need for a run-time bounds check. The type checker

360+so there is no need for a run-time bounds check. The type checker

352−guarantees that the location is no larger than the length of the vector.

361+guarantees that the location is no larger than the length of the

362+vector.

353

363

354−Note also that there is no case for ``Nil`` here. This is because it is

364+Note also that there is no case for ``Nil`` here. This is because it

355−impossible. Since there is no element of ``Fin Z``, and the location is

365+is impossible. Since there is no element of ``Fin Z``, and the

356−a ``Fin n``, then ``n`` can not be ``Z``. As a result, attempting to

366+location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,

357−look up an element in an empty vector would give a compile time type

367+attempting to look up an element in an empty vector would give a

358−error, since it would force ``n`` to be ``Z``.

368+compile time type error, since it would force ``n`` to be ``Z``.

359

369

360Implicit Arguments

370Implicit Arguments

361~~~~~~~~~~~~~~~~~~

371~~~~~~~~~~~~~~~~~~

@@ -376,13 +386,14 @@ names, ``n`` and ``a``, which are not declared explicitly. These are

376

386

377 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

387 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

378

388

379−Implicit arguments, given in braces ``{}`` in the type declaration, are

389+Implicit arguments, given in braces ``{}`` in the type declaration,

380−not given in applications of ``index``; their values can be inferred

390+are not given in applications of ``index``; their values can be

381−from the types of the ``Fin n`` and ``Vect n a`` arguments. Any name

391+inferred from the types of the ``Fin n`` and ``Vect n a``

382−with a which appears as a parameter or index in a type declaration, but

392+arguments. Any name with a which appears as a parameter or index in a

383−which is otherwise free, will be automatically bound as an implicit

393+type declaration, but which is otherwise free, will be automatically

384−argument. Implicit arguments can still be given explicitly in

394+bound as an implicit argument. Implicit arguments can still be given

385−applications, using ``{a=value}`` and ``{n=value}``, for example:

395+explicitly in applications, using ``{a=value}`` and ``{n=value}``, for

396+example:

386

397

387.. code-block:: idris

398.. code-block:: idris

388

399

@@ -403,10 +414,10 @@ clear.

403~~~~~~~~~~~~~~~~~~~~

414~~~~~~~~~~~~~~~~~~~~

404

415

405Sometimes it is useful to provide types of implicit arguments,

416Sometimes it is useful to provide types of implicit arguments,

406−particularly where there is a dependency ordering, or where the implicit

417+particularly where there is a dependency ordering, or where the

407−arguments themselves have dependencies. For example, we may wish to

418+implicit arguments themselves have dependencies. For example, we may

408−state the types of the implicit arguments in the following definition,

419+wish to state the types of the implicit arguments in the following

409−which defines a predicate on vectors:

420+definition, which defines a predicate on vectors:

410

421

411.. code-block:: idris

422.. code-block:: idris

412

423

@@ -414,10 +425,10 @@ which defines a predicate on vectors:

414 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

425 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

415 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

426 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

416

427

417−An instance of ``Elem x xs`` states that ``x`` is an element of ``xs``.

428+An instance of ``Elem x xs`` states that ``x`` is an element of

418−We can construct such a predicate if the required element is ``Here``,

429+``xs``. We can construct such a predicate if the required element is

419−at the head of the vector, or ``There``, in the tail of the vector. For

430+``Here``, at the head of the vector, or ``There``, in the tail of the

420−example:

431+vector. For example:

421

432

422.. code-block:: idris

433.. code-block:: idris

423

434

@@ -429,8 +440,8 @@ example:

429

440

430If the same implicit arguments are being used a lot, it can make a

441If the same implicit arguments are being used a lot, it can make a

431definition difficult to read. To avoid this problem, a ``using`` block

442definition difficult to read. To avoid this problem, a ``using`` block

432−gives the types and ordering of any implicit arguments which can appear

443+gives the types and ordering of any implicit arguments which can

433−within the block:

444+appear within the block:

434

445

435.. code-block:: idris

446.. code-block:: idris

436

447

@@ -445,8 +456,8 @@ Note: Declaration Order and ``mutual`` blocks

445In general, functions and data types must be defined before use, since

456In general, functions and data types must be defined before use, since

446dependent types allow functions to appear as part of types, and their

457dependent types allow functions to appear as part of types, and their

447reduction behaviour to affect type checking. However, this restriction

458reduction behaviour to affect type checking. However, this restriction

448−can be relaxed by using a ``mutual`` block, which allows data types and

459+can be relaxed by using a ``mutual`` block, which allows data types

449−functions to be defined simultaneously:

460+and functions to be defined simultaneously:

450

461

451.. code-block:: idris

462.. code-block:: idris

452

463

@@ -461,7 +472,8 @@ functions to be defined simultaneously:

461

472

462In a ``mutual`` block, first all of the type declarations are added,

473In a ``mutual`` block, first all of the type declarations are added,

463then the function bodies. As a result, none of the function types can

474then the function bodies. As a result, none of the function types can

464−depend on the reduction behaviour of any of the functions in the block.

475+depend on the reduction behaviour of any of the functions in the

476+block.

465

477

466I/O

478I/O

467---

479---

@@ -477,18 +489,18 @@ side-effects — is that I/O is inherently side-effecting. Therefore in

477 data IO a -- IO operation returning a value of type a

489 data IO a -- IO operation returning a value of type a

478

490

479We’ll leave the definition of ``IO`` abstract, but effectively it

491We’ll leave the definition of ``IO`` abstract, but effectively it

480−describes what the I/O operations to be executed are, rather than how to

492+describes what the I/O operations to be executed are, rather than how

481−execute them. The resulting operations are executed externally, by the

493+to execute them. The resulting operations are executed externally, by

482−run-time system. We’ve already seen one IO program:

494+the run-time system. We’ve already seen one IO program:

483

495

484.. code-block:: idris

496.. code-block:: idris

485

497

486 main : IO ()

498 main : IO ()

487 main = putStrLn "Hello world"

499 main = putStrLn "Hello world"

488

500

489−The type of ``putStrLn`` explains that it takes a string, and returns an

501+The type of ``putStrLn`` explains that it takes a string, and returns

490−element of the unit type ``()`` via an I/O action. There is a variant

502+an element of the unit type ``()`` via an I/O action. There is a

491−``putStr`` which outputs a string without a newline:

503+variant ``putStr`` which outputs a string without a newline:

492

504

493.. code-block:: idris

505.. code-block:: idris

494

506

@@ -501,8 +513,8 @@ We can also read strings from user input:

501

513

502 getLine : IO String

514 getLine : IO String

503

515

504−A number of other I/O operations are defined in the prelude, for example

516+A number of other I/O operations are defined in the prelude, for

505−for reading and writing files, including:

517+example for reading and writing files, including:

506

518

507.. code-block:: idris

519.. code-block:: idris

508

520

@@ -523,10 +535,10 @@ for reading and writing files, including:

523“``do``” notation

535“``do``” notation

524-----------------

536-----------------

525

537

526−I/O programs will typically need to sequence actions, feeding the output

538+I/O programs will typically need to sequence actions, feeding the

527−of one computation into the input of the next. ``IO`` is an abstract

539+output of one computation into the input of the next. ``IO`` is an

528−type, however, so we can’t access the result of a computation directly.

540+abstract type, however, so we can’t access the result of a computation

529−Instead, we sequence operations with ``do`` notation:

541+directly. Instead, we sequence operations with ``do`` notation:

530

542

531.. code-block:: idris

543.. code-block:: idris

532

544

@@ -538,16 +550,16 @@ Instead, we sequence operations with ``do`` notation:

538The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of

550The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of

539type ``IO a``, and puts the result, of type ``a`` into the variable

551type ``IO a``, and puts the result, of type ``a`` into the variable

540``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``

552``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``

541−has type ``String``. Indentation is significant — each statement in the

553+has type ``String``. Indentation is significant — each statement in

542−do block must begin in the same column. The ``return`` operation allows

554+the do block must begin in the same column. The ``return`` operation

543−us to inject a value directly into an IO operation:

555+allows us to inject a value directly into an IO operation:

544

556

545.. code-block:: idris

557.. code-block:: idris

546

558

547 return : a -> IO a

559 return : a -> IO a

548

560

549−As we will see later, ``do`` notation is more general than this, and can

561+As we will see later, ``do`` notation is more general than this, and

550−be overloaded.

562+can be overloaded.

551

563

552.. _sect-lazy:

564.. _sect-lazy:

553

565

@@ -564,11 +576,11 @@ not always the best approach. Consider the following function:

564 boolCase True t e = t;

576 boolCase True t e = t;

565 boolCase False t e = e;

577 boolCase False t e = e;

566

578

567−This function uses one of the ``t`` or ``e`` arguments, but not both (in

579+This function uses one of the ``t`` or ``e`` arguments, but not both

568−fact, this is used to implement the ``if...then...else`` construct as we

580+(in fact, this is used to implement the ``if...then...else`` construct

569−will see later. We would prefer if *only* the argument which was used

581+as we will see later. We would prefer if *only* the argument which was

570−was evaluated. To achieve this, ``Idris`` provides a ``Lazy`` data type,

582+used was evaluated. To achieve this, ``Idris`` provides a ``Lazy``

571−which allows evaluation to be suspended:

583+data type, which allows evaluation to be suspended:

572

584

573.. code-block:: idris

585.. code-block:: idris

574

586

@@ -578,10 +590,10 @@ which allows evaluation to be suspended:

578 Force : Lazy a -> a

590 Force : Lazy a -> a

579

591

580A value of type ``Lazy a`` is unevaluated until it is forced by

592A value of type ``Lazy a`` is unevaluated until it is forced by

581−``Force``. The ``Idris`` type checker knows about the ``Lazy`` type, and

593+``Force``. The ``Idris`` type checker knows about the ``Lazy`` type,

582−inserts conversions where necessary between ``Lazy a`` and ``a``, and

594+and inserts conversions where necessary between ``Lazy a`` and ``a``,

583−vice versa. We can therefore write ``boolCase`` as follows, without any

595+and vice versa. We can therefore write ``boolCase`` as follows,

584−explicit use of ``Force`` or ``Delay``:

596+without any explicit use of ``Force`` or ``Delay``:

585

597

586.. code-block:: idris

598.. code-block:: idris

587

599

@@ -611,19 +623,19 @@ We have already seen the ``List`` and ``Vect`` data types:

611 (::) : a -> Vect k a -> Vect (S k) a

623 (::) : a -> Vect k a -> Vect (S k) a

612

624

613Note that the constructor names are the same for each — constructor

625Note that the constructor names are the same for each — constructor

614−names (in fact, names in general) can be overloaded, provided that they

626+names (in fact, names in general) can be overloaded, provided that

615−are declared in different namespaces (see Section :ref:`sect-namespaces`),

627+they are declared in different namespaces (see Section

616−and will typically be resolved according to their type. As syntactic

628+:ref:`sect-namespaces`), and will typically be resolved according to

617−sugar, any type with the constructor names ``Nil`` and ``::`` can be

629+their type. As syntactic sugar, any type with the constructor names

618−written in list form. For example:

630+``Nil`` and ``::`` can be written in list form. For example:

619

631

620- ``[]`` means ``Nil``

632- ``[]`` means ``Nil``

621

633

622- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``

634- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``

623

635

624The library also defines a number of functions for manipulating these

636The library also defines a number of functions for manipulating these

625−types. ``map`` is overloaded both for ``List`` and ``Vect`` and applies

637+types. ``map`` is overloaded both for ``List`` and ``Vect`` and

626−a function to every element of the list or vector.

638+applies a function to every element of the list or vector.

627

639

628.. code-block:: idris

640.. code-block:: idris

629

641

@@ -667,8 +679,8 @@ directory. For more details of the functions available on ``List`` and

667- ``libs/base/Data/VectType.idr``

679- ``libs/base/Data/VectType.idr``

668

680

669Functions include filtering, appending, reversing, and so on. Also

681Functions include filtering, appending, reversing, and so on. Also

670−remember that ``Idris`` is still in development, so if you don’t see the

682+remember that ``Idris`` is still in development, so if you don’t see

671−function you need, please feel free to add it and submit a patch!

683+the function you need, please feel free to add it and submit a patch!

672

684

673Aside: Anonymous functions and operator sections

685Aside: Anonymous functions and operator sections

674~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

686~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -684,18 +696,18 @@ would be to use an anonymous function:

684The notation ``\x => val`` constructs an anonymous function which takes

696The notation ``\x => val`` constructs an anonymous function which takes

685one argument, ``x`` and returns the expression ``val``. Anonymous

697one argument, ``x`` and returns the expression ``val``. Anonymous

686functions may take several arguments, separated by commas,

698functions may take several arguments, separated by commas,

687−e.g. \ ``\x, y, z => val``. Arguments may also be given explicit types,

699+e.g. ``\x, y, z => val``. Arguments may also be given explicit types,

688−e.g. \ ``\x : Int => x * 2``, and can pattern match,

700+e.g. ``\x : Int => x * 2``, and can pattern match,

689−e.g. \ ``\(x, y) => x + y``. We could also use an operator section:

701+e.g. ``\(x, y) => x + y``. We could also use an operator section:

690

702

691::

703::

692

704

693 *usefultypes> show (map (* 2) intVec)

705 *usefultypes> show (map (* 2) intVec)

694 "[2, 4, 6, 8, 10]" : String

706 "[2, 4, 6, 8, 10]" : String

695

707

696−``(*2)`` is shorthand for a function which multiplies a number by 2. It

708+``(*2)`` is shorthand for a function which multiplies a number

697−expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand to

709+by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand

698−``\x => 2 * x``.

710+to ``\x => 2 * x``.

699

711

700Maybe

712Maybe

701~~~~~

713~~~~~

@@ -707,9 +719,9 @@ given type, or there isn’t:

707

719

708 data Maybe a = Just a | Nothing

720 data Maybe a = Just a | Nothing

709

721

710−``Maybe`` is one way of giving a type to an operation that may fail. For

722+``Maybe`` is one way of giving a type to an operation that may

711−example, looking something up in a ``List`` (rather than a vector) may

723+fail. For example, looking something up in a ``List`` (rather than a

712−result in an out of bounds error:

724+vector) may result in an out of bounds error:

713

725

714.. code-block:: idris

726.. code-block:: idris

715

727

@@ -740,9 +752,9 @@ Values can be paired with the following built-in data type:

740

752

741 data Pair a b = MkPair a b

753 data Pair a b = MkPair a b

742

754

743−As syntactic sugar, we can write ``(a, b)`` which, according to context,

755+As syntactic sugar, we can write ``(a, b)`` which, according to

744−means either ``Pair a b`` or ``MkPair a b``. Tuples can contain an

756+context, means either ``Pair a b`` or ``MkPair a b``. Tuples can

745−arbitrary number of values, represented as nested pairs:

757+contain an arbitrary number of values, represented as nested pairs:

746

758

747.. code-block:: idris

759.. code-block:: idris

748

760

@@ -766,8 +778,8 @@ as “sigma types”:

766

778

767Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

779Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

768of a pair of A and P, where the name ``a`` can occur inside ``P``.

780of a pair of A and P, where the name ``a`` can occur inside ``P``.

769−``( a ** p )`` constructs a value of this type. For example, we can pair

781+``( a ** p )`` constructs a value of this type. For example, we can

770−a number with a ``Vect`` of a particular length.

782+pair a number with a ``Vect`` of a particular length.

771

783

772.. code-block:: idris

784.. code-block:: idris

773

785

@@ -783,27 +795,28 @@ equivalent.

783 vec = MkSigma 2 [3, 4]

795 vec = MkSigma 2 [3, 4]

784

796

785The type checker could of course infer the value of the first element

797The type checker could of course infer the value of the first element

786−from the length of the vector. We can write an underscore ``_`` in place

798+from the length of the vector. We can write an underscore ``_`` in

787−of values which we expect the type checker to fill in, so the above

799+place of values which we expect the type checker to fill in, so the

788−definition could also be written as:

800+above definition could also be written as:

789

801

790.. code-block:: idris

802.. code-block:: idris

791

803

792 vec : (n : Nat ** Vect n Int)

804 vec : (n : Nat ** Vect n Int)

793 vec = (_ ** [3, 4])

805 vec = (_ ** [3, 4])

794

806

795−We might also prefer to omit the type of the first element of the pair,

807+We might also prefer to omit the type of the first element of the

796−since, again, it can be inferred:

808+pair, since, again, it can be inferred:

797

809

798.. code-block:: idris

810.. code-block:: idris

799

811

800 vec : (n ** Vect n Int)

812 vec : (n ** Vect n Int)

801 vec = (_ ** [3, 4])

813 vec = (_ ** [3, 4])

802

814

803−One use for dependent pairs is to return values of dependent types where

815+One use for dependent pairs is to return values of dependent types

804−the index is not necessarily known in advance. For example, if we filter

816+where the index is not necessarily known in advance. For example, if

805−elements out of a ``Vect`` according to some predicate, we will not know

817+we filter elements out of a ``Vect`` according to some predicate, we

806−in advance what the length of the resulting vector will be:

818+will not know in advance what the length of the resulting vector will

819+be:

807

820

808.. code-block:: idris

821.. code-block:: idris

809

822

@@ -815,9 +828,9 @@ If the ``Vect`` is empty, the result is easy:

815

828

816 filter p Nil = (_ ** [])

829 filter p Nil = (_ ** [])

817

830

818−In the ``::`` case, we need to inspect the result of a recursive call to

831+In the ``::`` case, we need to inspect the result of a recursive call

819−``filter`` to extract the length and the vector from the result. To do

832+to ``filter`` to extract the length and the vector from the result. To

820−this, we use ``with`` notation, which allows pattern matching on

833+do this, we use ``with`` notation, which allows pattern matching on

821intermediate values:

834intermediate values:

822

835

823.. code-block:: idris

836.. code-block:: idris

@@ -849,9 +862,9 @@ Intermediate values can be calculated using ``let`` bindings:

849 splitAt c x = case break (== c) x of

862 splitAt c x = case break (== c) x of

850 (x, y) => (x, strTail y)

863 (x, y) => (x, strTail y)

851

864

852−We can do simple pattern matching in ``let`` bindings too. For example,

865+We can do simple pattern matching in ``let`` bindings too. For

853−we can extract fields from a record as follows, as well as by pattern

866+example, we can extract fields from a record as follows, as well as by

854−matching at the top level:

867+pattern matching at the top level:

855

868

856.. code-block:: idris

869.. code-block:: idris

857

870

@@ -872,9 +885,9 @@ for building lists. The general form is:

872 [ expression | qualifiers ]

885 [ expression | qualifiers ]

873

886

874This generates the list of values produced by evaluating the

887This generates the list of values produced by evaluating the

875−``expression``, according to the conditions given by the comma separated

888+``expression``, according to the conditions given by the comma

876−``qualifiers``. For example, we can build a list of Pythagorean triples

889+separated ``qualifiers``. For example, we can build a list of

877−as follows:

890+Pythagorean triples as follows:

878

891

879.. code-block:: idris

892.. code-block:: idris

880

893

@@ -884,16 +897,16 @@ as follows:

884

897

885The ``[a..b]`` notation is another shorthand which builds a list of

898The ``[a..b]`` notation is another shorthand which builds a list of

886numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a

899numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a

887−list of numbers between ``a`` and ``c`` with the increment specified by

900+list of numbers between ``a`` and ``c`` with the increment specified

888−the difference between ``a`` and ``b``. This works for any numeric type,

901+by the difference between ``a`` and ``b``. This works for any numeric

889−using the ``count`` function from the prelude.

902+type, using the ``count`` function from the prelude.

890

903

891``case`` expressions

904``case`` expressions

892~~~~~~~~~~~~~~~~~~~~

905~~~~~~~~~~~~~~~~~~~~

893

906

894Another way of inspecting intermediate values of *simple* types is to

907Another way of inspecting intermediate values of *simple* types is to

895−use a ``case`` expression. The following function, for example, splits a

908+use a ``case`` expression. The following function, for example, splits

896−string into two at a given character:

909+a string into two at a given character:

897

910

898.. code-block:: idris

911.. code-block:: idris

899

912

@@ -907,10 +920,11 @@ deconstruct the pair it returns, and remove the first character of the

907second string.

920second string.

908

921

909A ``case`` expression can match several cases, for example, to inspect

922A ``case`` expression can match several cases, for example, to inspect

910−an intermediate value of type ``Maybe a``. Recall ``list_lookup`` which

923+an intermediate value of type ``Maybe a``. Recall ``list_lookup``

911−looks up an index in a list, returning ``Nothing`` if the index is out

924+which looks up an index in a list, returning ``Nothing`` if the index

912−of bounds. We can use this to write ``lookup_default``, which looks up

925+is out of bounds. We can use this to write ``lookup_default``, which

913−an index and returns a default value if the index is out of bounds:

926+looks up an index and returns a default value if the index is out of

927+bounds:

914

928

915.. code-block:: idris

929.. code-block:: idris

916

930

@@ -919,8 +933,8 @@ an index and returns a default value if the index is out of bounds:

919 Nothing => def

933 Nothing => def

920 Just x => x

934 Just x => x

921

935

922−If the index is in bounds, we get the value at that index, otherwise we

936+If the index is in bounds, we get the value at that index, otherwise

923−get a default value:

937+we get a default value:

924

938

925::

939::

926

940

@@ -929,15 +943,15 @@ get a default value:

929 *usefultypes> lookup_default 4 [3,4,5,6] (-1)

943 *usefultypes> lookup_default 4 [3,4,5,6] (-1)

930 -1 : Integer

944 -1 : Integer

931

945

932−**Restrictions:** The ``case`` construct is intended for simple analysis

946+**Restrictions:** The ``case`` construct is intended for simple

933−of intermediate expressions to avoid the need to write auxiliary

947+analysis of intermediate expressions to avoid the need to write

934−functions, and is also used internally to implement pattern matching

948+auxiliary functions, and is also used internally to implement pattern

935−``let`` and lambda bindings. It will *only* work if:

949+matching ``let`` and lambda bindings. It will *only* work if:

936

950

937- Each branch *matches* a value of the same type, and *returns* a value

951- Each branch *matches* a value of the same type, and *returns* a value

938 of the same type.

952 of the same type.

939

953

940−- The type of the result is “known”. i.e. the type of the expression

954+- The type of the result is “known”. i.e. the type of the expression

941 can be determined *without* type checking the ``case``-expression

955 can be determined *without* type checking the ``case``-expression

942 itself.

956 itself.

943

957

@@ -946,8 +960,8 @@ Dependent Records

946

960

947*Records* are data types which collect several values (the record’s

961*Records* are data types which collect several values (the record’s

948*fields*) together. ``Idris`` provides syntax for defining records and

962*fields*) together. ``Idris`` provides syntax for defining records and

949−automatically generating field access and update functions. For example,

963+*automatically generating field access and update functions. For

950−we can represent a person’s name and age in a record:

964+*example, we can represent a person’s name and age in a record:

951

965

952.. code-block:: idris

966.. code-block:: idris

953

967

@@ -958,10 +972,11 @@ we can represent a person’s name and age in a record:

958 fred : Person

972 fred : Person

959 fred = MkPerson "Fred" 30

973 fred = MkPerson "Fred" 30

960

974

961−Record declarations are like ``data`` declarations, except that they are

975+Record declarations are like ``data`` declarations, except that they

962−introduced by the ``record`` keyword, and can only have one constructor.

976+are introduced by the ``record`` keyword, and can only have one

963−The names of the binders in the constructor type (``name`` and ``age``)

977+constructor. The names of the binders in the constructor type

964−here are the field names, which we can use to access the field values:

978+(``name`` and ``age``) here are the field names, which we can use to

979+access the field values:

965

980

966::

981::

967

982

@@ -972,8 +987,8 @@ here are the field names, which we can use to access the field values:

972 *record> :t name

987 *record> :t name

973 name : Person -> String

988 name : Person -> String

974

989

975−We can also use the field names to update a record (or, more precisely,

990+We can also use the field names to update a record (or, more

976−produce a new record with the given fields updated).

991+precisely, produce a new record with the given fields updated).

977

992

978.. code-block:: bash

993.. code-block:: bash

979

994

@@ -1024,9 +1039,9 @@ syntax:

1024 record { a->b->c = val } x

1039 record { a->b->c = val } x

1025

1040

1026This returns a new record, with the field accessed by the path

1041This returns a new record, with the field accessed by the path

1027−``a->b->c`` set to ``x``. The syntax is first class, i.e.

1042+``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {

1028−``record { a->b->c = val }`` itself has a function type. Symmetrically,

1043+a->b->c = val }`` itself has a function type. Symmetrically, the field

1029−the field can also be accessed with the following syntax:

1044+can also be accessed with the following syntax:

1030

1045

1031.. code-block:: idris

1046.. code-block:: idris

1032

1047

docs/tutorial/views.rst+22−22

@@ -8,9 +8,10 @@ Dependent pattern matching

8--------------------------

10Since types can depend on values, the form of some arguments can be

11−determined by the value of others. For example, if we were to write down

11+determined by the value of others. For example, if we were to write

12−the implicit length arguments to ``(++)``, we’d see that the form of the

12+down the implicit length arguments to ``(++)``, we’d see that the form

13−length argument was determined by whether the vector was empty or not:

13+of the length argument was determined by whether the vector was empty

14+or not:

15.. code-block:: idris

16.. code-block:: idris

@@ -18,10 +19,8 @@ length argument was determined by whether the vector was empty or not:

18 (++) {n=Z} [] ys = ys

19 (++) {n=Z} [] ys = ys

19 (++) {n=S k} (x :: xs) ys = x :: xs ++ ys

20 (++) {n=S k} (x :: xs) ys = x :: xs ++ ys

21−If ``n`` was a successor in the ``[]`` case, or zero in the ``::`` case,

22+If ``n`` was a successor in the ``[]`` case, or zero in the ``::``

22−the definition would not be well typed.

23+case, the definition would not be well typed.

23−

24−

26.. _sect-nattobin:

25.. _sect-nattobin:

@@ -29,13 +28,13 @@ The ``with`` rule — matching intermediate values

29------------------------------------------------

28------------------------------------------------

31Very often, we need to match on the result of an intermediate

30Very often, we need to match on the result of an intermediate

32−computation. ``Idris`` provides a construct for this, the ``with`` rule,

31+computation. ``Idris`` provides a construct for this, the ``with``

33−inspired by views in ``Epigram`` [1]_, which takes account of

32+rule, inspired by views in ``Epigram`` [1]_, which takes account of

34the fact that matching on a value in a dependently typed language can

33the fact that matching on a value in a dependently typed language can

35affect what we know about the forms of other values. In its simplest

34affect what we know about the forms of other values. In its simplest

36form, the ``with`` rule adds another argument to the function being

35form, the ``with`` rule adds another argument to the function being

37−defined, e.g. we have already seen a vector filter function, defined as

36+defined, e.g. we have already seen a vector filter function, defined

38−follows:

37+as follows:

40.. code-block:: idris

39.. code-block:: idris

@@ -51,8 +50,8 @@ which we place after the vertical bar.

51If the intermediate computation itself has a dependent type, then the

50If the intermediate computation itself has a dependent type, then the

52result can affect the forms of other arguments — we can learn the form

51result can affect the forms of other arguments — we can learn the form

53of one value by testing another. For example, a ``Nat`` is either even

52of one value by testing another. For example, a ``Nat`` is either even

54−or odd. If it’s even it will be the sum of two equal ``Nat``\ s.

53+or odd. If it’s even it will be the sum of two equal ``Nat``.

55−Otherwise, it is the sum of two equal ``Nat``\ s plus one:

54+Otherwise, it is the sum of two equal ``Nat`` plus one:

57.. code-block:: idris

56.. code-block:: idris

@@ -69,8 +68,9 @@ accordingly.

69 parity : (n:Nat) -> Parity n

68 parity : (n:Nat) -> Parity n

71We’ll come back to the definition of ``parity`` shortly. We can use it

70We’ll come back to the definition of ``parity`` shortly. We can use it

72−to write a function which converts a natural number to a list of binary

71+to write a function which converts a natural number to a list of

73−digits (least significant first) as follows, using the ``with`` rule:

72+binary digits (least significant first) as follows, using the ``with``

73+rule:

75.. code-block:: idris

@@ -81,13 +81,13 @@ digits (least significant first) as follows, using the ``with`` rule:

81 natToBin (S (j + j)) | Odd = True :: natToBin j

83The value of the result of ``parity k`` affects the form of ``k``,

84−because the result of ``parity k`` depends on ``k``. So, as well as the

84+because the result of ``parity k`` depends on ``k``. So, as well as

85−patterns for the result of the intermediate computation (``Even`` and

85+the patterns for the result of the intermediate computation (``Even``

86−``odd``) right of the ``\mid``, we also write how the results affect the

86+and ``odd``) right of the ``\mid``, we also write how the results

87−other patterns left of the :math:`\mid`. Note that there is a function

87+affect the other patterns left of the :math:`\mid`. Note that there is

88−in the patterns (``+``) and repeated occurrences of ``j``—this is

88+a function in the patterns (``+``) and repeated occurrences of

89−allowed because another argument has determined the form of these

89+``j``—this is allowed because another argument has determined the form

90−patterns.

90+of these patterns.

92We will return to this function in Section :ref:`sect-provisional` to

93complete the definition of ``parity``.