ef50150 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Updates

+ Made paragraphs respect 80 char line width. + Fixed rogue hyperlinks. + Added missing Effects and Idris names. + Fixed errors from initial pandoc conversion. + Fixed hyperlinks.

commitef5015095bbfdcbb1b23969e6d38dba1684f6cca authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateThu 19 Mar 2015, 21:12 (12 years ago) parent4e88ac8

21 files changed+1117−1080

compare with master

unifiedsplit

docs/effects/conclusions.rst+11−10

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

55===============

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

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

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

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

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

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

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

11+paper [1]_.

1112

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

13−places:

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

14+following places:

1415

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

1617 library, supporting graphics in particular.

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

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

2627 protocol description language.

2728

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

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

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

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

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

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

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

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

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

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

3334

3435

3536

docs/effects/depeff.rst+12−10

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

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

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

8282

83−.. code-block:: idris

83+::

8484

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

8686 block in readInt:

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

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

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

129129

130−**Aside:** 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−``case`` construct, however, abstracts over the value being inspected in

133−the type of each branch.

130+.. note::

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

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

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

134+ being inspected in the type of each branch.

134135

135136File Management

136137---------------

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

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

232233error of the following form:

233234

234−.. code-block:: idris

235+::

235236

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

237238 block in testFile:

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

275276 close

276277

277278This 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:

279280

280281.. code-block:: idris

281282

282283 do pat <- val | <alternatives>

283284 p

284285

285−...is desugared to...

286+is desugared to

286287

287288.. code-block:: idris

288289

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

292293 <alternatives>

293294

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

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

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

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

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

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

297299``getArgs``:

298300

299301.. code-block:: idris

docs/effects/hangman.rst+30−27

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

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

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

233233``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

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

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

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

236236

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

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

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

248248 putStrLn !StrState

249249

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

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

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

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

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

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

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

254254

255255.. code-block:: idris

256256

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

261261

262262 wtype = proof search

263263

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

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

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

267−type inference, but very useful in practice.

264+.. note::

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

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

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

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

268269

269270

270271.. _mword:

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

300301Discussion

301302----------

302303

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

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

305−This has practical applications in more serious contexts;

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

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

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

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

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

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

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

309+*precisely-typed API*.

308310

309311In 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

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

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

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

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

315−were caught during development:

316−

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

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

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

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

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

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

317+following errors were caught during development:

318+

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

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

319321 as a starting state.

320322

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

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

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

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

325+ game.

323326

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

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

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

326329

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

328−before any testing of the game.

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

331+checker before any testing of the game.

329332

330333.. [1]

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

docs/effects/impleff.rst+53−51

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

1616State

1717-----

1818

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

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

21−operations are described as follows:

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

20+constructors describe the operations provided when the effect is

21+available. Stateful operations are described as follows:

2222

2323.. code-block:: idris

2424

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

2626 Get : { a } State a

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

2828

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

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

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

32−is run. Here, it means:

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

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

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

32+operation is run. Here, it means:

3333

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

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

36− type ``a``.

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

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

36+ of type ``a``.

3737

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

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

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

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

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

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

41+ unit type.

4142

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

4344

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

6162 = eff inst (\b => outst)

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

6364

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

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

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

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

6667

6768.. code-block:: idris

6869

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

7071 STATE t = MkEff t State

7172

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

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

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

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

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

7576

7677.. code-block:: idris

7778

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

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

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

9293

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

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

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

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

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

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

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

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

9798

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

99100 ``State``)

100101

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

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

102103

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

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

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

105106

106107There 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−result of the operation); secondly, and more importantly, the

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

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

109110continuation can be called zero or more times.

110111

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

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

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

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

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

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

114115

115116.. code-block:: idris

116117

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

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

134135 putM val = call (Put val)

135136

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

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

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

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

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

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

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

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

140141

141142.. code-block:: idris

142143

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

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

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

146147

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

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

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

150−``xs``.

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

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

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

151+effects ``xs``.

151152

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

153154new effects, however.

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

186187Console I/O

187188-----------

188189

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

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

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

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

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

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

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

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

193194

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

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

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

269270 SELECT : EFFECT

270271 SELECT = MkEff () Selection

271272

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

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

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

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

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

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

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

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

277+value.

276278

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

278280each 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.

282284File Management

283285---------------

284286

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

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

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

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

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

290−``Eff`` programs.

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

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

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

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

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

292+the equivalent ``Eff`` programs.

291293

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

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

docs/effects/introduction.rst+34−32

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

22Introduction

33============

5−Pure functional languages with dependent types such as

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1414supporting mutable state, interaction with the outside world,

1515exceptions, and verified resource management.

1616

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

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

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

3939

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

4141 input device.

4242

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

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

4545

46−- Write output

46+- Write output

4747

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

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

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

5656===========

5757

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

6061

6162.. code-block:: idris

6263

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

7071 main : IO ()

7172 main = run hello

7273

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

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

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

76−presented in the remainder of this tutorial.

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

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

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

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

7778

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

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

80−in this tutorial):

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

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

81+required for all examples in this tutorial):

8182

8283.. code-block:: sh

8384

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

8788Outline

8889=======

8990

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

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

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

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

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

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

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

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

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

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

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

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

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

103−accurately. References to further reading are given in

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

104106:ref:`sect-further`.

105107

106108.. [1]

docs/effects/simpleeff.rst+109−102

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

55==============

77So 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

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

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

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

1010

1111.. _eff-state:

1212.. code-block:: idris

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

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

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

2828which 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

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

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

32−:ref:`sect-impleff`.

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

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

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

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

3333

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

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

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

3737begin 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

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

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

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

4040examples of programs which combine multiple effects.

4141

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

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

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

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

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

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

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

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

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

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

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

5454

5555.. _eff-stdio:

5656.. code-block:: idris

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

8383 x <- getStr

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

8585

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

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

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

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

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

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

89+follows:

8990

9091.. code-block:: idris

9192

9293 main : IO ()

9394 main = run hello

9495

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

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

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

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

9798

9899.. code-block:: idris

99100

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

101102 hello = do putStr "Name? "

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

103104

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

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

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

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

107+said hello to:

106108

107109.. code-block:: idris

108110

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

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

114116 hello

115117

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

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

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

119−changed.

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

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

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

121+to be changed.

120122

121123Aside: Resource Types

122124~~~~~~~~~~~~~~~~~~~~~

123125

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

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

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

127−function at the REPL:

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

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

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

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

128130

129131.. code-block:: idris

130132

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

137139----------

138140

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

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

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

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

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

144+generally.

142145

143146.. _eff-exception:

144147.. code-block:: idris

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

180183

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

182185context 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

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

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

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

185188

186189.. code-block:: idris

187190

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

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

199202 Left NotANumber : Either Err Int

200203

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

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

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

204−integers, ``Bounded``:

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

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

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

207+bounded integers, ``Bounded``:

205208

206209.. code-block:: idris

207210

208211 Bounded : Int -> Type

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

210213

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

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

213−result of a dynamic check:

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

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

216+from the result of a dynamic check:

214217

215218.. code-block:: idris

216219

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

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

261264produce a random number:

262265

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

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

264267 and upper bounds.

265268

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

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

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

268271

269272Example

270273~~~~~~~

271274

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

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

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

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

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

275278correct:

276279

277280.. code-block:: idris

278281

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

280283

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

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

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

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

285−effectful program.

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

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

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

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

286289

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

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

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

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

292+``guess``:

289293

290294.. code-block:: idris

291295

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

322326Non-determinism

323327---------------

324328

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

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

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

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

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

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

328332succeeds.

329333

330334.. _eff-select:

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

344348Example

345349~~~~~~~

346350

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

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

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

350−values which does not satisfy the constraint:

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

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

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

354+of values which does not satisfy the constraint:

351355

352356.. code-block:: idris

353357

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

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

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

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

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

366−an exception is thrown) execution fails.

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

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

367371

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

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

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

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

372−try this as follows:

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

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

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

373377

374378.. code-block:: idris

375379

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

391395

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

393397checks 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

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

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

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

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

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

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

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

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

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

403+they are equal:

399404

400405.. code-block:: idris

401406

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

412417

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

414419

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

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

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

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

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

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

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

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

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

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

425+within range.

420426

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

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

423−are of differing lengths:

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

429+inputs are of differing lengths:

424430

425431.. code-block:: idris

426432

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

431437 (_ ** ys) <- read_vec

432438 putStrLn (show !(vadd_check xs ys))

433439

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

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

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

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

438−gracefully.

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

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

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

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

444+with gracefully.

439445

440446.. code-block:: idris

441447 :caption: Reading a vector from the console.

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

459465Example: An Expression Calculator

460466---------------------------------

461467

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

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

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

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

470+values.

464471

465472.. code-block:: idris

466473

467474 data Expr = Val Integer

468475 | Add Expr Expr

469476

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

471−are no situations in which it can fail!

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

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

472479

473480.. code-block:: idris

474481

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

476483 eval (Val x) = x

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

478485

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

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

481−variables may be undefined.

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

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

488+variables, and variables may be undefined.

482489

483490.. code-block:: idris

484491

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

488495

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

490497and 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

492499values:

493500

494501.. code-block:: idris

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

527534 eval' e = do put args

528535 eval e

529536

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

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

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

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

534−fine, for example.

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

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

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

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

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

535542

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

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

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

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

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

539546

540547.. code-block:: idris

541548

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

544551 | Add Expr Expr

545552 | Random Integer

546553

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

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

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

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

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

550557

551558.. code-block:: idris

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

563570 putStrLn (show val)

564571 return val

565572

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

567−something like the following:

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

574+error something like the following:

568575

569−.. code-block:: idris

576+::

570577

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

572579 Can't solve goal

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

580587

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

582589

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

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

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

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

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

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

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

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

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

588−types are first class in :

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

589596

590597.. code-block:: idris

591598

docs/effects/state.rst+109−109

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

55=====

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

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

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

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

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

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

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

1111

1212|image|

1313

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

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

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

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

1616

1717.. code-block:: idris

1818

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

2626 "Sheila"

2727 (Node Leaf "Bob" Leaf))

2828

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

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

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

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

3131

3232.. code-block:: idris

3333

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

3636First attempt

3737-------------

3838

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

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

41−subtree:

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

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

41+for each subtree:

4242

4343.. code-block:: idris

4444

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

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

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

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

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

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

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

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

75+explicit.

7576

7677Introducing ``Effects``

7778-----------------------

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

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

8687

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

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

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

90−type:

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

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

91+following type:

9192

9293.. code-block:: idris

9394

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

9596

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

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

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

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

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

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

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

100101

101102.. code-block:: idris

102103

103104 STATE : Type -> EFFECT

104105

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

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

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

108−follows:

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

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

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

109+implemented as follows:

109110

110111.. code-block:: idris

111112

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

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

119120

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

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

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

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

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

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

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

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

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

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

126127

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

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

128129

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

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

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

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

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

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

133134

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

135136 operation.

136137

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

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

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

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

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

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

140141

141142.. code-block:: idris

142143

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

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

145146

146147A 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−called function. In this case, it is valid for ``treeTagAux`` to call

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

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

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

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

150151``STATE Int`` effect.

151152

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

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

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

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

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

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

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

157+state:

156158

157159.. code-block:: idris

158160

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

216218Effects and Resources

217219---------------------

218220

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

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

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

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

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

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

223−for illustrative purposes):

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

225+here for illustrative purposes):

224226

225227.. code-block:: idris

226228

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

238240

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

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

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

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

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

244−the following functions:

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

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

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

246+using one of the following functions:

245247

246248.. code-block:: idris

247249

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

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

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

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

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

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

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

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

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

269271

270272.. code-block:: idris

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

272274 treeTagAux : BTree a

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

274276

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

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

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

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

279−important.

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

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

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

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

281+particularly important.

280282

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

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

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

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

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

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

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

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

285287

286288.. code-block:: idris

287289

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

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

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

291293

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

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

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

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

296−values [2]_.

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

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

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

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

298+disambiguate values [2]_.

297299

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

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

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

301−counts leaves can be written as follows:

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

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

303+also counts leaves can be written as follows:

302304

303305.. code-block:: idris

304306

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

334336

335337To summarise, we have:

336338

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

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

338340

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

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

340342 operation.

341343

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

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

343345

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

345−for the situation where available effects are not updated):

346+Or, more formally with their types (slightly simplified to account

347+only for the situation where available effects are not updated):

346348

347349.. code-block:: idris

348350

@@ -359,8 +361,8 @@ Hence, a label can be anything—a string, an integer, a type, etc.

359361

360362In many cases, using ``do``-notation can make programs unnecessarily

361363verbose, particularly in cases where the value bound is used once,

362−immediately. The following program returns the length of the ``String``

363−stored in the state, for example:

364+immediately. The following program returns the length of the

365+``String`` stored in the state, for example:

364366

365367.. code-block:: idris

366368

@@ -378,8 +380,8 @@ this. The above program can be written instead as:

378380 stateLength = pure (length !get)

379381

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

381−evaluated and then implicitly bound. Conceptually, we can think of ``!``

382−as being a prefix function with the following type:

383+evaluated and then implicitly bound. Conceptually, we can think of

384+``!`` as being a prefix function with the following type:

383385

384386.. code-block:: idris

385387

@@ -393,13 +395,13 @@ to right. In practice, ``!``-notation allows us to program in a more

393395direct style, while still giving a notational clue as to which

394396expressions are effectful.

395397

396−For example, the expression…

398+For example, the expression:

397399

398400.. code-block:: idris

399401

400402 let y = 42 in f !(g !(print y) !x)

401403

402−…is lifted to:

404+is lifted to:

403405

404406.. code-block:: idris

405407

@@ -411,10 +413,10 @@ For example, the expression…

411413Syntactic Sugar and ``Eff``

412414---------------------------

413415

414−By now, you may be wondering about the syntax we are using for ``Eff``,

415−because it doesn’t look like a normal type! (If not, you may safely skip

416−this section and return to it later.) In fact, the type of ``Eff`` is

417−the following:

416+By now, you may be wondering about the syntax we are using for

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

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

419+``Eff`` is the following:

418420

419421.. code-block:: idris

420422

@@ -425,32 +427,32 @@ This is more general than the types we have been writing so far. It is

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

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

427429

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

429−of *output* effects, computed from the result of an effectful operation.

430−That is: running an effectful program can change the set of effects

431−available! This is a particularly powerful idea, and we will see its

432−consequences in more detail later. Some examples of operations which can

433−change the set of available effects are:

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

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

432+operation. That is: running an effectful program can change the set

433+of effects available! This is a particularly powerful idea, and we

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

435+operations which can change the set of available effects are:

434436

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

437+- Updating a state containing a dependent type (for example adding an

436438 element to a vector).

437439

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

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

440− opened.

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

441+ *is* open afterwards depends on whether the file was successfully

442+ opened.

441443

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

443− possible.

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

445+ possible.

444446

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

446−Therefore, the library provides syntactic sugar which is translated such

447−that…

448+Therefore, the library provides syntactic sugar which is translated

449+such that:

448450

449451.. code-block:: idris

450452

451453 { xs } Eff a

452454

453−…is expanded to …

455+is expanded to

454456

455457.. code-block:: idris

456458

@@ -458,8 +460,8 @@ that…

458460

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

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

461−side-effecting programs. We could also have written ``treeTagAux`` with

462−the expanded type:

463+side-effecting programs. We could also have written ``treeTagAux``

464+with the expanded type:

463465

464466.. code-block:: idris

465467

@@ -472,14 +474,14 @@ Later, we will see programs which update effects:

472474

