@@ -14,9 +14,10 @@ supports programming and reasoning with side-effecting programs,
1414supporting mutable state, interaction with the outside world,
1515exceptions, and verified resource management.
1616
17−This tutorial assumes familiarity with pure programming in , as
18−described in Sections 1–6 of the main tutorial [1]_. The examples are
19−tested with version .
17+This tutorial assumes familiarity with pure programming in ``Idris``,
18+as 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
20+examples directory of the ``Idris`` repository.
2021
2122Consider, for example, the following introductory function which
2223illustrates the kind of properties which can be expressed in the type
@@ -46,16 +47,16 @@ able to apply the ``vadd`` function? Before doing so, we will have to:
4647
4748The complete program will include side-effects for I/O and error
4849handling, before we can get to the pure core functionality. In this
49−tutorial, we will see how supports side-effects. Furthermore, we will
50−see how we can use the dependent type system to *reason* about stateful
51−and side-effecting programs. We will return to this specific example
52−later.
50+tutorial, we will see how ``Idris`` supports side-effects.
51+Furthermore, we will see how we can use the dependent type system to
52+*reason* about stateful and side-effecting programs. We will return to
53+this specific example later.
5354
5455Hello world
5556===========
5657
5758To give an idea of how programs with effects look in , here is the
58−ubiquitous “Hello world” program, written using the library:
59+ubiquitous “Hello world” program, written using the ``Effects`` library:
5960
6061.. code-block:: idris
6162
@@ -74,8 +75,8 @@ the ``hello`` function which supports the ``STDIO`` effect for console
7475I/O, and returns the unit value. The details of the ``Eff`` type will be
7576presented in the remainder of this tutorial.
7677
77−To compile and run this program, needs to be told to include the
78−package, using the ``-p`` flag (this flag is required for all examples
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
7980in this tutorial):
8081
8182.. code-block:: sh
@@ -86,20 +87,21 @@ in this tutorial):
8687Outline
8788=======
8889
89−The tutorial is structured as follows: first, in :ref:`sect-state`,
90−we will discuss state management, describing why it is important and
91−introducing the library to show how it can be used to manage state. This
92−section also gives an overview of the syntax of effectful programs.
93−:ref:`sect-simpleff` then introduces a number of other effects a
94−program may have: I/O; Exceptions; Random Numbers; and Non-determinism,
95−giving examples for each, and an extended example combining several
96−effects in one complete program. :ref:`sect-depeff` introduces
97−*dependent* effects, showing how states and resources can be managed in
98−types. :ref:`sect-impleff` shows how new effects can be implemented.
99−:ref:`sect-hangman` gives an extended example showing how to
100−implement a “mystery word” guessing game, using effects to describe the
101−rules of the game and ensure they are implemented accurately. References
102−to further reading are given in :ref:`sect-further`.
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
104+:ref:`sect-further`.
103105
104106.. [1]
105107 You do not, however, need to know what a monad is. A correctness