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