473475 { xs ==> xs' } Eff a

474476

475−…which is expanded to …

477+which is expanded to

476478

477479.. code-block:: idris

478480

479481 Eff a xs (\_ => xs')

480482

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

482−a state machine). There is, for example, a version of ``put`` which

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

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

483485updates the type of the state:

484486

485487.. code-block:: idris

@@ -492,7 +494,7 @@ Also, we have:

492494

493495 { xs ==> {res} xs' } Eff a

494496

495−…which is expanded to …

497+which is expanded to

496498

497499.. code-block:: idris

498500

@@ -501,13 +503,11 @@ Also, we have:

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

502504operation ``res``.

503505

504−.. [1]

505− The earlier paper [3]_ describes the essential implementation details,

506− although the library presented there is an earlier version which is

507− less powerful than that presented in this tutorial.

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

507+ details, although the library presented there is an earlier version

508+ which is less powerful than that presented in this tutorial.

508509

509−.. [2]

510− In practice, ``’name`` simply introduces a new empty type

510+.. [2] In practice, ``’name`` simply introduces a new empty type

511511

512512.. [3] Edwin Brady. 2013. Programming and reasoning with algebraic

513513 effects and dependent types. SIGPLAN Not. 48, 9 (September

docs/guides/type-providers-ffi.rst+56−55

@@ -1,34 +1,33 @@

11Type Providers in Idris

22=======================

4−.. sectionauthor:: David Christiansen

5−

6−`Type providers in

7−Idris <http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

4+`Type providers in Idris

5+<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

86are simple enough, but there are a few caveats to using them that it

97would 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.

1110

1211The use case

1312------------

1413

15−First, let's talk about *why* we might want type providers. There are a

16−number of reasons to use them and there are other examples available

14+First, let's talk about *why* we might want type providers. There are

15+a number of reasons to use them and there are other examples available

1716around the net, but in this tutorial we'll be using them to port C's

1817``struct stat`` to Idris.

1918

20−Why do we need type providers? Well, Idris's FFI needs to know the types

21−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

23−upon. We don't just want to hard-code these types into our program... so

24−we'll use a type provider to find them at compile time!

19+Why do we need type providers? Well, Idris's FFI needs to know the

20+types of the things it passes to and from C, but the fields of a

21+``struct stat`` are implementation-dependent types that cannot be

22+relied upon. We don't just want to hard-code these types into our

23+program... so we'll use a type provider to find them at compile time!

2524

2625A simple example

2726----------------

2827

2928First, 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

31−themselves are simple.

29+functions can be confusing but it's important to remember that

30+providers themselves are simple.

3231

3332A type provider is simply an IO action that returns a value of this

3433type:

@@ -58,11 +57,11 @@ actions. Let's write a simple one now:

5857 -- the readInt function is left as an exercise

5958

6059We 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

62−later.) Then, if their response can be converted to an integer, we

63−present ``Provide sizeTSize`` as the result of our IO action; or if it

64−can't, we signal a failure. (This will then become a compile-time

65−error.)

60+``size_t``, so we'll just ask them! (Don't worry, we'll get it

61+ourselves later.) Then, if their response can be converted to an

62+integer, we present ``Provide sizeTSize`` as the result of our IO

63+action; or if it can't, we signal a failure. (This will then become a

64+compile-time error.)

6665

6766Now we can use this IO action as a type provider:

6867

@@ -88,8 +87,8 @@ Now we can use this IO action as a type provider:

8887 putStr " bytes!"

8988

9089Yay! 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

92−hardly a step up from having them edit in the size of ``size_t``

90+good, actually. Our library is going to be difficult to compile! This

91+is hardly a step up from having them edit in the size of ``size_t``

9392themselves!

9493

9594Don't worry, there's a better way.

@@ -98,18 +97,18 @@ Foreign Functions

9897-----------------

9998

10099It's actually pretty easy to write a C function that figures out the

101−size of size\_t:

100+size of ``size_t``:

102101

103102.. code:: c

104103

105104 int sizeof_size_t() { return sizeof(size_t); }

106105

107−(Why an int and not a size\_t? The FFI needs to know how to receive the

108−return value of this function and translate it into an Idris value. If

109−we knew how to do this for values of C type size\_t, we wouldn't need to

110−write this function at all! If we really wanted to be safe from

111−overflow, we could use an array of multiple integers, but the SIZE of

112−size\_t is never going to be a 65535 byte integer.)

106+(Why an int and not a ``size_t``? The FFI needs to know how to receive

107+the return value of this function and translate it into an Idris

108+value. If we knew how to do this for values of C type ``size_t``, we

109+wouldn't need to write this function at all! If we really wanted to be

110+safe from overflow, we could use an array of multiple integers, but

111+the SIZE of ``size_t`` is never going to be a 65535 byte integer.)

113112

114113So now we can get the size of ``size_t`` as long as we're in C code.

115114We'd like to be able to use this from Idris. Can we do this? It turns

@@ -128,24 +127,24 @@ like this:

128127

129128Pretty simple. ``mkForeign`` takes a specification of what function it

130129needs 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

132−a return type.

130+``FFun`` just takes a name, a list of argument types (we have none),

131+and a return type.

133132

134133One thing you might want to note: the return type we've specified is

135134``FInt``, not ``Int``. That's because ``Int`` is an idris type and C

136135functions 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

138−"Treat the return value of this C function like it's a C int, and when

139−you pass it back into Idris, convert it to an Idris int."

136+is just the representation of the type of a C int. It tells the

137+compiler "Treat the return value of this C function like it's a C int,

138+and when you pass it back into Idris, convert it to an Idris int."

140139

141140Caveats of mkForeign

142141^^^^^^^^^^^^^^^^^^^^

143142

144143First and foremost: ``mkForeign`` is not actually a function. It is

145−treated specially by the compiler, and there are certain rules you need

146−to follow when using it.

144+treated specially by the compiler, and there are certain rules you

145+need to follow when using it.

147146

148−- Rule 1: the name string must be a literal or constant

147+- Rule 1: the name string must be a literal or constant

149148

150149This does not work:

151150

@@ -155,14 +154,15 @@ This does not work:

155154 intIntToInt name = mkForeign (FFun name [FInt, FInt] FInt)

156155

157156You'll just have to bite the bullet and write out the whole

158−``mkForeign`` and ``FFun`` expression each time. \* Rule 2: the "call"

159−to ``mkForeign`` must be fully applied

157+``mkForeign`` and ``FFun`` expression each time.

158+

159+- Rule 2: the "call" to ``mkForeign`` must be fully applied

160160

161161This just means that every argument appearing in the list of argument

162162types 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

164−to be there. For example, if we have ``strlen : String -> IO Int``, then

165−this is fine:

163+don't have to be literals or even known at compile time; they just

164+have to be there. For example, if we have ``strlen : String -> IO

165+Int``, then this is fine:

166166

167167.. code-block:: idris

168168

@@ -181,7 +181,8 @@ applied. This is okay:

181181

182182.. code-block:: idris

183183

184− lengths : IO [Int] lengths = mapM strlen listOfStrings

184+ lengths : IO [Int]

185+ lengths = mapM strlen listOfStrings

185186

186187Running foreign functions

187188~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -194,8 +195,8 @@ our code.

194195In the interpreter

195196^^^^^^^^^^^^^^^^^^

196197

197−If we want to call our foreign functions from interpreted code (such as

198−the REPL or a type provider), we need to dynamically link a library

198+If we want to call our foreign functions from interpreted code (such

199+as the REPL or a type provider), we need to dynamically link a library

199200containing the symbols we need. This is pretty easy to do with the

200201``%dynamic`` directive:

201202

@@ -204,10 +205,10 @@ containing the symbols we need. This is pretty easy to do with the

204205 %dynamic "./filename.so"

205206

206207Note that the leading "./" is important: currently, the string you

207−provide is interpreted as by dlopen(), which on Unix does not search in

208−the current directory by default. If you use the "./", the library will

