83ff2b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2047 from jfdm/userdocs/package-creation

83ff2b6Jan de Muijnck-Hughes12 years ago

docs/effects/conclusions.rst+1−1

compare with master

unifiedsplit

@@ -5,7 +5,7 @@ Further Reading

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

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

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

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

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

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

11paper [1]_.

docs/effects/hangman.rst+1−1

@@ -264,7 +264,7 @@ generator, then pick a random ``Fin`` to index into a list of

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

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

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

269

270

docs/effects/introduction.rst+5−5

@@ -14,10 +14,10 @@ and supports programming and reasoning with side-effecting programs,

14supporting mutable state, interaction with the outside world,

15exceptions, and verified resource management.

17−This tutorial assumes familiarity with pure programming in ``Idris``,

17+This tutorial assumes familiarity with pure programming in Idris,

18as described in Sections 1–6 of the main tutorial [1]_. The examples

19−are presented are tested with ``Idris`` and can be found in the

19+are presented are tested with Idris and can be found in the

20−examples directory of the ``Idris`` repository.

20+examples directory of the Idris repository.

22Consider, for example, the following introductory function which

23illustrates the kind of properties which can be expressed in the type

@@ -47,7 +47,7 @@ able to apply the ``vadd`` function? Before doing so, we will have to:

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

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

50−tutorial, we will see how ``Idris`` supports side-effects.

50+tutorial, we will see how Idris supports side-effects.

51Furthermore, we will see how we can use the dependent type system to

52*reason* about stateful and side-effecting programs. We will return to

53this specific example later.

@@ -78,7 +78,7 @@ returns the unit value. All programs using the ``Effects`` library must

78``import Effects``. The details of the ``Eff`` type will be presented in the

79remainder of this tutorial.

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

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

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

83required for all examples in this tutorial):

docs/effects/simpleeff.rst+1−1

@@ -592,7 +592,7 @@ which ``eval`` can be ``run`` to those which support ``STDIO``, such

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

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

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

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

595+types are first class in Idris:

596

597.. code-block:: idris

598

docs/effects/state.rst+1−1

@@ -77,7 +77,7 @@ explicit.

77Introducing ``Effects``

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

80−``Idris`` provides a library, ``Effects`` [3]_, which captures this

80+Idris provides a library, ``Effects`` [3]_, which captures this

81pattern and many others involving effectful computation [1]_. An

82effectful program ``f`` has a type of the following form:

docs/index.rst+1

@@ -35,6 +35,7 @@ The Idris Tutorial

35 tutorial/typesfuns

36 tutorial/classes

37 tutorial/modules

38+ tutorial/packages

38 tutorial/interp

39 tutorial/interp

39 tutorial/views

40 tutorial/views

40 tutorial/theorems

41 tutorial/theorems

docs/reference/erasure.rst+4−4

@@ -94,11 +94,11 @@ cannot get below O(n) with time complexities.

94One could argue that Idris in fact compiles ``Nat`` via GMP but

95that's a moot point for two reasons:

97−* First, whenever we try to index our datastructures with anything

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.

98+ else than ``Nat``, the compiler is not going to come to the rescue.

100−* Second, even with ``Nat``, the GMP integers are *still* there and

100++ Second, even with ``Nat``, the GMP integers are *still* there and

101−they slow the runtime down.

101+ they slow the runtime down.

102

103This ought not to be the case since the ``Nat`` are never used at

104runtime and they are only there for typechecking purposes. Hence we

docs/tutorial/classes.rst+2−2

@@ -366,7 +366,7 @@ Rather than having to insert ``m_app`` everywhere there is an

366application, we can use to do the job for us. To do this, we can make

367``Maybe`` an instance of ``Applicative`` as follows, where ``<>`` is

368defined in the same way as ``m_app`` above (this is defined in the

369−``Idris`` library):

369+Idris library):

370

371.. code-block:: idris

372

@@ -481,7 +481,7 @@ Given the following list:

481 testList = [3,4,1]

482