209−be searched for in the directory from which you run idris (*not* the

210−location of the file you're running!). Of course, if you're using

208+provide is interpreted as by ``dlopen()``, which on Unix does not search

209+in the current directory by default. If you use the "./", the library

210+will be searched for in the directory from which you run idris (*not*

211+the location of the file you're running!). Of course, if you're using

211212functions from an installed library rather than something you wrote

212213yourself, the "./" is not necessary.

213214

@@ -222,18 +223,18 @@ instead. We'll use the ``%include`` and ``%link`` directives:

222223 %include C "filename.h"

223224 %link C "filename.o"

224225

225−Note the extra argument to the directive! We specify that we're linking

226−a C header and library. Also, unlike ``%dynamic``, these directives

227−search in the current directory by default. (That is, the directory from

228−which we run idris.)

226+Note the extra argument to the directive! We specify that we're

227+linking a C header and library. Also, unlike ``%dynamic``, these

228+directives search in the current directory by default. (That is, the

229+directory from which we run idris.)

229230

230231Putting it all together

231232-----------------------

232233

233234So, 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−the mysterious typedef'd C types into Idris types, and that's what we'll

236−do here.

235+port ``struct stat`` to Idris. The relevant part is just translating

236+all the mysterious typedef'd C types into Idris types, and that's what

237+we'll do here.

237238

238239First, let's write a C file containing functions that we'll bind to.

239240

docs/reference/documenting.rst+21−18

@@ -4,9 +4,9 @@

44Documenting Idris Code

55======================

7−Idris documentation comes in two major forms: comments, which exist for

8−a reader’s edification and are ignored by the compiler, and inline API

9−documentation, which the compiler parses and stores for future

7+Idris documentation comes in two major forms: comments, which exist

8+for a reader’s edification and are ignored by the compiler, and inline

9+API documentation, which the compiler parses and stores for future

1010reference. To consult the documentation for a declaration ``f``, write

1111``:doc f`` at the REPL or use the appropriate command in your editor

1212(``C-c C-d`` in Emacs, in Vim).

@@ -14,12 +14,12 @@ reference. To consult the documentation for a declaration ``f``, write

1414Comments

1515--------

1616

17−Use comments to explain why code is written the way that it is. Idris’s

18−comment syntax is the same as that of Haskell: lines beginning with

19−``--`` are comments, and regions bracketed by ``{-`` and ``-}`` are

20−comments even if they extend across multiple lines. These can be used to

21−comment out lines of code or provide simple documentation for the

22−readers of Idris code.

17+Use comments to explain why code is written the way that it

18+is. Idris’s comment syntax is the same as that of Haskell: lines

19+beginning with ``--`` are comments, and regions bracketed by ``{-``

20+and ``-}`` are comments even if they extend across multiple

21+lines. These can be used to comment out lines of code or provide

22+simple documentation for the readers of Idris code.

2323

2424Inline Documentation

2525--------------------

@@ -36,15 +36,16 @@ constructors, or functions can be associated with these arguments using

3636their names.

3737

3838The inline documentation for a declaration is an unbroken string of

39−lines, each of which begins with ``|||`` (three pipe symbols). The first

40−paragraph of the documentation is taken to be an overview, and in some

41−contexts, only this overview will be shown. After the documentation for

42−the declaration as a whole, it is possible to associate documetation

43−with specific named parameters, which can either be explicitly name or

44−the results of converting free variables to implicit parameters.

45−Annotations are the same as with Javadoc annotations, that is for the

46−named parameter ``(n : T)``, the corresponding annotation is

47−``||| @ n Some description`` that is placed before the declaration.

39+lines, each of which begins with ``|||`` (three pipe symbols). The

40+first paragraph of the documentation is taken to be an overview, and

41+in some contexts, only this overview will be shown. After the

42+documentation for the declaration as a whole, it is possible to

43+associate documetation with specific named parameters, which can

44+either be explicitly name or the results of converting free variables

45+to implicit parameters. Annotations are the same as with Javadoc

46+annotations, that is for the named parameter ``(n : T)``, the

47+corresponding annotation is ``||| @ n Some description`` that is

48+placed before the declaration.

4849

4950Documentation is written in Markdown, though not all contexts will

5051display all possible formatting (for example, images are not displayed

@@ -53,6 +54,8 @@ italics correctly). A comprehensive set of examples is given below.

5354

5455.. code-block:: idris

5556

57+

58+ ||| Modules can also be documented.

5659 module Docs

5760

5861 ||| Add some numbers.

docs/reference/erasure.rst+121−139

@@ -1,45 +1,17 @@

11Erasure By Usage Analysis

22=========================

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

33−proposal <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

35−out of date — and sometimes even in direct contradiction with the

4+This work stems from this `feature proposal

5+<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__

6+(obsoleted by this page). Beware that the information in the proposal

7+is out of date — and sometimes even in direct contradiction with the

368eventual implementation.

379

3810Motivation

3911----------

4012

41−Traditional dependently typed languages (Agda, Coq) are good at erasing

42−*proofs* (either via irrelevance or an extra universe).

13+Traditional dependently typed languages (Agda, Coq) are good at

14+erasing *proofs* (either via irrelevance or an extra universe).

4315

4416.. code-block:: idris

4517

@@ -47,16 +19,16 @@ Traditional dependently typed languages (Agda, Coq) are good at erasing

4719 half Z EZ = Z

4820 half (S (S n)) (ES pf) = S (half n pf)

4921

50−For example, in the above snippet, the second argument is a proof, which

51−is used only to convince the compiler that the function is total. This

52−proof is never inspected at runtime and thus can be erased. In this

53−case, the mere existence of the proof is sufficient and we can use

54−irrelevance-related methods to achieve erasure.

22+For example, in the above snippet, the second argument is a proof,

23+which is used only to convince the compiler that the function is

24+total. This proof is never inspected at runtime and thus can be

25+erased. In this case, the mere existence of the proof is sufficient

26+and we can use irrelevance-related methods to achieve erasure.

5527

5628However, sometimes we want to erase *indices* and this is where the

5729traditional approaches stop being useful, mainly for reasons described

58−in the `original

59−proposal <https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.

30+in the `original proposal

31+<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.

6032

6133.. code-block:: idris

6234

@@ -66,11 +38,11 @@ proposal <https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annot

6638 | (xs, ys) = (x :: xs, y :: ys)

6739

6840Notice 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

70−program is generally the same as in the previous case.

41+we would like to get rid of the ``n`` instead, although the shape of

42+the program is generally the same as in the previous case.

7143

72−There are methods described by Brady, McBride and McKinna in [BMM04] to

73−remove the indices from data structures, exploiting the fact that

44+There are methods described by Brady, McBride and McKinna in [BMM04]_

45+to remove the indices from data structures, exploiting the fact that

7446functions operating on them either already have a copy of the

7547appropriate index or the index can be quickly reconstructed if needed.

7648However, we often want to erase the indices altogether, from the whole

@@ -82,7 +54,7 @@ the runtime performance asymptotically.

8254Binary numbers

8355~~~~~~~~~~~~~~

8456

85−- O(n) instead of O(log n)

57+- O(n) instead of O(log n)

8658

8759Consider the following ``Nat``-indexed type family representing binary

8860numbers:

@@ -99,10 +71,10 @@ memory-efficient because their size is logarithmic compared to the

9971numbers they represent.

10072

10173Unfortunately this is not the case. The problem is that these binary

102−numbers still carry the *unary* indices with them, performing arithmetic

103−on the indices whenever arithmetic is done on the binary numbers

104−themselves. Hence the real representation of the number 15 looks like

105−this:

74+numbers still carry the *unary* indices with them, performing

75+arithmetic on the indices whenever arithmetic is done on the binary

76+numbers themselves. Hence the real representation of the number 15

77+looks like this:

10678

10779::

10880

@@ -119,13 +91,16 @@ this:

11991The used memory is actually *linear*, not logarithmic and therefore we

12092cannot get below O(n) with time complexities.

12193

122−One could argue that Idris in fact compiles ``Nat``\ s via GMP but

123−that's a moot point for two reasons: \* First, whenever we try to index

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.

94+One could argue that Idris in fact compiles ``Nat`` via GMP but

95+that's a moot point for two reasons:

12796

128−This ought not to be the case since the ``Nat``\ s are never used at

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+

103+This ought not to be the case since the ``Nat`` are never used at

129104runtime and they are only there for typechecking purposes. Hence we

130105should get rid of them and get runtime code similar to what a idris

131106programmer would write.

@@ -155,22 +130,22 @@ For better intuition, the shape of the U-view of

155130 z (one)

156131

157132When 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]``.

159−No matter whether these lists are stored or built on demand, they take

160−up a quadratic amount of memory (because they cannot share nodes), and

161−hence it takes a quadratic amount of time just to build values of this

162−index alone.

133+``[x0,x1,x2,z,y2,y1,y0]``, ``[x1,x2,z,y2,y1]``, ``[x2,z,y2]``,

134+``[z]``. No matter whether these lists are stored or built on demand,

135+they take up a quadratic amount of memory (because they cannot share

136+nodes), and hence it takes a quadratic amount of time just to build

137+values of this index alone.

163138

164139But 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

166−this goal.

140+linear time — so we need to erase the index ``xs`` if we want to

141+achieve this goal.

167142

168143Changes to Idris

169144----------------

170145

171−Usage analysis is run at every compilation and its outputs are used for

172−various purposes. This is actually invisible to the user but it's a

173−relatively big and important change, which enables the new features.

146+Usage analysis is run at every compilation and its outputs are used

147+for various purposes. This is actually invisible to the user but it's

148+a relatively big and important change, which enables the new features.

174149

175150Everything that is found to be unused is erased. No annotations are

176151needed, 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

178153warning if the thing is accidentally used.

179154

180155"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

182−found to be irrelevant to the run-time behaviour by the usage analysis

183−algorithm.)

156+influence run-time behaviour of the program. (More precisely, it is

157+not found to be irrelevant to the run-time behaviour by the usage

158+analysis algorithm.)

159+

160+"Things" considered for removal by erasure include:

161+

162+* function arguments

184163

185−"Things" considered for removal by erasure include: \* function

186−arguments \* data constructor fields (including record fields and

187−dictionary fields of class instances)

164+* data constructor fields (including record fields and dictionary

165+ fields of class instances)

188166

189167For example, ``Either`` often compiles to the same runtime

190−representation as ``Bool``. Constructor field removal sometimes combines

191−with the newtype optimisation to have quite a strong effect.

168+representation as ``Bool``. Constructor field removal sometimes

169+combines with the newtype optimisation to have quite a strong effect.

192170

193171There is a new compiler option ``--warnreach``, which will enable

194−warnings coming from erasure. Since we have full usage analysis, we can

195−compile even those programs that violate erasure annotations -- it's

196−just that the binaries may run slower than expected. The warnings will

197−be enabled by default in future versions of Idris (and possibly turned

198−to errors). However, in this transitional period, we chose to keep them

199−on-demand to avoid confusion until better documentation is written.

172+warnings coming from erasure. Since we have full usage analysis, we

173+can compile even those programs that violate erasure annotations --

174+it's just that the binaries may run slower than expected. The warnings

175+will be enabled by default in future versions of Idris (and possibly

176+turned to errors). However, in this transitional period, we chose to

177+keep them on-demand to avoid confusion until better documentation is

178+written.

200179

201180Case-tree elaboration tries to avoid using dotted "things" whenever

202181possible. (NB. This is not yet perfect and it's being worked on:

@@ -218,8 +197,8 @@ runtime.

218197 O : .{n : Nat} -> Bin n -> Bin (0 + 2*n)

219198 I : .{n : Nat} -> Bin n -> Bin (1 + 2*n)

220199

221−If these fields are found to be used at runtime, the dots will trigger a

222−warning (with ``--warnreach``).

200+If these fields are found to be used at runtime, the dots will trigger

201+a warning (with ``--warnreach``).

223202

224203Note that free (unbound) implicits are dotted by default so, for

225204example, the constructor ``O`` can be defined as:

@@ -244,29 +223,31 @@ and free implicits are automatically dotted here, too.

244223What it means

245224-------------

246225

247−Dot annotations serve two purposes: \* influence case-tree elaboration

248−to avoid dotted variables \* trigger warnings when a dotted variable is

249−used

226+Dot annotations serve two purposes:

227+

228+* influence case-tree elaboration to avoid dotted variables

229+

230+* trigger warnings when a dotted variable is used

250231

251232However, there's no direct connection between being dotted and being

252233erased. The compiler erases everything it can, dotted or not. The dots

253−are there mainly to help the programmer (and the compiler) refrain from

254−using the values they want to erase.

234+are there mainly to help the programmer (and the compiler) refrain

235+from using the values they want to erase.

255236

256237How to use it

257238-------------

258239

259−Ideally, few or no extra annotations are needed -- in practice, it turns

260−out that having free implicits automatically dotted is enough to get

261−good erasure.

240+Ideally, few or no extra annotations are needed -- in practice, it

241+turns out that having free implicits automatically dotted is enough to

242+get good erasure.

262243

263−Therefore, just compile with ``--warnreach`` to see warnings if erasure

264−cannot remove parts of the program.

244+Therefore, just compile with ``--warnreach`` to see warnings if

245+erasure cannot remove parts of the program.

265246

266−However, those programs that have been written without runtime behaviour

267−in mind, will need some help to get in the form that compiles to a

268−reasonable binary. Generally, it's sufficient to follow erasure warnings

269−(which may be sometimes unhelpful at the moment).

247+However, those programs that have been written without runtime

248+behaviour in mind, will need some help to get in the form that

249+compiles to a reasonable binary. Generally, it's sufficient to follow

250+erasure warnings (which may be sometimes unhelpful at the moment).

270251

271252Benchmarks

272253----------

@@ -289,49 +270,50 @@ their names.

289270

290271There is no decent documentation yet. This wiki page is the first one.

291272

292−There is no generally accepted terminology. We switch between "dotted",

293−"unused", "erased", "irrelevant", "inaccessible", while each has a

294−slightly different meaning. We need more consistent and understandable

295−naming.

296−

297−If the same type is used in both erased and non-erased context, it will

298−retain its fields to accomodate the least common denominator -- the

299−non-erased context. This is particularly troublesome in the case of the

300−type of (dependent) pairs, where it actually means that no erasure would

301−be performed. We should probably locate disjoint uses of data types and

302−split them into "sub-types". There are three different flavours of

303−dependent types now: ``Sigma`` (nothing erased), ``Exists`` (first

304−component erased), ``Subset`` (second component erased).

273+There is no generally accepted terminology. We switch between

274+"dotted", "unused", "erased", "irrelevant", "inaccessible", while each

275+has a slightly different meaning. We need more consistent and

276+understandable naming.

277+

278+If the same type is used in both erased and non-erased context, it

279+will retain its fields to accomodate the least common denominator --

280+the non-erased context. This is particularly troublesome in the case

281+of the type of (dependent) pairs, where it actually means that no

282+erasure would be performed. We should probably locate disjoint uses of

283+data types and split them into "sub-types". There are three different

284+flavours of dependent types now: ``Sigma`` (nothing erased),

285+``Exists`` (first component erased), ``Subset`` (second component

286+erased).

305287

306288Case-tree building does not avoid dotted values coming from

307289pattern-matched constructors (https://gist.github.com/ziman/10458331).

308290This is to be fixed soon. (Fixed.)

309291

310292Higher-order function arguments and opaque functional variables are

311−considered to be using all their arguments. To work around this, you can

312−force erasure via the type system, using the ``Erased`` wrapper:

293+considered to be using all their arguments. To work around this, you

294+can force erasure via the type system, using the ``Erased`` wrapper:

313295https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr

314296

315297Typeclass methods are considered to be using the union of all their

316−implementations. In other words, an argument of a method is unused only

317−if it is unused in every implementation of the method that occurs in the

318−program.

298+implementations. In other words, an argument of a method is unused

299+only if it is unused in every implementation of the method that occurs

300+in the program.

319301

320302Planned features

321303----------------

322304

323−- Fixes to the above shortcomings in general.

305+- Fixes to the above shortcomings in general.

324306

325−- Improvements to the case-tree elaborator so that it properly avoids

307+- Improvements to the case-tree elaborator so that it properly avoids

326308 dotted fields of data constructors. Done.

327309

328−- Compiler pragma ``%default_usage used/unused`` and per-function

329− overrides ``used`` and ``unused``, which allow the programmer to mark

330− the return value of a function as used, even if the function is not

331− used in ``main`` (which is the case when writing library code). These

332− annotations will help library writers discover usage violations in

333− their code before it is actually published and used in compiled

334− programs.

310+- Compiler pragma ``%default_usage used/unused`` and per-function

311+ overrides ``used`` and ``unused``, which allow the programmer to

312+ mark the return value of a function as used, even if the function

313+ is not used in ``main`` (which is the case when writing library

314+ code). These annotations will help library writers discover usage

315+ violations in their code before it is actually published and used

316+ in compiled programs.

335317

336318Troubleshooting

337319---------------

@@ -366,15 +348,15 @@ There should be no warnings in this function

366348A possible cause is non-totality of the function (more precisely,

367349non-coverage). If a function is non-covering, the program needs to

368350inspect all arguments in order to detect coverage failures at runtime.

369−Since the function inspects all its arguments, nothing can be erased and

370−this may transitively cause usage violations. The solution is to make

371−the function total or accept the fact that it will use its arguments and

372−remove some dots from the appropriate constructor fields and function

373−arguments. (Please note that this is not a shortcoming of erasure and

374−there is nothing we can do about it.)

375−

376−Another possible cause is the currently imperfect case-tree elaboration,

377−which does not avoid dotted constructor fields (see

351+Since the function inspects all its arguments, nothing can be erased

352+and this may transitively cause usage violations. The solution is to

353+make the function total or accept the fact that it will use its

354+arguments and remove some dots from the appropriate constructor fields

355+and function arguments. (Please note that this is not a shortcoming of

356+erasure and there is nothing we can do about it.)

357+

358+Another possible cause is the currently imperfect case-tree

359+elaboration, which does not avoid dotted constructor fields (see

378360https://gist.github.com/ziman/10458331). You can either rephrase the

379361function or wait until this is fixed, hopefully soon. Fixed.

380362

@@ -496,15 +478,15 @@ We can see that the argument ``n`` of both ``I`` and ``O`` is used in

496478the function ``toN``, argument 1.

497479

498480At this stage of development, warnings only contain argument numbers,

499−not names; this will hopefully be fixed. When numbering arguments, we go

500−from 0, taking free implicits first, left-to-right; then the bound

481+not names; this will hopefully be fixed. When numbering arguments, we

482+go from 0, taking free implicits first, left-to-right; then the bound

501483arguments. The function ``toN`` has therefore in fact two arguments:

502484``n`` (argument 0) and ``b`` (argument 1). And indeed, as the warning

503485says, we project the dotted field from ``b``.

504486

505487Again, 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

507−every constructor of ``Bin`` and make it a bound implicit:

488+result honestly; the other one is to accept that we carry a ``Nat``

489+with every constructor of ``Bin`` and make it a bound implicit:

508490

509491.. code-block:: idris

510492

@@ -514,6 +496,6 @@ every constructor of ``Bin`` and make it a bound implicit:

514496References

515497----------

516498

517−[BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive families

518−need not store their

519−indices <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__

499+.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

500+ families need not store their indices

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

44.. sectionauthor:: Edwin Brady

6−Ever since Idris has had multiple backends compiling to different target

7−languages on potentially different platforms, we have had the problem

8−that the foreign function interface (FFI) was written under the

9−assumption of compiling to C. As a result, it has been hard to write

10−generic code for multiple targets, or even to be sure that if code

11−compiles that it will run on the expected target.

6+Ever since Idris has had multiple backends compiling to different

7+target languages on potentially different platforms, we have had the

8+problem that the foreign function interface (FFI) was written under

9+the assumption of compiling to C. As a result, it has been hard to

10+write generic code for multiple targets, or even to be sure that if

11+code compiles that it will run on the expected target.

1212

1313As of 0.9.17, Idris will have a new foreign function interface (FFI)

1414which is aware of multiple targets. Users who are working with the

1515default code generator can happily continue writing programs as before

1616with 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

18−some things you will need to be aware of, which this page describes.

17+library, writing a back end, or working with a non-C back end, there

18+are some things you will need to be aware of, which this page

19+describes.

1920

2021The ``IO'`` monad, and ``main``

2122-------------------------------

2223

23−The ``IO`` monad exists as before, but is now specific to the C backend

24−(or, more precisely, any backend whose foreign function calls are

25−compatible with C.) Additionally, there is now an ``IO'`` monad, which

26−is parameterised over a FFI descriptor:

24+The ``IO`` monad exists as before, but is now specific to the C

25+backend (or, more precisely, any backend whose foreign function calls

26+are compatible with C.) Additionally, there is now an ``IO'`` monad,

27+which is parameterised over a FFI descriptor:

2728

2829.. code-block:: idris

2930

3031 data IO' : (lang : FFI) -> Type -> Type

3132

3233The Prelude defines two FFI descriptors which are imported

33−automatically, for C and JavaScript/Node, and defines ``IO`` to use the

34−C FFI and ``JS_IO`` to use the JavaScript FFI:

34+automatically, for C and JavaScript/Node, and defines ``IO`` to use

35+the C FFI and ``JS_IO`` to use the JavaScript FFI:

3536

3637.. code-block:: idris

3738

@@ -44,26 +45,27 @@ C FFI and ``JS_IO`` to use the JavaScript FFI:

4445 JS_IO : Type -> Type

4546 JS_IO a = IO' FFI_JS a

4647

47−As before, the entry point to an Idris program is ``main``, but the type

48−of ``main`` can now be any instance of ``IO'``, e.g. the following are

49−both valid:

48+As before, the entry point to an Idris program is ``main``, but the

49+type of ``main`` can now be any instance of ``IO'``, e.g. the

50+following are both valid:

5051

5152.. code-block:: idris

5253

5354 main : IO ()

5455 main : JS_IO ()

5556

56−The FFI descriptor includes details about which types can be marshalled

57−between the foreign language and Idris, and the "target" of a foreign

58−function call (typically just a String representation of the function's

59−name, but potentially something more complicated such as an external

60−library file or even a URL).

57+The FFI descriptor includes details about which types can be

58+marshalled between the foreign language and Idris, and the "target" of

59+a foreign function call (typically just a String representation of the

60+function's name, but potentially something more complicated such as an

61+external library file or even a URL).

6162

6263FFI descriptors

6364---------------

6465

65−An FFI descriptor is a record containing a predicate which holds when a

66−type can be marshalled, and the type of the target of a foreign call:

66+An FFI descriptor is a record containing a predicate which holds when

67+a type can be marshalled, and the type of the target of a foreign

68+call:

6769

6870.. code-block:: idris

6971

@@ -112,12 +114,12 @@ type is given by the ``ffi_fn`` field of ``FFI_C`` here), and a function

112114type, which gives the expected types of the remaining arguments. Here,

113115we're calling an external function ``fileOpen`` which takes, in the C, a

114116``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*``

116118and vice versa.

117119

118120The 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

120−to be valid.

121+``fn_types`` predicate of the ``FFI_C`` description for the foreign

122+call to be valid.

121123

122124**Note** The arguments to ``foreign`` *must* be known at compile time,

123125because the foreign calls are generated statically. The ``%inline``

@@ -136,14 +138,18 @@ FFI implementation

136138

137139In order to write bindings to external libraries, the details of how

138140``foreign`` works are unnecessary --- you simply need to know that

139−``foreign`` takes an FFI descriptor, the function name, and its type. It

140−is instructive to look a little deeper, however:

141+``foreign`` takes an FFI descriptor, the function name, and its

142+type. It is instructive to look a little deeper, however:

141143

142144The type of ``foreign`` is as follows:

143145

144146.. code-block:: idris

145147

146− foreign : (ffi : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy ffi [] ty} -> ty

148+ foreign : (ffi : FFI)

149+ -> (fname : ffi_fn f)

150+ -> (ty : Type)

151+ -> {auto fty : FTy ffi [] ty}

152+ -> ty

147153

148154The important argument here is the implicit ``fty``, which contains a

149155proof (``FTy``) that the given type is valid according to the FFI

@@ -155,10 +161,11 @@ description ``ffi``:

155161 FRet : ffi_types f t -> FTy f xs (IO' f t)

156162 FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)

157163

158−Notice that this uses the ``ffi_types`` field of the FFI descriptor ---

159−these arguments to ``FRet`` and ``FFun`` give explicit proofs that the

160−type is valid in this FFI. For example, the above ``do_fopen`` builds

161−the following implicit proof as the ``fty`` argument to ``foreign``:

164+Notice that this uses the ``ffi_types`` field of the FFI descriptor

165+--- these arguments to ``FRet`` and ``FFun`` give explicit proofs that

166+the type is valid in this FFI. For example, the above ``do_fopen``

167+builds the following implicit proof as the ``fty`` argument to

168+``foreign``:

162169

163170.. code-block:: idris

164171

@@ -169,13 +176,13 @@ Compiling foreign calls

169176

170177(This section assumes some knowledge of the Idris internals.)

171178

172−When writing a back end, we now need to know how to compile ``foreign``.

173−We'll skip the details here of how a ``foreign`` call reaches the

174−intermediate representation (the IR), though you can look in ``IO.idr``

175−in the ``prelude`` package to see a bit more detail --- a ``foreign``

176−call is implemented by the primitive function ``mkForeignPrim``. The

177−important part of the IR as defined in ``Lang.hs`` is the following

178−constructor:

179+When writing a back end, we now need to know how to compile

180+``foreign``. We'll skip the details here of how a ``foreign`` call

181+reaches the intermediate representation (the IR), though you can look

182+in ``IO.idr`` in the ``prelude`` package to see a bit more detail ---

183+a ``foreign`` call is implemented by the primitive function

184+``mkForeignPrim``. The important part of the IR as defined in

185+``Lang.hs`` is the following constructor:

179186

180187.. code-block:: idris

181188

@@ -186,9 +193,9 @@ constructor:

186193

187194So, a ``foreign`` call appears in the IR as the ``LForeign``

188195constructor, which takes a function descriptor (of a type given by the

189−``ffi_fn`` field in the FFI descriptor), a return type descriptor (given

190−by an application of ``FTy``), and a list of arguments with type

191−descriptors (also given by an application of ``FTy``).

196+``ffi_fn`` field in the FFI descriptor), a return type descriptor

197+(given by an application of ``FTy``), and a list of arguments with

198+type descriptors (also given by an application of ``FTy``).

192199

193200An ``FDesc`` describes an application of a name to some arguments, and

194201is really just a simplified subset of an ``LExp``:

@@ -210,9 +217,9 @@ Our ``do_fopen`` example above arrives in the ``LExp`` form as:

210217 LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))

211218 [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]

212219

213−(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations of

214−the arguments.) This information should be enough for any back end to

215−marshal the arguments and return value appropriately.

220+(Assuming that ``f`` and ``m`` stand for the ``LExp`` representations

221+of the arguments.) This information should be enough for any back end

222+to marshal the arguments and return value appropriately.

216223

217224.. note::

218225

@@ -228,7 +235,8 @@ JavaScript FFI descriptor

228235~~~~~~~~~~~~~~~~~~~~~~~~~

229236

230237The 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:

232240

233241.. code-block:: idris

234242

@@ -255,9 +263,9 @@ JavaScript FFI supports marshalling functions. It is defined as follows:

255263The reason for wrapping function types in a ``JsFn`` is to help the

256264proof search when building ``FTy``. We hope to improve proof search

257265eventually, but for the moment it works much more reliably if the

258−indices are disjoint! An example of using this appears in

259−`IdrisScript <https://github.com/idris-hackers/IdrisScript>`__ when

260−setting timeouts:

266+indices are disjoint! An example of using this appears in `IdrisScript

267+<https://github.com/idris-hackers/IdrisScript>`__ when setting

268+timeouts:

261269

262270.. code-block:: idris

263271

docs/reference/uniqueness-types.rst+49−51

@@ -1,8 +1,6 @@

11Uniqueness Types

22================

4−.. sectionauthor:: Edwin Brady

5−

64Uniqueness Types are an experimental feature available from Idris

750.9.15. A value with a unique type is guaranteed to have *at most one*

86reference 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,

1210device drivers, and any other system with hard real-time requirements,

1311ideally while giving up as little high level conveniences as possible.

1412

15−They are inspired by linear types, `Uniqueness

16−Types <https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the

17−`Clean <http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

18−ownership types and borrowed pointers in the

19−`Rust <http://www.rust-lang.org/>`__ programming language.

13+They are inspired by linear types, `Uniqueness Types

14+<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean

15+<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

16+ownership types and borrowed pointers in the `Rust

17+<http://www.rust-lang.org/>`__ programming language.

2018

2119Some things we hope to be able to do eventually with uniqueness types

2220include:

@@ -39,11 +37,11 @@ declare the type of unique lists as follows:

3937 Nil : UList a

4038 (::) : a -> UList a -> UList a

4139

42−If we have a value ``xs : UList a``, then there is at most one reference

43−to ``xs`` at run-time. The type checker preserves this guarantee by

44−ensuring that there is at most one reference to any value of a unique

45−type in a pattern clause. For example, the following function definition

46−would be valid:

40+If we have a value ``xs : UList a``, then there is at most one

41+reference to ``xs`` at run-time. The type checker preserves this

42+guarantee by ensuring that there is at most one reference to any value

43+of a unique type in a pattern clause. For example, the following

44+function definition would be valid:

4745

4846.. code-block:: idris

4947

@@ -55,8 +53,8 @@ In the second clause, ``xs`` is a value of a unique type, and only

5553appears once on the right hand side, so this clause is valid. Not only

5654that, since we know there can be no other reference to the ``UList a``

5755argument, 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

59−the list.

56+is aware of this, and compiles this definition to an in-place update

57+of the list.

6058

6159The following function definition would not be valid (even assuming an

6260implementation of ``++``), however, since ``xs`` appears twice:

@@ -84,14 +82,14 @@ If we explicitly copy, however, the typechecker is happy:

8482Note that it's fine to use ``x`` twice, because ``a`` is a ``Type``,

8583rather than a ``UniqueType``.

8684

87−There are some other restrictions on where a ``UniqueType`` can appear,

88−so that the uniqueness property is preserved. In particular, the type of

89−the function type, ``(x : a) -> b`` depends on the type of ``a`` or

90−``b`` - if either is a ``UniqueType``, then the function type is also a

91−``UniqueType``. Then, in a data declaration, if the type constructor

92−builds a ``Type``, then no constructor can have a ``UniqueType``. For

93−example, the following definition is invalid, since it would embed a

94−unique value in a possible non-unique value:

85+There are some other restrictions on where a ``UniqueType`` can

86+appear, so that the uniqueness property is preserved. In particular,

87+the type of the function type, ``(x : a) -> b`` depends on the type of

88+``a`` or ``b`` - if either is a ``UniqueType``, then the function type

89+is also a ``UniqueType``. Then, in a data declaration, if the type

90+constructor builds a ``Type``, then no constructor can have a

91+``UniqueType``. For example, the following definition is invalid,

92+since it would embed a unique value in a possible non-unique value:

9593

9694.. code-block:: idris

9795

@@ -127,15 +125,15 @@ composition as follows:

127125

128126The ``Type*`` type stands for either unique or non-unique types. Since

129127such a function may be passed a ``UniqueType``, any value of type

130−``Type*`` must also satisfy the requirement that it appears at most once

131−on the right hand side.

128+``Type*`` must also satisfy the requirement that it appears at most

129+once on the right hand side.

132130

133131Borrowed Types

134132~~~~~~~~~~~~~~

135133

136134It quickly becomes obvious when working with uniqueness types that

137−having only one reference at a time can be painful. For example, what if

138−we want to display a list before updating it?

135+having only one reference at a time can be painful. For example, what

136+if we want to display a list before updating it?

139137

140138.. code-block:: idris

141139

@@ -158,8 +156,8 @@ the list! So the following function would be invalid:

158156

159157Still, one would hope to be able to display a unique list without

160158problem, 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

162−Unique type which can be inspected at the top level (by pattern

159+can achieve this, using the notion of *borrowing*. A Borrowed type is

160+a Unique type which can be inspected at the top level (by pattern

163161matching, or by *lending* to another function) but no further. This

164162ensures that the internals (i.e. the arguments to top level patterns)

165163will not be passed to any function which will update them.

@@ -191,21 +189,21 @@ this, we can write ``showU`` as follows:

191189 showU' [x] = show x

192190 showU' (Read (x :: xs)) = show x ++ ", " ++ showU' (lend xs)

193191

194−Unlike a unique value, a borrowed value may be referred to as many times

195−as desired. However, there is a restriction on how a borrowed value can

196−be used. After all, much like a library book or your neighbour's

197−lawnmower, if a function borrows a value it is expected to return it in

198−exactly the condition in which it was received!

192+Unlike a unique value, a borrowed value may be referred to as many

193+times as desired. However, there is a restriction on how a borrowed

194+value can be used. After all, much like a library book or your

195+neighbour's lawnmower, if a function borrows a value it is expected to

196+return it in exactly the condition in which it was received!

199197

200−The restriction is that when a ``Borrowed`` type is matched, any pattern

201−variables under the ``Read`` which have a unique type may not be

202−referred to at all on the right hand side (unless they are themselves

203−``lent`` to another function).

198+The restriction is that when a ``Borrowed`` type is matched, any

199+pattern variables under the ``Read`` which have a unique type may not

200+be referred to at all on the right hand side (unless they are

201+themselves ``lent`` to another function).

204202

205203Uniqueness information is stored in the type, and in particular in

206204function 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

208−following sort of bad program being implemented:

205+is constructed will be required to have unique type, which prevents

206+the following sort of bad program being implemented:

209207

210208.. code-block:: idris

211209

@@ -234,20 +232,20 @@ Problems/Disadvantages/Still to do...

234232This is a work in progress, there is lots to do. The most obvious

235233problem is the loss of abstraction. On the one hand, we have more

236234precise control over memory usage with ``UniqueType`` and

237−``BorrowedType``, but they are not in general compatible with functions

238−polymorphic over ``Type``. In the short term, we can start to write

239−reactive and low memory systems with this, but longer term it would be

240−nice to support more abstraction.

235+``BorrowedType``, but they are not in general compatible with

236+functions polymorphic over ``Type``. In the short term, we can start

237+to write reactive and low memory systems with this, but longer term it

238+would be nice to support more abstraction.

241239

242240We also haven't checked any of the metatheory, so this could all be

243241fatally flawed! The implementation is based to a large extent on

244−`Uniqueness Typing

245−Simplified <http://lambda-the-ultimate.org/node/2708>`__, by de Vries et

246−al, so there is reason to believe things should be fine, but we still

247−have to do the work.

242+`Uniqueness Typing Simplified

243+<http://lambda-the-ultimate.org/node/2708>`__, by de Vries et al, so

244+there is reason to believe things should be fine, but we still have to

245+do the work.

248246

249247Much as there are with linear types, there are some annoyances when

250−trying to prove properties of functions with unique types (for example,

251−what counts as a use of a value). Since we require *at most* one use of

252−a value, rather than *exactly* one, this seems to be less of an issue in

253−practice, but still needs thought.

248+trying to prove properties of functions with unique types (for

249+example, what counts as a use of a value). Since we require *at most*

250+one use of a value, rather than *exactly* one, this seems to be less

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.

1313To achieve this, we use a feature which has proved to be effective in

1414Haskell, namely *type classes*. To define a type class, we provide a

1515collection of overloaded operations which describe the interface for

16−*instances* of that class. A simple example is the ``Show`` type class,

17−which is defined in the prelude and provides an interface for converting

18−values to ``String``:

16+*instances* of that class. A simple example is the ``Show`` type

17+class, which is defined in the prelude and provides an interface for

18+converting values to ``String``:

1919

2020.. code-block:: idris

2121

@@ -29,9 +29,9 @@ This generates a function of the following type (which we call a

2929

3030 show : Show a => a -> String

3131

32−We can read this as: “under the constraint that ``a`` is an instance of

33−``Show``, take an input ``a`` and return a ``String``.” An instance of a

34−class is defined with an ``instance`` declaration, which provides

32+We can read this as: “under the constraint that ``a`` is an instance

33+of ``Show``, take an input ``a`` and return a ``String``.” An instance

34+of a class is defined with an ``instance`` declaration, which provides

3535implementations of the function for a specific type. For example, the

3636``Show`` instance for ``Nat`` could be defined as:

3737

@@ -41,7 +41,7 @@ implementations of the function for a specific type. For example, the

4141 show Z = "Z"

4242 show (S k) = "s" ++ show k

4343

44−.. code-block:: idris

44+::

4545

4646 Idris> show (S (S (S Z)))

4747 "sssZ" : String

@@ -77,8 +77,8 @@ the built-in types:

7777 (==) : a -> a -> Bool

7878 (/=) : a -> a -> Bool

7979

80−To declare an instance of a type, we have to give definitions of all of

81−the methods. For example, for an instance of ``Eq`` for ``Nat``:

80+To declare an instance of a type, we have to give definitions of all

81+of the methods. For example, for an instance of ``Eq`` for ``Nat``:

8282

8383.. code-block:: idris

8484

@@ -92,8 +92,8 @@ the methods. For example, for an instance of ``Eq`` for ``Nat``:

9292

9393It is hard to imagine many cases where the ``/=`` method will be

9494anything other than the negation of the result of applying the ``==``

95−method. It is therefore convenient to give a default definition for each

96−method in the class declaration, in terms of the other method:

95+method. It is therefore convenient to give a default definition for

96+each method in the class declaration, in terms of the other method:

9797

9898.. code-block:: idris

9999

@@ -113,9 +113,9 @@ Extending Classes

113113-----------------

114114

115115Classes can also be extended. A logical next step from an equality

116−relation ``Eq`` is to define an ordering relation ``Ord``. We can define

117−an ``Ord`` class which inherits methods from ``Eq`` as well as defining

118−some of its own:

116+relation ``Eq`` is to define an ordering relation ``Ord``. We can

117+define an ``Ord`` class which inherits methods from ``Eq`` as well as

118+defining some of its own:

119119

120120.. code-block:: idris

121121

@@ -136,18 +136,18 @@ some of its own:

136136The ``Ord`` class allows us to compare two values and determine their

137137ordering. Only the ``compare`` method is required; every other method

138138has a default definition. Using this we can write functions such as

139−``sort``, a function which sorts a list into increasing order, provided

140−that the element type of the list is in the ``Ord`` class. We give the

141−constraints on the type variables left of the fat arrow ``=>``, and the

142−function type to the right of the fat arrow:

139+``sort``, a function which sorts a list into increasing order,

140+provided that the element type of the list is in the ``Ord`` class. We

141+give the constraints on the type variables left of the fat arrow

142+``=>``, and the function type to the right of the fat arrow:

143143

144144.. code-block:: idris

145145

146146 sort : Ord a => List a -> List a

147147

148−Functions, classes and instances can have multiple constraints. Multiple

149−constaints are written in brackets in a comma separated list, for

150−example:

148+Functions, classes and instances can have multiple

149+constraints. Multiple constaints are written in brackets in a comma

150+separated list, for example:

151151

152152.. code-block:: idris

153153

@@ -159,8 +159,8 @@ Functors and Applicatives

159159

160160So far, we have seen single parameter type classes, where the parameter

161161is 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

163−the parameter is not ``Type``, we need to give an explicit type

162+0) of parameters, and the parameters can have *any* type. If the type

163+of the parameter is not ``Type``, we need to give an explicit type

164164declaration. For example, the ``Functor`` class is defined in the

165165library:

166166

@@ -198,7 +198,7 @@ Monads and ``do``-notation

198198--------------------------

199199

200200The ``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

202202:ref:`sect-do`. It extends ``Applicative`` as defined above, and is

203203defined as follows:

204204

@@ -210,11 +210,11 @@ defined as follows:

210210Inside a ``do`` block, the following syntactic transformations are

211211applied:

212212

213−- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``

213+- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``

214214

215−- ``v; e`` becomes ``v >>= (\backslash_ => e)``

215+- ``v; e`` becomes ``v >>= (\backslash_ => e)``

216216

217−- ``let x = v; e`` becomes ``let x = v in e``

217+- ``let x = v; e`` becomes ``let x = v in e``

218218

219219``IO`` is an instance of ``Monad``, defined using primitive functions.

220220We can also define an instance for ``Maybe``, as follows:

@@ -226,7 +226,7 @@ We can also define an instance for ``Maybe``, as follows:

226226 (Just x) >>= k = k x

227227

228228Using 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:

230230

231231.. code-block:: idris

232232

@@ -235,8 +235,8 @@ Using this we can, for example, define a function which adds two

235235 y' <- y -- Extract value from y

236236 return (x' + y') -- Add them

237237

238−This function will extract the values from ``x`` and ``y``, if they are

239−available, or return ``Nothing`` if they are not. Managing the

238+This function will extract the values from ``x`` and ``y``, if they

239+are available, or return ``Nothing`` if they are not. Managing the

240240``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the

241241``do`` notation.

242242

@@ -252,8 +252,8 @@ available, or return ``Nothing`` if they are not. Managing the

252252

253253In many cases, using ``do``-notation can make programs unnecessarily

254254verbose, 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

256−version, as follows:

255+bound is used once, immediately. In these cases, we can use a

256+shorthand version, as follows:

257257

258258.. code-block:: idris

259259

@@ -261,8 +261,8 @@ version, as follows:

261261 m_add x y = return (!x + !y)

262262

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

264−evaluated and then implicitly bound. Conceptually, we can think of ``!``

265−as being a prefix function with the following type:

264+evaluated and then implicitly bound. Conceptually, we can think of

265+``!`` as being a prefix function with the following type:

266266

267267.. code-block:: idris

268268

@@ -276,13 +276,13 @@ to right. In practice, ``!``-notation allows us to program in a more

276276direct style, while still giving a notational clue as to which

277277expressions are monadic.

278278

279−For example, the expression…

279+For example, the expression:

280280

281281.. code-block:: idris

282282

283283 let y = 42 in f !(g !(print y) !x)

284284

285−…is lifted to:

285+is lifted to:

286286

287287.. code-block:: idris

288288

@@ -294,9 +294,9 @@ For example, the expression…

294294Monad comprehensions

295295~~~~~~~~~~~~~~~~~~~~

296296

297−The list comprehension notation we saw in Section :ref:`sect-more-expr` is more

298−general, and applies to anything which is an instance of both ``Monad``

299−and ``Alternative``:

297+The list comprehension notation we saw in Section

298+:ref:`sect-more-expr` is more general, and applies to anything which

299+is an instance of both ``Monad`` and ``Alternative``:

300300

301301.. code-block:: idris

302302

@@ -304,18 +304,18 @@ and ``Alternative``:

304304 empty : f a

305305 (<|>) : f a -> f a -> f a

306306

307−In general, a comprehension takes the form

308−``[ exp | qual1, qual2, …, qualn ]`` where ``quali`` can be one of:

307+In general, a comprehension takes the form ``[ exp | qual1, qual2, …,

308+qualn ]`` where ``quali`` can be one of:

309309

310−- A generator ``x <- e``

310+- A generator ``x <- e``

311311

312−- A *guard*, which is an expression of type ``Bool``

312+- A *guard*, which is an expression of type ``Bool``

313313

314−- A let binding ``let x = e``

314+- A let binding ``let x = e``

315315

316316To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first

317−any qualifier ``qual`` which is a *guard* is translated to

318−``guard qual``, using the following function:

317+any qualifier ``qual`` which is a *guard* is translated to ``guard

318+qual``, using the following function:

319319

320320.. code-block:: idris

321321

@@ -338,13 +338,13 @@ would be:

338338Idiom brackets

339339--------------

340340

341−While ``do`` notation gives an alternative meaning to sequencing, idioms

342−give an alternative meaning to *application*. The notation and larger

343−example in this section is inspired by Conor McBride and Ross Paterson’s

344−paper “Applicative Programming with Effects” [1]_.

341+While ``do`` notation gives an alternative meaning to sequencing,

342+idioms give an alternative meaning to *application*. The notation and

343+larger example in this section is inspired by Conor McBride and Ross

344+Paterson’s paper “Applicative Programming with Effects” [1]_.

345345

346346First, 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

348348could abstract out the application:

349349

350350.. code-block:: idris

@@ -365,8 +365,8 @@ alternative notion of function application, with explicit calls to

365365Rather than having to insert ``m_app`` everywhere there is an

366366application, we can use to do the job for us. To do this, we can make

367367``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``

369−library):

368+defined in the same way as ``m_app`` above (this is defined in the

369+``Idris`` library):

370370

371371.. code-block:: idris

372372

@@ -376,8 +376,9 @@ library):

376376 (Just f) <*> (Just a) = Just (f a)

377377 _ <*> _ = Nothing

378378

379−Using we can use this instance as follows, where a function application

380−``[| f a1 …an |]`` is translated into ``pure f <> a1 <> …<> an``:

379+Using we can use this instance as follows, where a function

380+application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>

381+…<> an``:

381382

382383.. code-block:: idris

383384

@@ -387,9 +388,9 @@ Using we can use this instance as follows, where a function application

387388An error-handling interpreter

388389~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

389390

390−Idiom notation is commonly useful when defining evaluators. McBride and

391−Paterson describe such an evaluator [1]_, for a language similar to the

392−following:

391+Idiom notation is commonly useful when defining evaluators. McBride

392+and Paterson describe such an evaluator [1]_, for a language similar

393+to the following:

393394

394395.. code-block:: idris

395396

@@ -423,8 +424,8 @@ retrieve values from the context during evaluation:

423424When defining an evaluator for the language, we will be applying

424425functions in the context of an ``Eval``, so it is natural to make

425426``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an

426−instance of ``Applicative`` it is necessary to make ``Eval`` an instance

427−of ``Functor``:

427+instance of ``Applicative`` it is necessary to make ``Eval`` an

428+instance of ``Functor``:

428429

429430.. code-block:: idris

430431

@@ -471,7 +472,7 @@ To achieve this, instances can be *named* as follows:

471472This declares an instance as normal, but with an explicit name,

472473``myord``. The syntax ``compare @{myord}`` gives an explicit instance to

473474``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.

475476Given the following list:

476477

477478.. code-block:: idris

@@ -479,7 +480,7 @@ Given the following list:

479480 testList : List Nat

480481 testList = [3,4,1]

481482

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

483484instance ``myord`` as follows, at the ``Idris`` prompt:

484485

485486::

docs/tutorial/conclusions.rst+5−5

@@ -11,24 +11,24 @@ dependent types in general, can be obtained from various sources:

1111 questions on the mailing list.

1212

1313- The IRC channel ``#idris``, on

14− `chat.freenode.net <chat.freenode.net>`__.

14+ `chat.freenode.net <http://chat.freenode.net>`__.

1515

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

1717 user provided information, in particular:

1818

1919 - https://github.com/idris-lang/Idris-dev/wiki/Manual

2020

2121 - https://github.com/idris-lang/Idris-dev/wiki/Language-Features

2222

23−- Examining the prelude and exploring the ``samples`` in the

23+- Examining the prelude and exploring the ``samples`` in the

2424 distribution. The ``Idris`` source can be found online at:

2525 https://github.com/idris-lang/Idris-dev.

2626

2727- Existing projects on the ``Idris Hackers`` web space:

2828 http://idris-hackers.github.io.

2929

30−- Various papers (e.g. [1]_, [2]_, and [3]_).

31− Although these mostly describe older versions of ``Idris``.

30+- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly

31+ describe older versions of ``Idris``.

3232

3333.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems

3434 programming with embedded domain specific languages. In

docs/tutorial/interactive.rst+51−45

@@ -5,29 +5,31 @@ Interactive Editing

55===================

77By 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

9−more precise description of its intended behaviour in its *type*. We

8+system can give extra confidence in a function’s correctness by giving

9+a more precise description of its intended behaviour in its *type*. We

1010have also seen an example of how the type system can help with EDSL

1111development by allowing a programmer to describe the type system of an

1212object language. However, precise types give us more than verification

13−of programs — we can also exploit types to help write programs which are

14−*correct by construction*.

13+of programs — we can also exploit types to help write programs which

14+are *correct by construction*.

1515

1616The ``Idris`` REPL provides several commands for inspecting and

1717modifying parts of programs, based on their types, such as case

18−splitting on a pattern variable, inspecting the type of a metavariable,

19−and even a basic proof search mechanism. In this section, we explain how

20−these features can be exploited by a text editor, and specifically how

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

18+splitting on a pattern variable, inspecting the type of a

19+metavariable, and even a basic proof search mechanism. In this

20+section, we explain how these features can be exploited by a text

21+editor, and specifically how to do so in `Vim

22+<https://github.com/idris-hackers/idris-vim>`_. An interactive mode

23+for `Emacs <https://github.com/idris-hackers/idris-emacs>`_ is also

2224available.

2325

2426

2527Editing at the REPL

2628-------------------

2729

28−The REPL provides a number of commands, which we will describe shortly,

29−which generate new program fragments based on the currently loaded

30−module. These take the general form

30+The REPL provides a number of commands, which we will describe

31+shortly, which generate new program fragments based on the currently

32+loaded module. These take the general form

3133

3234::

3335

@@ -63,8 +65,8 @@ Editing Commands

6365~~~~~~~~~~

6466

6567The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a

66−template definition for the function named ``f`` declared on line ``n``.

67−For example, if the code beginning on line 94 contains:

68+template definition for the function named ``f`` declared on line

69+``n``. For example, if the code beginning on line 94 contains:

6870

6971.. code-block:: idris

7072

@@ -111,23 +113,23 @@ then ``:cs 96 xs`` will give:

111113

112114That is, the pattern variable ``xs`` has been split into the two

113115possible cases ``[]`` and ``x :: xs``. Again, the names are chosen

114−according to the same heuristic. If we update the file (using ``:cs!``)

115−then case split on ``ys`` on the same line, we get:

116+according to the same heuristic. If we update the file (using

117+``:cs!``) then case split on ``ys`` on the same line, we get:

116118

117119.. code-block:: idris

118120

119121 vzipWith f [] [] = ?vzipWith_rhs_3

120122

121123That is, the pattern variable ``ys`` has been split into one case

122−``[]``, ``Idris`` having noticed that the other possible case

123−``y :: ys`` would lead to a unification error.

124+``[]``, ``Idris`` having noticed that the other possible case ``y ::

125+ys`` would lead to a unification error.

124126

125127:addmissing

126128~~~~~~~~~~~

127129

128130The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

129131clauses 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

131133

132134.. code-block:: idris

133135

@@ -168,25 +170,27 @@ then ``:ps 96 vzipWith_rhs_1`` will give

168170

169171 []

170172

171−This works because it is searching for a ``Vect`` of length 0, of which

172−the empty vector is the only possibiliy. Similarly, and perhaps

173−surprisingly, there is only one possibility if we try to solve

174−``:ps 97 vzipWith_rhs_2``:

173+This works because it is searching for a ``Vect`` of length 0, of

174+which the empty vector is the only possibiliy. Similarly, and perhaps

175+surprisingly, there is only one possibility if we try to solve ``:ps

176+97 vzipWith_rhs_2``:

175177

176178.. code-block:: idris

177179

178180 f x y :: (vzipWith f xs ys)

179181

180−This works because ``vzipWith`` has a precise enough type: The resulting

181−vector has to be non-empty (a ``::``); the first element must have type

182−``c`` and the only way to get this is to apply ``f`` to ``x`` and ``y``;

183−finally, the tail of the vector can only be built recursively.

182+This works because ``vzipWith`` has a precise enough type: The

183+resulting vector has to be non-empty (a ``::``); the first element

184+must have type ``c`` and the only way to get this is to apply ``f`` to

185+``x`` and ``y``; finally, the tail of the vector can only be built

186+recursively.

184187

185188:makewith

186189~~~~~~~~~

187190

188−The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a ``with``

189−to a pattern clause. For example, recall ``parity``. If line 10 is:

191+The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a

192+``with`` to a pattern clause. For example, recall ``parity``. If line

193+10 is:

190194

191195.. code-block:: idris

192196

@@ -209,9 +213,10 @@ patterns:

209213 parity (S (S (plus n n))) | odd = ?parity_rhs_2

210214

211215Note that case splitting has normalised the patterns here (giving

212−``plus`` rather than ``+``). In any case, we see that using interactive

213−editing significantly simplifies the implementation of dependent pattern

214−matching by showing a programmer exactly what the valid patterns are.

216+``plus`` rather than ``+``). In any case, we see that using

217+interactive editing significantly simplifies the implementation of

218+dependent pattern matching by showing a programmer exactly what the

219+valid patterns are.

215220

216221Interactive Editing in Vim

217222--------------------------

@@ -221,32 +226,33 @@ interactive editing support using the commands described above.

221226Interactive editing is achieved using the following editor commands,

222227each of which update the buffer directly:

223228

224−- ``\d`` adds a template definition for the name declared on the

229+- ``\d`` adds a template definition for the name declared on the

225230 current line (using ``:addclause``).

226231

227−- ``\c`` case splits the variable at the cursor (using ``:casesplit``).

232+- ``\c`` case splits the variable at the cursor (using

233+ ``:casesplit``).

228234

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

230236 ``:addmissing``).

231237

232−- ``\w`` adds a ``with`` clause (using ``:makewith``).

238+- ``\w`` adds a ``with`` clause (using ``:makewith``).

233239

234−- ``\o`` invokes a proof search to solve the metavariable under the

240+- ``\o`` invokes a proof search to solve the metavariable under the

235241 cursor (using ``:proofsearch``).

236242

237−- ``\p`` invokes a proof search with additional hints to solve the

243+- ``\p`` invokes a proof search with additional hints to solve the

238244 metavariable under the cursor (using ``:proofsearch``).