483We can sort it using the default ``Ord`` instance, then the named

484−instance ``myord`` as follows, at the ``Idris`` prompt:

484+instance ``myord`` as follows, at the Idris prompt:

485

486::

487

docs/tutorial/conclusions.rst+4−4

@@ -4,10 +4,10 @@

4Further Reading

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

7−Further information about ``Idris`` programming, and programming with

7+Further information about Idris programming, and programming with

8dependent types in general, can be obtained from various sources:

10−- The ``Idris`` web site (http://idris-lang.org/) and by asking

10+- The Idris web site (http://idris-lang.org/) and by asking

11 questions on the mailing list.

13- The IRC channel ``#idris``, on

@@ -21,14 +21,14 @@ dependent types in general, can be obtained from various sources:

21 - https://github.com/idris-lang/Idris-dev/wiki/Language-Features

23- Examining the prelude and exploring the ``samples`` in the

24− distribution. The ``Idris`` source can be found online at:

24+ distribution. The Idris source can be found online at:

25 https://github.com/idris-lang/Idris-dev.

27- Existing projects on the ``Idris Hackers`` web space:

28 http://idris-hackers.github.io.

30- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly

31− describe older versions of ``Idris``.

31+ describe older versions of Idris.

33.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems

34 programming with embedded domain specific languages. In

docs/tutorial/index.rst+1

@@ -23,6 +23,7 @@ The is the Idris Tutorial. It will teach you about programming in the Idris Lang

23 typesfuns

24 classes

25 modules

26+ packages

26 interp

27 interp

27 views

28 views

28 theorems

29 theorems

docs/tutorial/interactive.rst+3−3

@@ -4,7 +4,7 @@

4Interactive Editing

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

7−By now, we have seen several examples of how ``Idris``’ dependent type

7+By now, we have seen several examples of how Idris’ dependent type

8system can give extra confidence in a function’s correctness by giving

9a more precise description of its intended behaviour in its *type*. We

10have also seen an example of how the type system can help with EDSL

@@ -13,7 +13,7 @@ object language. However, precise types give us more than verification

13of programs — we can also exploit types to help write programs which

14are *correct by construction*.

16−The ``Idris`` REPL provides several commands for inspecting and

16+The Idris REPL provides several commands for inspecting and

17modifying parts of programs, based on their types, such as case

18splitting on a pattern variable, inspecting the type of a

19metavariable, and even a basic proof search mechanism. In this

@@ -121,7 +121,7 @@ according to the same heuristic. If we update the file (using

121 vzipWith f [] [] = ?vzipWith_rhs_3

122

123That is, the pattern variable ``ys`` has been split into one case

124−``[]``, ``Idris`` having noticed that the other possible case ``y ::

124+``[]``, Idris having noticed that the other possible case ``y ::

125ys`` would lead to a unification error.

126

127:addmissing

docs/tutorial/interp.rst+6−6

@@ -22,7 +22,7 @@ booleans, and functions, represented by ``Ty``:

22 data Ty = TyInt | TyBool | TyFun Ty Ty

24We can write a function to translate these representations to a concrete

25−``Idris`` type — remember that types are first class, so can be

25+Idris type — remember that types are first class, so can be

26calculated just like any other value:

28.. code-block:: idris

@@ -176,7 +176,7 @@ environment:

176 else interp env e

177

178Given this, an interpreter (Listing :ref:`interpdef`) is a function which

179−translates an ``Expr`` into a concrete ``Idris`` value with respect to a

179+translates an ``Expr`` into a concrete Idris value with respect to a

180specific environment:

181

182.. code-block:: idris

@@ -199,7 +199,7 @@ value:

199Lambdas are more interesting. In this case, we construct a function

200which interprets the scope of the lambda with a new value in the

201environment. So, a function in the object language is translated to an

202−``Idris`` function:

202+Idris function:

203

204.. code-block:: idris

205

@@ -214,8 +214,8 @@ because of its type:

214 interp env (App f s) = interp env f (interp env s)

215

216Operators and interpreters are, again, direct translations into the

217−equivalent ``Idris`` constructs. For operators, we apply the function to

217+equivalent Idris constructs. For operators, we apply the function to

218−its operands directly, and for ``If``, we apply the ``Idris``

218+its operands directly, and for ``If``, we apply the Idris

219``if...then...else`` construct directly.

220

221.. code-block:: idris

@@ -263,7 +263,7 @@ function on user input:

263Here, ``cast`` is an overloaded function which converts a value from

264one type to another if possible. Here, it converts a string to an

265integer, giving 0 if the input is invalid. An example run of this

266−program at the ``Idris`` interactive environment is shown in Listing

266+program at the Idris interactive environment is shown in Listing

267:ref:`factrun`.

268

269

docs/tutorial/introduction.rst+4−4

@@ -35,10 +35,10 @@ following type to the ``app`` function, which concatenates vectors:

36 app : Vect n a -> Vect m a -> Vect (n + m) a

38−This tutorial introduces ``Idris``, a general purpose functional

38+This tutorial introduces Idris, a general purpose functional

39−programming language with dependent types. The goal of the ``Idris``

39+programming language with dependent types. The goal of the Idris

40project is to build a dependently typed language suitable for

41−verifiable *systems* programming. To this end, ``Idris`` is a compiled

41+verifiable *systems* programming. To this end, Idris is a compiled

42language which aims to generate efficient executable code. It also has

43a lightweight foreign function interface which allows easy interaction

44with external ``C`` libraries.

@@ -58,7 +58,7 @@ Example Code

58------------

60This tutorial includes some example code, which has been tested with

61−``Idris`` version . The files are available in the ``Idris``

61+Idris version . The files are available in the Idris

62distribution, and provided along side the tutorial source, so that you

63can try them out easily, under ``tutorial/examples``. However, it is

64strongly recommended that you can type them in yourself, rather than

docs/tutorial/miscellany.rst+17−17

@@ -48,7 +48,7 @@ this to happen silently. We define ``head`` as follows:

48 head : (xs : List a) -> {auto p : isCons xs = True} -> a

49 head (x :: xs) = x

51−The ``auto`` annotation on the implicit argument means that ``Idris``

51+The ``auto`` annotation on the implicit argument means that Idris

52will attempt to fill in the implicit argument using the ``trivial``

53tactic, which searches through the context for a proof, and tries to

54solve with ``refl`` if a proof is not found. Now when ``head`` is

@@ -72,7 +72,7 @@ to:

72Implicit conversions

73--------------------

75−``Idris`` supports the creation of *implicit conversions*, which allow

75+Idris supports the creation of *implicit conversions*, which allow

76automatic conversion of values from one type to another when required to

77make a term type correct. This is intended to increase convenience and

78reduce verbosity. A contrived but simple example is the following:

@@ -101,7 +101,7 @@ beyond the scope of this tutorial.

101Literate programming

102--------------------

103

104−Like Haskell, ``Idris`` supports *literate* programming. If a file has

104+Like Haskell, Idris supports *literate* programming. If a file has

105an extension of ``.lidr`` then it is assumed to be a literate file. In

106literate programs, everything is assumed to be a comment unless the line

107begins with a greater than sign ``>``, for example:

@@ -124,7 +124,7 @@ Foreign function calls

124

125For practical programming, it is often necessary to be able to use

126external libraries, particularly for interfacing with the operating

127−system, file system, networking, *et cetera*. ``Idris`` provides a

127+system, file system, networking, *et cetera*. Idris provides a

128lightweight foreign function interface for achieving this, as part of

129the prelude. For this, we assume a certain amount of knowledge of C and

130the ``gcc`` compiler. First, we define a datatype which describes the

@@ -136,7 +136,7 @@ external types we can handle:

136

137Each of these corresponds directly to a C type. Respectively: ``int``,

138``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a

139−translation to a concrete ``Idris`` type, described by the following

139+translation to a concrete Idris type, described by the following

140function:

141

142.. code-block:: idris

@@ -150,7 +150,7 @@ function:

150 interpFTy FUnit = ()

151

152A foreign function is described by a list of input types and a return

153−type, which can then be converted to an ``Idris`` type:

153+type, which can then be converted to an Idris type:

154

155.. code-block:: idris

156

@@ -170,7 +170,7 @@ A foreign function is assumed to be impure, so ``ForeignTy`` builds an

170We build a call to a foreign function by giving the name of the

171function, a list of argument types and the return type. The built in

172construct ``mkForeign`` converts this description to a function callable

173−by ``Idris``:

173+by Idris:

174

175.. code-block:: idris

176

@@ -194,7 +194,7 @@ Include and linker directives

194~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

195

196Foreign function calls are translated directly to calls to C functions,

197−with appropriate conversion between the ``Idris`` representation of a

197+with appropriate conversion between the Idris representation of a

198value and the C representation. Often this will require extra libraries

199to be linked in, or extra header and object files. This is made possible

200through the following directives:

@@ -303,7 +303,7 @@ are available in an external collection [1]_.

303C Target

304--------

305

306−The default target of ``Idris`` is C. Compiling via :

306+The default target of Idris is C. Compiling via :

307

308::

309

@@ -343,7 +343,7 @@ is shown below :

343JavaScript Target

344-----------------

345

346−``Idris`` is capable of producing *JavaScript* code that can be run in a

346+Idris is capable of producing *JavaScript* code that can be run in a

347browser as well as in the *NodeJS* environment or alike. One can use the

348FFI to communicate with the *JavaScript* ecosystem.

349

@@ -360,7 +360,7 @@ that is tailored for running in the browser issue the following command:

360The resulting file can be embedded into your HTML just like any other

361*JavaScript* code.

362

363−Generating code for *NodeJS* is slightly different. ``Idris`` outputs a

363+Generating code for *NodeJS* is slightly different. Idris outputs a

364*JavaScript* file that can be directly executed via ``node``.

365

366::

@@ -421,7 +421,7 @@ the way we use ``f`` in ``twice``, it would be more obvious if

421

422The *JavaScript* FFI is able to understand functions as arguments when

423you give it something of type ``FFunction``. The following example code

424−calls ``twice`` in *JavaScript* and returns the result to our ``Idris``

424+calls ``twice`` in *JavaScript* and returns the result to our Idris

425program:

426

427.. code-block:: idris

@@ -450,7 +450,7 @@ via FFI which are stored in external files. The *JavaScript* and

450mind that *JavaScript* and *NodeJS* are handled as different code

451generators, therefore you will have to state which one you want to

452target. This means that you can include different files for *JavaScript*

453−and *NodeJS* in the same ``Idris`` source file.

453+and *NodeJS* in the same Idris source file.

454

455So whenever you want to add an external *JavaScript* file you can do

456this like so:

@@ -488,13 +488,13 @@ This directive compiles into the following *JavaScript*

488Shrinking down generated *JavaScript*

489~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

490

491−``Idris`` can produce very big chunks of *JavaScript* code. However, the

491+Idris can produce very big chunks of *JavaScript* code. However, the

492generated code can be minified using the ``closure-compiler`` from

493Google. Any other minifier is also suitable but ``closure-compiler``

494offers advanced compilation that does some aggressive inlining and code

495−elimination. ``Idris`` can take full advantage of this compilation mode

495+elimination. Idris can take full advantage of this compilation mode

496and it’s highly recommended to use it when shipping a *JavaScript*

497−application written in ``Idris``.

497+application written in Idris.

498

499Cumulativity

500------------

@@ -509,7 +509,7 @@ types themselves have types. For example:

509 *universe> :t Vect

510 Vect : Nat -> Type -> Type

511

512−But what about the type of ``Type``? If we ask ``Idris`` it reports

512+But what about the type of ``Type``? If we ask Idris it reports

513

514::

515

docs/tutorial/modules.rst+2−2

@@ -4,7 +4,7 @@

4Modules and Namespaces

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

7−An ``Idris`` program consists of a collection of modules. Each module

7+An Idris program consists of a collection of modules. Each module

8includes an optional ``module`` declaration giving the name of the

9module, a list of ``import`` statements giving the other modules which

10are to be imported, and a collection of declarations and definitions of

@@ -76,7 +76,7 @@ Export Modifiers

77By default, all names defined in a module are exported for use by other

78modules. However, it is good practice only to export a minimal interface

79−and keep internal details abstract. ``Idris`` allows functions, types,

79+and keep internal details abstract. Idris allows functions, types,

80and classes to be marked as: ``public``, ``abstract`` or ``private``:

82- ``public`` means that both the name and definition are exported. For

docs/tutorial/packages.rstnew file+77

@@ -0,0 +1,77 @@

1+.. _sect-packages:

3+========

4+Packages

5+========

7+Idris includes a simple system for building packages from a

8+package description file. These files can be used with the Idris

9+compiler to manage the development process of your Idris

10+programmes and packages.

11+

12+Package Descriptions

13+--------------------

14+

15+A package description includes the following:

16+

17++ A header, consisting of the keyword package followed by the package name.

18++ Fields describing package contents, ``<field> = <value>``

19+

20+At least one field must be the modules field, where the value is a

21+comma separated list of modules. For example, a library test which

22+has two modules ``foo.idr`` and ``bar.idr`` as source files would be

23+written as follows::

24+

25+ package foo

26+

27+ modules = foo, bar

28+

29+Other examples of package files can be found in the ``libs`` directory

30+of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.

31+

32+Other common fields which may be present in an ``ipkg`` file are:

33+

34++ ``sourcedir = <dir>``, which gives the directory (relative to the

35+ current directory) which contains the source. Default is the current

36+ directory.

37+

38++ ``executable = <output>``, which gives the name of the executable

39+ file to generate.

40+

41++ ``main = <module>``, which gives the name of the main module, and

42+ must be present if the executable field is present.

43+

44++ ``opts = "<idris options>"``, which allows options (such as other

45+ packages) to be passed to Idris.

46+

47+In more advanced cases, particularly to support creating bindings to

48+external ``C`` libraries, the following options are available:

49+

50++ ``makefile = <file>``, which specifies a ``Makefile``, to be built

51+ before the Idris modules, for example to support linking with a

52+ ``C`` library.

53+

54++ ``libs = <libs>``, which gives a comma separated list of libraries

55+ which must be present for the package to be usable.

56+

57++ ``objs = <objs>``, which gives a comma separated list of additional

58+ object files to be installed, perhaps generated by the ``Makefile``.

59+

60+Using Package files

61+-------------------

62+

63+Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:

64+

65++ ``idris --build test.ipkg`` will build all modules in the package

66+

67++ ``idris --install test.ipkg`` will install the package, making it

68+ accessible by other Idris libraries and programs.

69+

70++ ``idris --clean test.ipkg`` will delete all intermediate code and

71+ executable files generated when building.

72+

73+Once the test package has been installed, the command line option

74+``--package test`` makes it accessible (abbreviated to ``-p test``).

75+For example::

76+

77+ idris -p test Main.idr

docs/tutorial/provisional.rst+4−4

@@ -71,9 +71,9 @@ Provisional definitions are written in the same way as ordinary

71definitions, except that they introduce the right hand side with a

72``?=`` rather than ``=``. We define ``parity`` as follows:

74−When written in this form, instead of reporting a type error, ``Idris``

74+When written in this form, instead of reporting a type error, Idris

75will insert a metavariable standing for a theorem which will correct the

76−type error. ``Idris`` tells us we have two proof obligations, with names

76+type error. Idris tells us we have two proof obligations, with names

77generated from the module and function names:

79.. code-block:: idris

@@ -161,14 +161,14 @@ reversed:

161Suspension of Disbelief

162-----------------------

163

164−``Idris`` requires that proofs be complete before compiling programs

164+Idris requires that proofs be complete before compiling programs

165(although evaluation at the prompt is possible without proof details).

166Sometimes, especially when prototyping, it is easier not to have to do

167this. It might even be beneficial to test programs before attempting to

168prove things about them — if testing finds an error, you know you had

169better not waste your time proving something!

170

171−Therefore, ``Idris`` provides a built-in coercion function, which allows

171+Therefore, Idris provides a built-in coercion function, which allows

172you to use a value of the incorrect types:

173

174.. code-block:: idris

docs/tutorial/starting.rst+5−5

@@ -7,7 +7,7 @@ Getting Started

7Prerequisites

8-------------

10−Before installing ``Idris``, you will need to make sure you have all

10+Before installing Idris, you will need to make sure you have all

11of the necessary libraries and tools. You will need:

13- A fairly recent Haskell platform. Version 2013.2.0.0 should be

@@ -20,7 +20,7 @@ of the necessary libraries and tools. You will need:

20Downloading and Installing

21--------------------------

23−The easiest way to install ``Idris``, if you have all of the

23+The easiest way to install Idris, if you have all of the

24prerequisites, is to type:

26::

@@ -33,7 +33,7 @@ development version you can find it, as well as build intructions, on

33GitHub at: https://github.com/idris-lang/Idris-dev.

35To check that installation has succeeded, and to write your first

36−``Idris`` program, create a file called “``hello.idr``” containing the

36+Idris program, create a file called “``hello.idr``” containing the

37following text:

39If you are familiar with Haskell, it should be fairly clear what the

@@ -48,11 +48,11 @@ create an executable called ``hello``, which you can run:

48 $ ./hello

49 Hello world

51−Note that the ``$`` indicates the shell prompt! Should the ``Idris``

51+Note that the ``$`` indicates the shell prompt! Should the Idris

52executable not be found please ensure that you have added

53``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X

54users may find they need to use ``~/Library/Haskell/bin``

55−instead. Some useful options to the ``Idris`` command are:

55+instead. Some useful options to the Idris command are:

57- ``-o prog`` to compile to an executable called ``prog``.

docs/tutorial/syntax.rst+1−1

@@ -122,7 +122,7 @@ hard to program this way in practice. Recall the factorial program in

122 (Val 1) (Op (*) (app fact (Op (-) (Var Stop) (Val 1)))

123 (Var Stop)))

124

125−Since this is a particularly useful pattern, ``Idris`` provides syntax

125+Since this is a particularly useful pattern, Idris provides syntax

126overloading [1]_ to make it easier to program in such object

127languages:

128

docs/tutorial/typesfuns.rst+28−28

@@ -7,13 +7,13 @@ Types and Functions

7Primitive Types

8---------------

10−``Idris`` defines several primitive types: ``Int``, ``Integer`` and

10+Idris defines several primitive types: ``Int``, ``Integer`` and

11``Float`` for numeric operations, ``Char`` and ``String`` for text

12manipulation, and ``Ptr`` which represents foreign pointers. There are

13also several data types declared in the library, including ``Bool``,

14with values ``True`` and ``False``. We can declare some constants with

15these types. Enter the following into a file ``prims.idr`` and load it

16−into the ``Idris`` interactive environment by typing ``idris

16+into the Idris interactive environment by typing ``idris

17prims.idr``:

19.. code-block:: idris

@@ -32,9 +32,9 @@ prims.idr``:

32 quux : Bool

33 quux = False

35−An ``Idris`` file consists of an optional module declaration (here

35+An Idris file consists of an optional module declaration (here

36``module prims``) followed by an optional list of imports (none here,

37−however ``Idris`` programs can consist of several modules, and the

37+however Idris programs can consist of several modules, and the

38definitions in each module each have their own namespace, as we will

39discuss in Section :ref:`sect-namespaces`) and a collection of

40declarations and definitions. The order of definitions is significant

@@ -46,7 +46,7 @@ declaration. Alternatively, declarations may be terminated with a

46semicolon.

48A library module ``prelude`` is automatically imported by every

49−``Idris`` program, including facilities for IO, arithmetic, data

49+Idris program, including facilities for IO, arithmetic, data

50structures and various common functions. The prelude defines several

51arithmetic and comparison operators, which we can use at the prompt.

52Evaluating things at the prompt gives an answer, and the type of the

@@ -108,7 +108,7 @@ Functions

108---------

109

110Functions are implemented by pattern matching, again using a similar

111−syntax to Haskell. The main difference is that ``Idris`` requires type

111+syntax to Haskell. The main difference is that Idris requires type

112declarations for all functions, using a single colon ``:`` (rather

113than Haskell’s double colon ``::``). Some natural number arithmetic

114functions can be defined as follows, again taken from the standard

@@ -133,7 +133,7 @@ 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

135all part of the same namespace. We can test these functions at the

136−``Idris`` prompt:

136+Idris prompt:

137

138::

139

@@ -144,10 +144,10 @@ all part of the same namespace. We can test these functions at the

144

145.. note::

146

147− ``Idris`` automatically desugars the ``Nat`` representation into a

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:

150+ checked at the Idris prompt:

151

152::

153

@@ -169,7 +169,7 @@ computers have perfectly good integer arithmetic built in. The reason

169is primarily that unary numbers have a very convenient structure which

170is easy to reason about, and easy to relate to other data structures

171as we will see later. Nevertheless, we do not want this convenience to

172−be at the expense of efficiency. Fortunately, ``Idris`` knows about

172+be at the expense of efficiency. Fortunately, Idris knows about

173the relationship between ``Nat`` (and similarly structured types) and

174numbers. This means it can optimise the representation, and functions

175such as ``plus`` and ``mult``.

@@ -248,7 +248,7 @@ Vectors

248

249A standard example of a dependent type is the type of “lists with

250length”, conventionally called vectors in the dependent type

251−literature. They are available as part of the ``Idris`` library, by

251+literature. They are available as part of the Idris library, by

252importing ``Data.Vect``, or we can declare them as follows:

253

254.. code-block:: idris

@@ -258,7 +258,7 @@ importing ``Data.Vect``, or we can declare them as follows:

258 (::) : a -> Vect k a -> Vect (S k) a

259

260Note that we have used the same constructor names as for ``List``.

261−Ad-hoc name overloading such as this is accepted by ``Idris``,

261+Ad-hoc name overloading such as this is accepted by Idris,

262provided that the names are declared in different namespaces (in

263practice, normally in different modules). Ambiguous constructor names

264can normally be resolved from context.

@@ -289,7 +289,7 @@ defined as follows, appends two ``Vect``:

289

290The type of ``(++)`` states that the resulting vector’s length will be

291the sum of the input lengths. If we get the definition wrong in such a

292−way that this does not hold, ``Idris`` will not accept the definition.

292+way that this does not hold, Idris will not accept the definition.

293For example:

294

295.. code-block:: idris

@@ -298,7 +298,7 @@ For example:

298 (++) Nil ys = ys

299 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

300

301−When run through the ``Idris`` type checker, this results in the

301+When run through the Idris type checker, this results in the

302following:

303

304::

@@ -325,7 +325,7 @@ The Finite Sets

325~~~~~~~~~~~~~~~

326

327Finite sets, as the name suggests, are sets with a finite number of

328−elements. They are available as part of the ``Idris`` library, by

328+elements. They are available as part of the Idris library, by

329importing ``Data.Fin``, or can be declared as follows:

330

331.. code-block:: idris

@@ -480,9 +480,9 @@ I/O

480

481Computer programs are of little use if they do not interact with the

482user or the system in some way. The difficulty in a pure language such

483−as ``Idris`` — that is, a language where expressions do not have

483+as Idris — that is, a language where expressions do not have

484side-effects — is that I/O is inherently side-effecting. Therefore in

485−``Idris``, such interactions are encapsulated in the type ``IO``:

485+Idris, such interactions are encapsulated in the type ``IO``:

486

487.. code-block:: idris

488

@@ -567,7 +567,7 @@ Laziness

567--------

568

569Normally, arguments to functions are evaluated before the function

570−itself (that is, ``Idris`` uses *eager* evaluation). However, this is

570+itself (that is, Idris uses *eager* evaluation). However, this is

571not always the best approach. Consider the following function:

572

573.. code-block:: idris

@@ -579,7 +579,7 @@ not always the best approach. Consider the following function:

579This 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

581as we will see later. We would prefer if *only* the argument which was

582−used was evaluated. To achieve this, ``Idris`` provides a ``Lazy``

582+used was evaluated. To achieve this, Idris provides a ``Lazy``

583data type, which allows evaluation to be suspended:

584

585.. code-block:: idris

@@ -590,7 +590,7 @@ data type, which allows evaluation to be suspended:

590 Force : Lazy a -> a

591

592A value of type ``Lazy a`` is unevaluated until it is forced by

593−``Force``. The ``Idris`` type checker knows about the ``Lazy`` type,

593+``Force``. The Idris type checker knows about the ``Lazy`` type,

594and inserts conversions where necessary between ``Lazy a`` and ``a``,

595and vice versa. We can therefore write ``boolCase`` as follows,

596without any explicit use of ``Force`` or ``Delay``:

@@ -604,10 +604,10 @@ without any explicit use of ``Force`` or ``Delay``:

604Useful Data Types

605-----------------

606

607−``Idris`` includes a number of useful data types and library functions

607+Idris includes a number of useful data types and library functions

608(see the ``libs/`` directory in the distribution). This chapter

609describes a few of these. The functions described here are imported

610−automatically by every ``Idris`` program, as part of ``Prelude.idr``.

610+automatically by every Idris program, as part of ``Prelude.idr``.

611

612``List`` and ``Vect``

613~~~~~~~~~~~~~~~~~~~~~

@@ -679,7 +679,7 @@ directory. For more details of the functions available on ``List`` and

679- ``libs/base/Data/VectType.idr``

680

681Functions include filtering, appending, reversing, and so on. Also

682−remember that ``Idris`` is still in development, so if you don’t see

682+remember that Idris is still in development, so if you don’t see

683the function you need, please feel free to add it and submit a patch!

684

685Aside: Anonymous functions and operator sections

@@ -877,7 +877,7 @@ pattern matching at the top level:

877List comprehensions

878~~~~~~~~~~~~~~~~~~~

879

880−``Idris`` provides *comprehension* notation as a convenient shorthand

880+Idris provides *comprehension* notation as a convenient shorthand

881for building lists. The general form is:

882

883::

@@ -958,10 +958,10 @@ matching ``let`` and lambda bindings. It will *only* work if:

958Dependent Records

959-----------------

960

961−*Records* are data types which collect several values (the record’s

961+*Records* are data types which collect several values (the record's

962−*fields*) together. ``Idris`` provides syntax for defining records and

962+*fields*) together. Idris provides syntax for defining records and

963*automatically generating field access and update functions. For

964−*example, we can represent a person’s name and age in a record:

964+*example, we can represent a person's name and age in a record:

965

966.. code-block:: idris

967

@@ -1029,7 +1029,7 @@ length because it will not affect the type of the record:

1029Nested record update

1030~~~~~~~~~~~~~~~~~~~~

1031

1032−``Idris`` also provides a convenient syntax for accessing and updating

1032+Idris also provides a convenient syntax for accessing and updating

1033nested records. For example, if a field is accessible with the

1034expression ``c (b (a x))``, it can be updated using the following

1035syntax:

docs/tutorial/views.rst+1−1

@@ -28,7 +28,7 @@ The ``with`` rule — matching intermediate values

28------------------------------------------------

30Very often, we need to match on the result of an intermediate

31−computation. ``Idris`` provides a construct for this, the ``with``

31+computation. Idris provides a construct for this, the ``with``

32rule, inspired by views in ``Epigram`` [1]_, which takes account of

33the fact that matching on a value in a dependently typed language can

34affect what we know about the forms of other values. In its simplest