239245

240246There are also commands to invoke the type checker and evaluator:

241247

242−- ``\t`` displays the type of the (globally visible) name under the

243− cursor. In the case of a metavariable, this displays the context and

244− the expected type.

248+- ``\t`` displays the type of the (globally visible) name under the

249+ cursor. In the case of a metavariable, this displays the context

250+ and the expected type.

245251

246−- ``\e`` prompts for an expression to evaluate.

252+- ``\e`` prompts for an expression to evaluate.

247253

248−- ``\r`` reloads and type checks the buffer.

254+- ``\r`` reloads and type checks the buffer.

249255

250−Corresponding commands are also available in the Emacs mode. Support for

251−other editors can be added in a relatively straighforward manner by

252−using ``idris –client``.

256+Corresponding commands are also available in the Emacs mode. Support

257+for other editors can be added in a relatively straighforward manner

258+by using ``idris –client``.

docs/tutorial/interp.rst+31−28

@@ -6,9 +6,10 @@ Example: The Well-Typed Interpreter

77In this section, we’ll use the features we’ve seen so far to write a

88larger example, an interpreter for a simple functional programming

9−language, with variables, function application, binary operators and an

10−``if...then...else`` construct. We will use the dependent type system to

11−ensure that any programs which can be represented are well-typed.

9+language, with variables, function application, binary operators and

10+an ``if...then...else`` construct. We will use the dependent type

11+system to ensure that any programs which can be represented are

12+well-typed.

1213

1314Representing Languages

1415----------------------

@@ -74,8 +75,8 @@ look at each constructor in turn.

7475

7576We use a nameless representation for variables — they are *de Bruijn

7677indexed*. 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−context ``G`` has type ``T``. This is defined as follows:

78+the context, ``HasType i G T``, which is a proof that variable ``i``

79+in context ``G`` has type ``T``. This is defined as follows:

7980

8081.. code-block:: idris

8182

@@ -87,17 +88,17 @@ We can treat *Stop* as a proof that the most recently defined variable

8788is well-typed, and *Pop n* as a proof that, if the ``n``\ th most

8889recently defined variable is well-typed, so is the ``n+1``\ th. In

8990practice, 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−``Var`` constructor:

91+defined variable, ``Pop Stop`` to refer to the next, and so on, via

92+the ``Var`` constructor:

9293

9394.. code-block:: idris

9495

9596 Var : HasType i G t -> Expr G t

9697

97−So, in an expression ``\x,\y. x y``, the variable ``x`` would have a de

98−Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``, represented

99−as ``Stop``. We find these by counting the number of lambdas between the

100−definition and the use.

98+So, in an expression ``\x,\y. x y``, the variable ``x`` would have a

99+de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,

100+represented as ``Stop``. We find these by counting the number of

101+lambdas between the definition and the use.

101102

102103A value carries a concrete representation of an integer:

103104

@@ -105,9 +106,9 @@ A value carries a concrete representation of an integer:

105106

106107 Val : (x : Int) -> Expr G TyInt

107108

108−A lambda creates a function. In the scope of a function of type

109−``a -> t``, there is a new local variable of type ``a``, which is

110−expressed by the context index:

109+A lambda creates a function. In the scope of a function of type ``a ->

110+t``, there is a new local variable of type ``a``, which is expressed

111+by the context index:

111112

112113.. code-block:: idris

113114

@@ -128,9 +129,9 @@ informs what the types of the arguments must be:

128129 Op : (interpTy a -> interpTy b -> interpTy c) ->

129130 Expr G a -> Expr G b -> Expr G c

130131

131−Finally, if expressions make a choice given a boolean. Each branch must

132−have the same type, and we will evaluate the branches lazily so that

133−only the branch which is taken need be evaluated:

132+Finally, if expressions make a choice given a boolean. Each branch

133+must have the same type, and we will evaluate the branches lazily so

134+that only the branch which is taken need be evaluated:

134135

135136.. code-block:: idris

136137

@@ -142,13 +143,14 @@ only the branch which is taken need be evaluated:

142143Writing the Interpreter

143144-----------------------

144145

145−When we evaluate an ``Expr``, we’ll need to know the values in scope, as

146−well as their types. ``Env`` is an environment, indexed over the types

147−in scope. Since an environment is just another form of list, albeit with

148−a strongly specified connection to the vector of local variable types,

149−we use the usual ``::`` and ``Nil`` constructors so that we can use the

150−usual list syntax. Given a proof that a variable is defined in the

151−context, we can then produce a value from the environment:

146+When we evaluate an ``Expr``, we’ll need to know the values in scope,

147+as well as their types. ``Env`` is an environment, indexed over the

148+types in scope. Since an environment is just another form of list,

149+albeit with a strongly specified connection to the vector of local

150+variable types, we use the usual ``::`` and ``Nil`` constructors so

151+that we can use the usual list syntax. Given a proof that a variable

152+is defined in the context, we can then produce a value from the

153+environment:

152154

153155.. code-block:: idris

154156

@@ -258,10 +260,11 @@ function on user input:

258260 x <- getLine

259261 print (interp [] fact (cast x))

260262

261−Here, ``cast`` is an overloaded function which converts a value from one

262−type to another if possible. Here, it converts a string to an integer,

263−giving 0 if the input is invalid. An example run of this program at the

264−``Idris`` interactive environment is shown in Listing :ref:`factrun`.

263+Here, ``cast`` is an overloaded function which converts a value from

264+one type to another if possible. Here, it converts a string to an

265+integer, giving 0 if the input is invalid. An example run of this

266+program at the ``Idris`` interactive environment is shown in Listing

267+:ref:`factrun`.

265268

266269

267270.. literalinclude:: ../listing/idris-prompt-interp.txt

docs/tutorial/introduction.rst+15−12

@@ -1,11 +1,14 @@

1+.. _sect-intro:

13===========

24Introducton

35===========

57In conventional programming languages, there is a clear distinction

6−between *types* and *values*. For example, in `Haskell <http://www.haskell.org>`_, the following

7−are types, representing integers, characters, lists of characters, and

8−lists of any value respectively:

8+between *types* and *values*. For example, in `Haskell

9+<http://www.haskell.org>`_, the following are types, representing

10+integers, characters, lists of characters, and lists of any value

11+respectively:

912

1013- ``Int``, ``Char``, ``[Char]``, ``[a]``

1114

@@ -22,11 +25,11 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element

2225type and ``n`` is the length of the list and can be an arbitrary term.

2326

2427When 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

26−to describe its own properties. For example, concatenating two lists has

27−the property that the resulting list’s length is the sum of the lengths

28−of the two input lists. We can therefore give the following type to the

29−``app`` function, which concatenates vectors:

28+properties (e.g. the length of a list) the type of a function can

29+begin to describe its own properties. For example, concatenating two

30+lists has the property that the resulting list’s length is the sum of

31+the lengths of the two input lists. We can therefore give the

32+following type to the ``app`` function, which concatenates vectors:

3033

3134.. code-block:: idris

3235

@@ -34,10 +37,10 @@ of the two input lists. We can therefore give the following type to the

3437

3538This tutorial introduces ``Idris``, a general purpose functional

3639programming language with dependent types. The goal of the ``Idris``

37−project is to build a dependently typed language suitable for verifiable

38−*systems* programming. To this end, ``Idris`` is a compiled language

39−which aims to generate efficient executable code. It also has a

40−lightweight foreign function interface which allows easy interaction

40+project is to build a dependently typed language suitable for

41+verifiable *systems* programming. To this end, ``Idris`` is a compiled

42+language which aims to generate efficient executable code. It also has

43+a lightweight foreign function interface which allows easy interaction

4144with external ``C`` libraries.

4245

4346Intended Audience

docs/tutorial/starting.rst+25−24

@@ -7,13 +7,14 @@ Getting Started

77Prerequisites

88-------------

10−Before installing ``Idris``, you will need to make sure you have all of

11−the necessary libraries and tools. You will need:

10+Before installing ``Idris``, you will need to make sure you have all

11+of the necessary libraries and tools. You will need:

1212

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.

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

15+ date.

1516

16−- The *GNU Multiple Precision Arithmetic Library* (GMP) is available

17+- The *GNU Multiple Precision Arithmetic Library* (GMP) is available

1718 from MacPorts/Homebrew and all major Linux distributions.

1819

1920Downloading and Installing

@@ -26,10 +27,10 @@ prerequisites, is to type:

2627

2728 cabal update; cabal install idris

2829

29−This will install the latest version released on Hackage, along with any

30−dependencies. If, however, you would like the most up to date

30+This will install the latest version released on Hackage, along with

31+any dependencies. If, however, you would like the most up to date

3132development 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.

3334

3435To check that installation has succeeded, and to write your first

3536``Idris`` program, create a file called “``hello.idr``” containing the

@@ -37,9 +38,9 @@ following text:

3738

3839If you are familiar with Haskell, it should be fairly clear what the

3940program 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−``idris hello.idr -o hello`` at the shell prompt. This will create an

42−executable called ``hello``, which you can run:

41+details later. You can compile the program to an executable by

42+entering ``idris hello.idr -o hello`` at the shell prompt. This will

43+create an executable called ``hello``, which you can run:

4344

4445::

4546

@@ -49,16 +50,16 @@ executable called ``hello``, which you can run:

4950

5051Note that the ``$`` indicates the shell prompt! Should the ``Idris``

5152executable not be found please ensure that you have added

52−``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X users

53−may find they need to use ``~/Library/Haskell/bin`` instead. Some useful

54−options to the ``Idris`` command are:

53+``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X

54+users may find they need to use ``~/Library/Haskell/bin``

55+instead. Some useful options to the ``Idris`` command are:

5556

56−- ``-o prog`` to compile to an executable called ``prog``.

57+- ``-o prog`` to compile to an executable called ``prog``.

5758

58−- ``--check`` type check the file and its dependencies without starting

59− the interactive environment.

59+- ``--check`` type check the file and its dependencies without

60+ starting the interactive environment.

6061

61−- ``--help`` display usage summary and command line options

62+- ``--help`` display usage summary and command line options

6263

6364The Interactive Environment

6465---------------------------

@@ -71,12 +72,12 @@ environment. You should see something like the following:

7172This gives a ``ghci`` style interface which allows evaluation of, as

7273well as type checking of, expressions; theorem proving, compilation;

7374editing; and various other operations. The command ``:?`` gives a list

74−of supported commands. Listing :ref:`run1` shows an example run in which

75−``hello.idr`` is loaded, the type of ``main`` is checked and then the

76−program is compiled to the executable ``hello``. Type checking a file,

77−if successful, creates a bytecode version of the file (in this case

78−``hello.ibc``) to speed up loading in future. The bytecode is

79−regenerated if the source file changes.

75+of supported commands. Listing :ref:`run1` shows an example run in

76+which ``hello.idr`` is loaded, the type of ``main`` is checked and

77+then the program is compiled to the executable ``hello``. Type

78+checking a file, if successful, creates a bytecode version of the file

79+(in this case ``hello.ibc``) to speed up loading in future. The

80+bytecode is regenerated if the source file changes.

8081

8182.. literalinclude:: ../listing/idris-prompt-helloworld.txt

8283 :caption: Sample Interactive Run

docs/tutorial/syntax.rst+38−39

@@ -2,18 +2,17 @@ Syntax Extensions

22=================

44supports the implementation of *Embedded Domain Specific Languages*

5−(EDSLs) in several ways [1]_. One way, as we have

6−already seen, is through extending ``do`` notation. Another important

7−way is to allow extension of the core syntax. In this section we

8−describe two ways of extending the syntax: ``syntax`` rules and ``dsl``

9−notation.

5+(EDSLs) in several ways [1]_. One way, as we have already seen, is

6+through extending ``do`` notation. Another important way is to allow

7+extension of the core syntax. In this section we describe two ways of

8+extending the syntax: ``syntax`` rules and ``dsl`` notation.

109

1110``syntax`` rules

1211----------------

1312

1413We 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

16−already seen this function in Section :ref:`sect-lazy`):

14+in. Instead, we can define a function in the prelude as follows (we

15+have already seen this function in Section :ref:`sect-lazy`):

1716

1817.. code-block:: idris

1918

@@ -46,13 +45,13 @@ itself consists of:

4645 also be used to include reserved words in syntax rules, such as

4746 ``let`` or ``in``.

4847

49−The limitations on the form of a syntax rule are that it must include at

50−least one symbol or keyword, and there must be no repeated variables

51−standing for non-terminals. Any expression can be used, but if there are

52−two non-terminals in a row in a rule, only simple expressions may be

53−used (that is, variables, constants, or bracketed expressions). Rules

54−can use previously defined rules, but may not be recursive. The

55−following syntax extensions would therefore be valid:

48+The limitations on the form of a syntax rule are that it must include

49+at least one symbol or keyword, and there must be no repeated

50+variables standing for non-terminals. Any expression can be used, but

51+if there are two non-terminals in a row in a rule, only simple

52+expressions may be used (that is, variables, constants, or bracketed

53+expressions). Rules can use previously defined rules, but may not be

54+recursive. The following syntax extensions would therefore be valid:

5655

5756.. code-block:: idris

5857

@@ -63,7 +62,7 @@ following syntax extensions would therefore be valid:

6362

6463Syntax macros can be further restricted to apply only in patterns (i.e.,

6564only 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

6766being marked as ``pattern`` or ``term`` syntax rules. For example, we

6867might define an interval as follows, with a static check that the lower

6968bound is below the upper bound using ``so``:

@@ -74,8 +73,8 @@ bound is below the upper bound using ``so``:

7473 MkInterval : (lower : Float) -> (upper : Float) ->

7574 so (lower < upper) -> Interval

7675

77−We can define a syntax which, in patterns, always matches ``oh`` for the

78−proof argument, and in terms requires a proof term to be provided:

76+We can define a syntax which, in patterns, always matches ``oh`` for

77+the proof argument, and in terms requires a proof term to be provided:

7978

8079.. code-block:: idris

8180

@@ -97,23 +96,23 @@ forms. For example, a ``for`` loop binds a variable on each iteration:

9796 putStrLn ("Number " ++ show x)

9897 putStrLn "Done!"

9998

100−Note that we have used the ``{x}`` form to state that ``x`` represents a

101−bound variable, substituted on the right hand side. We have also put

99+Note that we have used the ``{x}`` form to state that ``x`` represents

100+a bound variable, substituted on the right hand side. We have also put

102101``in`` in quotation marks since it is already a reserved word.

103102

104103``dsl`` notation

105104----------------

106105

107−The well-typed interpreter in Section :ref:`sect-interp` is a simple example

108−of a common programming pattern with dependent types. Namely: describe

109−an *object language* and its type system with dependent types to

110−guarantee that only well-typed programs can be represented, then program

111−using that representation. Using this approach we can, for example,

112−write programs for serialising binary data [2]_ or running

106+The well-typed interpreter in Section :ref:`sect-interp` is a simple

107+example of a common programming pattern with dependent types. Namely:

108+describe an *object language* and its type system with dependent types

109+to guarantee that only well-typed programs can be represented, then

110+program using that representation. Using this approach we can, for

111+example, write programs for serialising binary data [2]_ or running

113112concurrent processes safely [3]_.

114113

115−Unfortunately, the form of object language programs makes it rather hard

116−to program this way in practice. Recall the factorial program in

114+Unfortunately, the form of object language programs makes it rather

115+hard to program this way in practice. Recall the factorial program in

117116``Expr`` for example:

118117

119118.. code-block:: idris

@@ -124,8 +123,8 @@ to program this way in practice. Recall the factorial program in

124123 (Var Stop)))

125124

126125Since this is a particularly useful pattern, ``Idris`` provides syntax

127−overloading [1]_ to make it easier to program in such

128−object languages:

126+overloading [1]_ to make it easier to program in such object

127+languages:

129128

130129.. code-block:: idris

131130

@@ -138,15 +137,15 @@ object languages:

138137 index_next = Pop

139138 lambda = mkLam

140139

141−A ``dsl`` block describes how each syntactic construct is represented in

142−an object language. Here, in the ``expr`` language, any variable is

140+A ``dsl`` block describes how each syntactic construct is represented

141+in an object language. Here, in the ``expr`` language, any variable is

143142translated to the ``Var`` constructor, using ``Pop`` and ``Stop`` to

144143construct the de Bruijn index (i.e., to count how many bindings since

145144the variable itself was bound); and any lambda is translated to a

146145``Lam`` constructor. The ``mkLam`` function simply ignores its first

147−argument, which is the name that the user chose for the variable. It is

148−also possible to overload ``let`` and dependent function syntax (``pi``)

149−in this way. We can now write ``fact`` as follows:

146+argument, which is the name that the user chose for the variable. It

147+is also possible to overload ``let`` and dependent function syntax

148+(``pi``) in this way. We can now write ``fact`` as follows:

150149

151150.. code-block:: idris

152151

@@ -154,8 +153,8 @@ in this way. We can now write ``fact`` as follows:

154153 fact = expr (\x => If (Op (==) x (Val 0))

155154 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))

156155

157−In this new version, ``expr`` declares that the next expression will be

158−overloaded. We can take this further, using idiom brackets, by

156+In this new version, ``expr`` declares that the next expression will

157+be overloaded. We can take this further, using idiom brackets, by

159158declaring:

160159

161160.. code-block:: idris

@@ -167,9 +166,9 @@ declaring:

167166 pure = id

168167

169168Note that there is no need for these to be part of an instance of

170−``Applicative``, since idiom bracket notation translates directly to the

171−names ``<*>`` and ``pure``, and ad-hoc type-directed overloading is

172−allowed. We can now say:

169+``Applicative``, since idiom bracket notation translates directly to

170+the names ``<*>`` and ``pure``, and ad-hoc type-directed overloading

171+is allowed. We can now say:

173172

174173.. code-block:: idris

175174

docs/tutorial/typesfuns.rst+203−188

@@ -1,3 +1,5 @@

1+.. _sect-typefuns:

13===================

24Types and Functions

35===================

@@ -11,8 +13,8 @@ manipulation, and ``Ptr`` which represents foreign pointers. There are

1113also several data types declared in the library, including ``Bool``,

1214with values ``True`` and ``False``. We can declare some constants with

1315these types. Enter the following into a file ``prims.idr`` and load it

14−into the ``Idris`` interactive environment by typing

15−``idris prims.idr``:

16+into the ``Idris`` interactive environment by typing ``idris

17+prims.idr``:

1618

1719.. code-block:: idris

1820

@@ -34,13 +36,14 @@ An ``Idris`` file consists of an optional module declaration (here

3436``module prims``) followed by an optional list of imports (none here,

3537however ``Idris`` programs can consist of several modules, and the

3638definitions in each module each have their own namespace, as we will

37−discuss in Section :ref:`sect-namespaces`) and a collection of declarations

38−and definitions. The order of definitions is significant — functions and

39−data types must be defined before use. Each definition must have a type

40−declaration, for example see ``x : Int``, ``foo : String``, from the

41−above listing. Indentation is significant — a new declaration begins at

42−the same level of indentation as the preceding declaration.

43−Alternatively, declarations may be terminated with a semicolon.

39+discuss in Section :ref:`sect-namespaces`) and a collection of

40+declarations and definitions. The order of definitions is significant

41+— functions and data types must be defined before use. Each definition

42+must have a type declaration, for example see ``x : Int``, ``foo :

43+String``, from the above listing. Indentation is significant — a new

44+declaration begins at the same level of indentation as the preceding

45+declaration. Alternatively, declarations may be terminated with a

46+semicolon.

4447

4548A library module ``prelude`` is automatically imported by every

4649``Idris`` program, including facilities for IO, arithmetic, data

@@ -56,10 +59,10 @@ answer. For example:

5659 *prims> x == 6*6+6

5760 True : Bool

5861

59−All of the usual arithmetic and comparison operators are defined for the

60−primitive types. They are overloaded using type classes, as we will

61−discuss in Section :ref:`sect-classes` and can be extended to work on user

62−defined types. Boolean expressions can be tested with the

62+All of the usual arithmetic and comparison operators are defined for

63+the primitive types. They are overloaded using type classes, as we

64+will discuss in Section :ref:`sect-classes` and can be extended to

65+work on user defined types. Boolean expressions can be tested with the

6366``if...then...else`` construct:

6467

6568::

@@ -71,8 +74,8 @@ Data Types

7174----------

7275

7376Data 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

75−as follows:

77+similar syntax. Natural numbers and lists, for example, can be

78+declared as follows:

7679

7780.. code-block:: idris

7881

@@ -81,19 +84,21 @@ as follows:

8184 data List a = Nil | (::) a (List a) -- Polymorphic lists

8285

8386The above declarations are taken from the standard library. Unary

84−natural numbers can be either zero (``Z``), or the successor of another

85−natural number (``S k``). Lists can either be empty (``Nil``) or a value

86−added to the front of another list (``x :: xs``). In the declaration for

87−``List``, we used an infix operator ``::``. New operators such as this

88−can be added using a fixity declaration, as follows:

87+natural numbers can be either zero (``Z``), or the successor of

88+another natural number (``S k``). Lists can either be empty (``Nil``)

89+or a value added to the front of another list (``x :: xs``). In the

90+declaration for ``List``, we used an infix operator ``::``. New

91+operators such as this can be added using a fixity declaration, as

92+follows:

8993

9094::

9195

9296 infixr 10 ::

9397

9498Functions, data constructors and type constructors may all be given

95−infix operators as names. They may be used in prefix form if enclosed in

96−brackets, e.g. \ ``(::)``. Infix operators can use any of the symbols:

99+infix operators as names. They may be used in prefix form if enclosed

100+in brackets, e.g. ``(::)``. Infix operators can use any of the

101+symbols:

97102

98103::

99104

@@ -104,9 +109,10 @@ Functions

104109

105110Functions are implemented by pattern matching, again using a similar

106111syntax to Haskell. The main difference is that ``Idris`` requires type

107−declarations for all functions, using a single colon ``:`` (rather than

108−Haskell’s double colon ``::``). Some natural number arithmetic functions

109−can be defined as follows, again taken from the standard library:

112+declarations for all functions, using a single colon ``:`` (rather

113+than Haskell’s double colon ``::``). Some natural number arithmetic

114+functions can be defined as follows, again taken from the standard

115+library:

110116

111117.. code-block:: idris

112118

@@ -123,10 +129,11 @@ can be defined as follows, again taken from the standard library:

123129The standard arithmetic operators ``+`` and ``*`` are also overloaded

124130for use by ``Nat``, and are implemented using the above functions.

125131Unlike Haskell, there is no restriction on whether types and function

126−names must begin with a capital letter or not. Function names (``plus``

127−and ``mult`` above), data constructors (``Z``, ``S``, ``Nil`` and

128−``::``) and type constructors (``Nat`` and ``List``) are all part of the

129−same namespace. We can test these functions at the ``Idris`` prompt:

132+names must begin with a capital letter or not. Function names

133+(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,

134+``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are

135+all part of the same namespace. We can test these functions at the

136+``Idris`` prompt:

130137

131138::

132139

@@ -135,10 +142,12 @@ same namespace. We can test these functions at the ``Idris`` prompt:

135142 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))

136143 12 : Nat

137144

138−**Note:** ``Idris`` automatically desugars the ``Nat`` representation

139−into a more human readable format. The result of

140−``plus (S (S Z)) (S (S Z))`` is actually ``(S (S (S (S Z))))`` which is

141−the Integer 4. This can be checked at the ``Idris`` prompt:

145+.. note::

146+

147+ ``Idris`` automatically desugars the ``Nat`` representation into a

148+ more human readable format. The result of ``plus (S (S Z)) (S (S Z))``

149+ is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be

150+ checked at the ``Idris`` prompt:

142151

143152::

144153

@@ -156,12 +165,12 @@ type classes, meaning that we can also test the functions as follows:

156165 12 : Nat

157166

158167You 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

160−primarily that unary numbers have a very convenient structure which is

161−easy to reason about, and easy to relate to other data structures as we

162−will see later. Nevertheless, we do not want this convenience to be at

163−the expense of efficiency. Fortunately, ``Idris`` knows about the

164−relationship between ``Nat`` (and similarly structured types) and

168+computers have perfectly good integer arithmetic built in. The reason

169+is primarily that unary numbers have a very convenient structure which

170+is easy to reason about, and easy to relate to other data structures

171+as we will see later. Nevertheless, we do not want this convenience to

172+be at the expense of efficiency. Fortunately, ``Idris`` knows about

173+the relationship between ``Nat`` (and similarly structured types) and

165174numbers. This means it can optimise the representation, and functions

166175such as ``plus`` and ``mult``.

167176

@@ -188,7 +197,7 @@ indented further than the outer function.

188197visible in the ``where`` clause (unless they have been redefined, such

189198as ``xs`` here). A name which appears only in the type will be in scope

190199in 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.

192201

193202As well as functions, ``where`` blocks can include local data

194203declarations, such as the following where ``MyLT`` is not accessible

@@ -210,9 +219,9 @@ In general, functions defined in a ``where`` clause need a type

210219declaration just like any top level function. However, the type

211220declaration for a function ``f`` *can* be omitted if:

212221

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

214223

215−- The type of ``f`` can be completely determined from its first

224+- The type of ``f`` can be completely determined from its first

216225 application

217226

218227So, for example, the following definitions are legal:

@@ -238,9 +247,9 @@ Vectors

238247~~~~~~~

239248

240249A standard example of a dependent type is the type of “lists with

241−length”, conventionally called vectors in the dependent type literature.

242−They are available as part of the ``Idris`` library, by importing

243−``Data.Vect``, or we can declare them as follows:

250+length”, conventionally called vectors in the dependent type

251+literature. They are available as part of the ``Idris`` library, by

252+importing ``Data.Vect``, or we can declare them as follows:

244253

245254.. code-block:: idris

246255

@@ -249,28 +258,28 @@ They are available as part of the ``Idris`` library, by importing

249258 (::) : a -> Vect k a -> Vect (S k) a

250259

251260Note that we have used the same constructor names as for ``List``.

252−Ad-hoc name overloading such as this is accepted by ``Idris``, provided

253−that the names are declared in different namespaces (in practice,

254−normally in different modules). Ambiguous constructor names can normally

255−be resolved from context.

261+Ad-hoc name overloading such as this is accepted by ``Idris``,

262+provided that the names are declared in different namespaces (in

263+practice, normally in different modules). Ambiguous constructor names

264+can normally be resolved from context.

256265

257266This declares a family of types, and so the form of the declaration is

258−rather different from the simple type declarations above. We explicitly

259−state the type of the type constructor ``Vect`` — it takes a ``Nat`` and

260−a type as an argument, where ``Type`` stands for the type of types. We

261−say that ``Vect`` is *indexed* over ``Nat`` and *parameterised* by

262−``Type``. Each constructor targets a different part of the family of

263−types. ``Nil`` can only be used to construct vectors with zero length,

264−and ``::`` to construct vectors with non-zero length. In the type of

265−``::``, we state explicitly that an element of type ``a`` and a tail of

266−type ``Vect k a`` (i.e., a vector of length ``k``) combine to make a

267−vector of length ``S k``.

267+rather different from the simple type declarations above. We

268+explicitly state the type of the type constructor ``Vect`` — it takes

269+a ``Nat`` and a type as an argument, where ``Type`` stands for the

270+type of types. We say that ``Vect`` is *indexed* over ``Nat`` and

271+*parameterised* by ``Type``. Each constructor targets a different part

272+of the family of types. ``Nil`` can only be used to construct vectors

273+with zero length, and ``::`` to construct vectors with non-zero

274+length. In the type of ``::``, we state explicitly that an element of

275+type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length

276+``k``) combine to make a vector of length ``S k``.

268277

269278We can define functions on dependent types such as ``Vect`` in the same

270279way as on simple types such as ``List`` and ``Nat`` above, by pattern

271280matching. The type of a function over ``Vect`` will describe what

272281happens to the lengths of the vectors involved. For example, ``++``,

273−defined as follows, appends two ``Vect``\ s:

282+defined as follows, appends two ``Vect``:

274283

275284.. code-block:: idris

276285

@@ -308,9 +317,9 @@ following:

308317 with

309318 plus k m

310319

311−This error message suggests that there is a length mismatch between two

312−vectors — we needed a vector of length ``k + m``, but provided a vector

313−of length ``k + k``.

320+This error message suggests that there is a length mismatch between

321+two vectors — we needed a vector of length ``k + m``, but provided a

322+vector of length ``k + k``.

314323

315324The Finite Sets

316325~~~~~~~~~~~~~~~

@@ -332,9 +341,9 @@ of elements in the set. Obviously we can’t construct an element of an

332341empty set, so neither constructor targets ``Fin Z``.

333342

334343A useful application of the ``Fin`` family is to represent bounded

335−natural numbers. Since the first ``n`` natural numbers form a finite set

336−of ``n`` elements, we can treat ``Fin n`` as the set of natural numbers

337−bounded by ``n``.

344+natural numbers. Since the first ``n`` natural numbers form a finite

345+set of ``n`` elements, we can treat ``Fin n`` as the set of natural

346+numbers bounded by ``n``.

338347

339348For example, the following function which looks up an element in a

340349``Vect``, by a bounded index given as a ``Fin n``, is defined in the

@@ -347,15 +356,16 @@ prelude:

347356 index (FS k) (x :: xs) = index k xs

348357

349358This 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

351−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.

359+location is bounded by the length of the vector (``n`` in each case),

360+so there is no need for a run-time bounds check. The type checker

361+guarantees that the location is no larger than the length of the

362+vector.

353363

354−Note also that there is no case for ``Nil`` here. This is because it is

355−impossible. Since there is no element of ``Fin Z``, and the location is

356−a ``Fin n``, then ``n`` can not be ``Z``. As a result, attempting to

357−look up an element in an empty vector would give a compile time type

358−error, since it would force ``n`` to be ``Z``.

364+Note also that there is no case for ``Nil`` here. This is because it

365+is impossible. Since there is no element of ``Fin Z``, and the

366+location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,

367+attempting to look up an element in an empty vector would give a

368+compile time type error, since it would force ``n`` to be ``Z``.

359369

360370Implicit Arguments

361371~~~~~~~~~~~~~~~~~~

@@ -376,13 +386,14 @@ names, ``n`` and ``a``, which are not declared explicitly. These are

376386

377387 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

378388

379−Implicit arguments, given in braces ``{}`` in the type declaration, are

380−not given in applications of ``index``; their values can be inferred

381−from the types of the ``Fin n`` and ``Vect n a`` arguments. Any name

382−with a which appears as a parameter or index in a type declaration, but

383−which is otherwise free, will be automatically bound as an implicit

384−argument. Implicit arguments can still be given explicitly in

385−applications, using ``{a=value}`` and ``{n=value}``, for example:

389+Implicit arguments, given in braces ``{}`` in the type declaration,

390+are not given in applications of ``index``; their values can be

391+inferred from the types of the ``Fin n`` and ``Vect n a``

392+arguments. Any name with a which appears as a parameter or index in a

393+type declaration, but which is otherwise free, will be automatically

394+bound as an implicit argument. Implicit arguments can still be given

395+explicitly in applications, using ``{a=value}`` and ``{n=value}``, for

396+example:

386397

387398.. code-block:: idris

388399

@@ -403,10 +414,10 @@ clear.

403414~~~~~~~~~~~~~~~~~~~~

404415

405416Sometimes it is useful to provide types of implicit arguments,

406−particularly where there is a dependency ordering, or where the implicit

407−arguments themselves have dependencies. For example, we may wish to

408−state the types of the implicit arguments in the following definition,

409−which defines a predicate on vectors:

417+particularly where there is a dependency ordering, or where the

418+implicit arguments themselves have dependencies. For example, we may

419+wish to state the types of the implicit arguments in the following

420+definition, which defines a predicate on vectors:

410421

411422.. code-block:: idris

412423

@@ -414,10 +425,10 @@ which defines a predicate on vectors:

414425 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

415426 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

416427

417−An instance of ``Elem x xs`` states that ``x`` is an element of ``xs``.

418−We can construct such a predicate if the required element is ``Here``,

419−at the head of the vector, or ``There``, in the tail of the vector. For

420−example:

428+An instance of ``Elem x xs`` states that ``x`` is an element of

429+``xs``. We can construct such a predicate if the required element is

430+``Here``, at the head of the vector, or ``There``, in the tail of the

431+vector. For example:

421432

422433.. code-block:: idris

423434

@@ -429,8 +440,8 @@ example:

429440

430441If the same implicit arguments are being used a lot, it can make a

431442definition difficult to read. To avoid this problem, a ``using`` block

432−gives the types and ordering of any implicit arguments which can appear

433−within the block:

443+gives the types and ordering of any implicit arguments which can

444+appear within the block:

434445

435446.. code-block:: idris

436447

@@ -445,8 +456,8 @@ Note: Declaration Order and ``mutual`` blocks

445456In general, functions and data types must be defined before use, since

446457dependent types allow functions to appear as part of types, and their

447458reduction behaviour to affect type checking. However, this restriction

448−can be relaxed by using a ``mutual`` block, which allows data types and

449−functions to be defined simultaneously:

459+can be relaxed by using a ``mutual`` block, which allows data types

460+and functions to be defined simultaneously:

450461

451462.. code-block:: idris

452463

@@ -461,7 +472,8 @@ functions to be defined simultaneously:

461472

462473In a ``mutual`` block, first all of the type declarations are added,

463474then 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.

465477

466478I/O

467479---

@@ -477,18 +489,18 @@ side-effects — is that I/O is inherently side-effecting. Therefore in

477489 data IO a -- IO operation returning a value of type a

478490

479491We’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

481−execute them. The resulting operations are executed externally, by the

482−run-time system. We’ve already seen one IO program:

492+describes what the I/O operations to be executed are, rather than how

493+to execute them. The resulting operations are executed externally, by

494+the run-time system. We’ve already seen one IO program:

483495

484496.. code-block:: idris

485497

486498 main : IO ()

487499 main = putStrLn "Hello world"

488500

489−The type of ``putStrLn`` explains that it takes a string, and returns an

490−element of the unit type ``()`` via an I/O action. There is a variant

491−``putStr`` which outputs a string without a newline:

501+The type of ``putStrLn`` explains that it takes a string, and returns

502+an element of the unit type ``()`` via an I/O action. There is a

503+variant ``putStr`` which outputs a string without a newline:

492504

493505.. code-block:: idris

494506

@@ -501,8 +513,8 @@ We can also read strings from user input:

501513

502514 getLine : IO String

503515

504−A number of other I/O operations are defined in the prelude, for example

505−for reading and writing files, including:

516+A number of other I/O operations are defined in the prelude, for

517+example for reading and writing files, including:

506518

507519.. code-block:: idris

508520

@@ -523,10 +535,10 @@ for reading and writing files, including:

523535“``do``” notation

524536-----------------

525537

526−I/O programs will typically need to sequence actions, feeding the output

527−of one computation into the input of the next. ``IO`` is an abstract

528−type, however, so we can’t access the result of a computation directly.

529−Instead, we sequence operations with ``do`` notation:

538+I/O programs will typically need to sequence actions, feeding the

539+output of one computation into the input of the next. ``IO`` is an

540+abstract type, however, so we can’t access the result of a computation

541+directly. Instead, we sequence operations with ``do`` notation:

530542

531543.. code-block:: idris

532544

@@ -538,16 +550,16 @@ Instead, we sequence operations with ``do`` notation:

538550The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of

539551type ``IO a``, and puts the result, of type ``a`` into the variable

540552``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``

541−has type ``String``. Indentation is significant — each statement in the

542−do block must begin in the same column. The ``return`` operation allows

543−us to inject a value directly into an IO operation:

553+has type ``String``. Indentation is significant — each statement in

554+the do block must begin in the same column. The ``return`` operation

555+allows us to inject a value directly into an IO operation:

544556

545557.. code-block:: idris

546558

547559 return : a -> IO a

548560

549−As we will see later, ``do`` notation is more general than this, and can

550−be overloaded.

561+As we will see later, ``do`` notation is more general than this, and

562+can be overloaded.

551563

552564.. _sect-lazy:

553565

@@ -564,11 +576,11 @@ not always the best approach. Consider the following function:

564576 boolCase True t e = t;

565577 boolCase False t e = e;

566578

567−This function uses one of the ``t`` or ``e`` arguments, but not both (in

568−fact, this is used to implement the ``if...then...else`` construct as we

569−will see later. We would prefer if *only* the argument which was used

570−was evaluated. To achieve this, ``Idris`` provides a ``Lazy`` data type,

571−which allows evaluation to be suspended:

579+This function uses one of the ``t`` or ``e`` arguments, but not both

580+(in fact, this is used to implement the ``if...then...else`` construct

581+as we will see later. We would prefer if *only* the argument which was

582+used was evaluated. To achieve this, ``Idris`` provides a ``Lazy``

583+data type, which allows evaluation to be suspended:

572584

573585.. code-block:: idris

574586

@@ -578,10 +590,10 @@ which allows evaluation to be suspended:

578590 Force : Lazy a -> a

579591

580592A value of type ``Lazy a`` is unevaluated until it is forced by

581−``Force``. The ``Idris`` type checker knows about the ``Lazy`` type, and

582−inserts conversions where necessary between ``Lazy a`` and ``a``, and

583−vice versa. We can therefore write ``boolCase`` as follows, without any

584−explicit use of ``Force`` or ``Delay``:

593+``Force``. The ``Idris`` type checker knows about the ``Lazy`` type,

594+and inserts conversions where necessary between ``Lazy a`` and ``a``,

595+and vice versa. We can therefore write ``boolCase`` as follows,

596+without any explicit use of ``Force`` or ``Delay``:

585597

586598.. code-block:: idris

587599

@@ -611,19 +623,19 @@ We have already seen the ``List`` and ``Vect`` data types:

611623 (::) : a -> Vect k a -> Vect (S k) a

612624

613625Note that the constructor names are the same for each — constructor

614−names (in fact, names in general) can be overloaded, provided that they

615−are declared in different namespaces (see Section :ref:`sect-namespaces`),

616−and will typically be resolved according to their type. As syntactic

617−sugar, any type with the constructor names ``Nil`` and ``::`` can be

618−written in list form. For example:

626+names (in fact, names in general) can be overloaded, provided that

627+they are declared in different namespaces (see Section

628+:ref:`sect-namespaces`), and will typically be resolved according to

629+their type. As syntactic sugar, any type with the constructor names

630+``Nil`` and ``::`` can be written in list form. For example:

619631

620632- ``[]`` means ``Nil``

621633

622634- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``

623635

624636The library also defines a number of functions for manipulating these

625−types. ``map`` is overloaded both for ``List`` and ``Vect`` and applies

626−a function to every element of the list or vector.

637+types. ``map`` is overloaded both for ``List`` and ``Vect`` and

638+applies a function to every element of the list or vector.

627639

628640.. code-block:: idris

629641

@@ -667,8 +679,8 @@ directory. For more details of the functions available on ``List`` and

667679- ``libs/base/Data/VectType.idr``

668680

669681Functions include filtering, appending, reversing, and so on. Also

670−remember that ``Idris`` is still in development, so if you don’t see the

671−function you need, please feel free to add it and submit a patch!

682+remember that ``Idris`` is still in development, so if you don’t see

683+the function you need, please feel free to add it and submit a patch!

672684

673685Aside: Anonymous functions and operator sections

674686~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -684,18 +696,18 @@ would be to use an anonymous function:

684696The notation ``\x => val`` constructs an anonymous function which takes

685697one argument, ``x`` and returns the expression ``val``. Anonymous

686698functions may take several arguments, separated by commas,

687−e.g. \ ``\x, y, z => val``. Arguments may also be given explicit types,

688−e.g. \ ``\x : Int => x * 2``, and can pattern match,

689−e.g. \ ``\(x, y) => x + y``. We could also use an operator section:

699+e.g. ``\x, y, z => val``. Arguments may also be given explicit types,

700+e.g. ``\x : Int => x * 2``, and can pattern match,

701+e.g. ``\(x, y) => x + y``. We could also use an operator section:

690702

691703::

692704

693705 *usefultypes> show (map (* 2) intVec)

694706 "[2, 4, 6, 8, 10]" : String

695707

696−``(*2)`` is shorthand for a function which multiplies a number by 2. It

697−expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand to

698−``\x => 2 * x``.

708+``(*2)`` is shorthand for a function which multiplies a number

709+by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand

710+to ``\x => 2 * x``.

699711

700712Maybe

701713~~~~~

@@ -707,9 +719,9 @@ given type, or there isn’t:

707719

708720 data Maybe a = Just a | Nothing

709721

710−``Maybe`` is one way of giving a type to an operation that may fail. For

711−example, looking something up in a ``List`` (rather than a vector) may

712−result in an out of bounds error:

722+``Maybe`` is one way of giving a type to an operation that may

723+fail. For example, looking something up in a ``List`` (rather than a

724+vector) may result in an out of bounds error:

713725

714726.. code-block:: idris

715727

@@ -740,9 +752,9 @@ Values can be paired with the following built-in data type:

740752

741753 data Pair a b = MkPair a b

742754

743−As syntactic sugar, we can write ``(a, b)`` which, according to context,

744−means either ``Pair a b`` or ``MkPair a b``. Tuples can contain an

745−arbitrary number of values, represented as nested pairs:

755+As syntactic sugar, we can write ``(a, b)`` which, according to

756+context, means either ``Pair a b`` or ``MkPair a b``. Tuples can

757+contain an arbitrary number of values, represented as nested pairs:

746758

747759.. code-block:: idris

748760

@@ -766,8 +778,8 @@ as “sigma types”:

766778

767779Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

768780of 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

770−a number with a ``Vect`` of a particular length.

781+``( a ** p )`` constructs a value of this type. For example, we can

782+pair a number with a ``Vect`` of a particular length.

771783

772784.. code-block:: idris

773785

@@ -783,27 +795,28 @@ equivalent.

783795 vec = MkSigma 2 [3, 4]

784796

785797The 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

787−of values which we expect the type checker to fill in, so the above

788−definition could also be written as:

798+from the length of the vector. We can write an underscore ``_`` in

799+place of values which we expect the type checker to fill in, so the

800+above definition could also be written as:

789801

790802.. code-block:: idris

791803

792804 vec : (n : Nat ** Vect n Int)

793805 vec = (_ ** [3, 4])

794806

795−We might also prefer to omit the type of the first element of the pair,

796−since, again, it can be inferred:

807+We might also prefer to omit the type of the first element of the

808+pair, since, again, it can be inferred:

797809

798810.. code-block:: idris

799811

800812 vec : (n ** Vect n Int)

801813 vec = (_ ** [3, 4])

802814

803−One use for dependent pairs is to return values of dependent types where

804−the index is not necessarily known in advance. For example, if we filter

805−elements out of a ``Vect`` according to some predicate, we will not know

806−in advance what the length of the resulting vector will be:

815+One use for dependent pairs is to return values of dependent types

816+where the index is not necessarily known in advance. For example, if

817+we filter elements out of a ``Vect`` according to some predicate, we

818+will not know in advance what the length of the resulting vector will

819+be:

807820

808821.. code-block:: idris

809822

@@ -815,9 +828,9 @@ If the ``Vect`` is empty, the result is easy:

815828

816829 filter p Nil = (_ ** [])

817830

818−In the ``::`` case, we need to inspect the result of a recursive call to

819−``filter`` to extract the length and the vector from the result. To do

820−this, we use ``with`` notation, which allows pattern matching on

831+In the ``::`` case, we need to inspect the result of a recursive call

832+to ``filter`` to extract the length and the vector from the result. To

833+do this, we use ``with`` notation, which allows pattern matching on

821834intermediate values:

822835

823836.. code-block:: idris

@@ -849,9 +862,9 @@ Intermediate values can be calculated using ``let`` bindings:

849862 splitAt c x = case break (== c) x of

850863 (x, y) => (x, strTail y)

851864

852−We can do simple pattern matching in ``let`` bindings too. For example,

853−we can extract fields from a record as follows, as well as by pattern

854−matching at the top level:

865+We can do simple pattern matching in ``let`` bindings too. For

866+example, we can extract fields from a record as follows, as well as by

867+pattern matching at the top level:

855868

856869.. code-block:: idris

857870

@@ -872,9 +885,9 @@ for building lists. The general form is:

872885 [ expression | qualifiers ]

873886

874887This generates the list of values produced by evaluating the

875−``expression``, according to the conditions given by the comma separated

876−``qualifiers``. For example, we can build a list of Pythagorean triples

877−as follows:

888+``expression``, according to the conditions given by the comma

889+separated ``qualifiers``. For example, we can build a list of

890+Pythagorean triples as follows:

878891

879892.. code-block:: idris

880893

@@ -884,16 +897,16 @@ as follows:

884897

885898The ``[a..b]`` notation is another shorthand which builds a list of

886899numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a

887−list of numbers between ``a`` and ``c`` with the increment specified by

888−the difference between ``a`` and ``b``. This works for any numeric type,

889−using the ``count`` function from the prelude.

900+list of numbers between ``a`` and ``c`` with the increment specified

901+by the difference between ``a`` and ``b``. This works for any numeric

902+type, using the ``count`` function from the prelude.

890903

891904``case`` expressions

892905~~~~~~~~~~~~~~~~~~~~

893906

894907Another way of inspecting intermediate values of *simple* types is to

895−use a ``case`` expression. The following function, for example, splits a

896−string into two at a given character:

908+use a ``case`` expression. The following function, for example, splits

909+a string into two at a given character:

897910

898911.. code-block:: idris

899912

@@ -907,10 +920,11 @@ deconstruct the pair it returns, and remove the first character of the

907920second string.

908921

909922A ``case`` expression can match several cases, for example, to inspect

910−an intermediate value of type ``Maybe a``. Recall ``list_lookup`` which

911−looks up an index in a list, returning ``Nothing`` if the index is out

912−of bounds. We can use this to write ``lookup_default``, which looks up

913−an index and returns a default value if the index is out of bounds:

923+an intermediate value of type ``Maybe a``. Recall ``list_lookup``

924+which looks up an index in a list, returning ``Nothing`` if the index

925+is out of bounds. We can use this to write ``lookup_default``, which

926+looks up an index and returns a default value if the index is out of

927+bounds:

914928

915929.. code-block:: idris

916930

@@ -919,8 +933,8 @@ an index and returns a default value if the index is out of bounds:

919933 Nothing => def

920934 Just x => x

921935

922−If the index is in bounds, we get the value at that index, otherwise we

923−get a default value:

936+If the index is in bounds, we get the value at that index, otherwise

937+we get a default value:

924938

925939::

926940

@@ -929,15 +943,15 @@ get a default value:

929943 *usefultypes> lookup_default 4 [3,4,5,6] (-1)

930944 -1 : Integer

931945

932−**Restrictions:** The ``case`` construct is intended for simple analysis

933−of intermediate expressions to avoid the need to write auxiliary

934−functions, and is also used internally to implement pattern matching

935−``let`` and lambda bindings. It will *only* work if:

946+**Restrictions:** The ``case`` construct is intended for simple

947+analysis of intermediate expressions to avoid the need to write

948+auxiliary functions, and is also used internally to implement pattern

949+matching ``let`` and lambda bindings. It will *only* work if:

936950

937951- Each branch *matches* a value of the same type, and *returns* a value

938952 of the same type.

939953

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

941955 can be determined *without* type checking the ``case``-expression

942956 itself.

943957

@@ -946,8 +960,8 @@ Dependent Records

946960

947961*Records* are data types which collect several values (the record’s

948962*fields*) together. ``Idris`` provides syntax for defining records and

949−automatically generating field access and update functions. For example,

950−we can represent a person’s name and age in a record:

963+*automatically generating field access and update functions. For

964+*example, we can represent a person’s name and age in a record:

951965

952966.. code-block:: idris

953967

@@ -958,10 +972,11 @@ we can represent a person’s name and age in a record:

958972 fred : Person

959973 fred = MkPerson "Fred" 30

960974

961−Record declarations are like ``data`` declarations, except that they are

962−introduced by the ``record`` keyword, and can only have one constructor.

963−The names of the binders in the constructor type (``name`` and ``age``)

964−here are the field names, which we can use to access the field values:

975+Record declarations are like ``data`` declarations, except that they

976+are introduced by the ``record`` keyword, and can only have one

977+constructor. The names of the binders in the constructor type

978+(``name`` and ``age``) here are the field names, which we can use to

979+access the field values:

965980

966981::

967982

@@ -972,8 +987,8 @@ here are the field names, which we can use to access the field values:

972987 *record> :t name

973988 name : Person -> String

974989

975−We can also use the field names to update a record (or, more precisely,

976−produce a new record with the given fields updated).

990+We can also use the field names to update a record (or, more

991+precisely, produce a new record with the given fields updated).

977992

978993.. code-block:: bash

979994

@@ -1024,9 +1039,9 @@ syntax:

10241039 record { a->b->c = val } x

10251040

10261041This 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.

1028−``record { a->b->c = val }`` itself has a function type. Symmetrically,

1029−the field can also be accessed with the following syntax:

1042+``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {

1043+a->b->c = val }`` itself has a function type. Symmetrically, the field

1044+can also be accessed with the following syntax:

10301045

10311046.. code-block:: idris

10321047

docs/tutorial/views.rst+22−22

@@ -8,9 +8,10 @@ Dependent pattern matching

88--------------------------

1010Since 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

12−the implicit length arguments to ``(++)``, we’d see that the form of the

13−length argument was determined by whether the vector was empty or not:

11+determined by the value of others. For example, if we were to write

12+down the implicit length arguments to ``(++)``, we’d see that the form

13+of the length argument was determined by whether the vector was empty

14+or not:

1415

1516.. code-block:: idris

1617

@@ -18,10 +19,8 @@ length argument was determined by whether the vector was empty or not:

1819 (++) {n=Z} [] ys = ys

1920 (++) {n=S k} (x :: xs) ys = x :: xs ++ ys

2021

21−If ``n`` was a successor in the ``[]`` case, or zero in the ``::`` case,

22−the definition would not be well typed.

23−

24−

22+If ``n`` was a successor in the ``[]`` case, or zero in the ``::``

23+case, the definition would not be well typed.

2524

2625.. _sect-nattobin:

2726

@@ -29,13 +28,13 @@ The ``with`` rule — matching intermediate values

2928------------------------------------------------

3029

3130Very often, we need to match on the result of an intermediate

32−computation. ``Idris`` provides a construct for this, the ``with`` rule,

33−inspired by views in ``Epigram`` [1]_, which takes account of

31+computation. ``Idris`` provides a construct for this, the ``with``

32+rule, inspired by views in ``Epigram`` [1]_, which takes account of

3433the fact that matching on a value in a dependently typed language can

3534affect what we know about the forms of other values. In its simplest

3635form, the ``with`` rule adds another argument to the function being

37−defined, e.g. we have already seen a vector filter function, defined as

38−follows:

36+defined, e.g. we have already seen a vector filter function, defined

37+as follows:

3938

4039.. code-block:: idris

4140

@@ -51,8 +50,8 @@ which we place after the vertical bar.

5150If the intermediate computation itself has a dependent type, then the

5251result can affect the forms of other arguments — we can learn the form

5352of 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.

55−Otherwise, it is the sum of two equal ``Nat``\ s plus one:

53+or odd. If it’s even it will be the sum of two equal ``Nat``.

54+Otherwise, it is the sum of two equal ``Nat`` plus one:

5655

5756.. code-block:: idris

5857

@@ -69,8 +68,9 @@ accordingly.

6968 parity : (n:Nat) -> Parity n

7069

7170We’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

73−digits (least significant first) as follows, using the ``with`` rule:

71+to write a function which converts a natural number to a list of

72+binary digits (least significant first) as follows, using the ``with``

73+rule:

7474

7575.. code-block:: idris

7676

@@ -81,13 +81,13 @@ digits (least significant first) as follows, using the ``with`` rule:

8181 natToBin (S (j + j)) | Odd = True :: natToBin j

8282

8383The 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

85−patterns for the result of the intermediate computation (``Even`` and

86−``odd``) right of the ``\mid``, we also write how the results affect the

87−other patterns left of the :math:`\mid`. Note that there is a function

88−in the patterns (``+``) and repeated occurrences of ``j``—this is

89−allowed because another argument has determined the form of these

90−patterns.

84+because the result of ``parity k`` depends on ``k``. So, as well as

85+the patterns for the result of the intermediate computation (``Even``

86+and ``odd``) right of the ``\mid``, we also write how the results

87+affect the other patterns left of the :math:`\mid`. Note that there is

88+a function in the patterns (``+``) and repeated occurrences of

89+``j``—this is allowed because another argument has determined the form

90+of these patterns.

9191

9292We will return to this function in Section :ref:`sect-provisional` to

9393complete the definition of ``parity``.