git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/docs/effects/introduction.rst
109 lines 4.4 kB history raw
1************
2Introduction
3************
5Pure functional languages with dependent types such as `Idris
6<http://www.idris-lang.org/>`_ support reasoning about programs directly
7in the type system, promising that we can *know* a program will run
8correctly (i.e. according to the specification in its type) simply
9because it compiles. Realistically, though, things are not so simple:
10programs have to interact with the outside world, with user input,
11input from a network, mutable state, and so on. In this tutorial I
12will introduce the library, which is included with the distribution
13and supports programming and reasoning with side-effecting programs,
14supporting mutable state, interaction with the outside world,
15exceptions, and verified resource management.
17This tutorial assumes familiarity with pure programming in Idris,
18as described in Sections 1–6 of the main tutorial [1]_. The examples
19presented are tested with Idris and can be found in the
20examples 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
24system:
26.. code-block:: idris
28 vadd : Vect n Int -> Vect n Int -> Vect n Int
29 vadd [] [] = []
30 vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
32This function adds corresponding elements in a pair of vectors. The type
33guarantees that the vectors will contain only elements of type ``Int``,
34and that the input lengths and the output length all correspond. A
35natural question to ask here, which is typically neglected by
36introductory tutorials, is “How do I turn this into a program?” That is,
37given some lists entered by a user, how do we get into a position to be
38able to apply the ``vadd`` function? Before doing so, we will have to:
40- Read user input, either from the keyboard, a file, or some other input device.
42- Check that the user inputs are valid, i.e. contain only ``Int`` and are the same length, and report an error if not.
44- Write output
46The complete program will include side-effects for I/O and error
47handling, before we can get to the pure core functionality. In this
48tutorial, we will see how Idris supports side-effects.
49Furthermore, we will see how we can use the dependent type system to
50*reason* about stateful and side-effecting programs. We will return to
51this specific example later.
53Hello world
54===========
56To give an idea of how programs with effects look, here is the
57ubiquitous “Hello world” program, written using the ``Effects``
58library:
60.. code-block:: idris
62 module Main
64 import Effects
65 import Effect.StdIO
67 hello : Eff () [STDIO]
68 hello = putStrLn "Hello world!"
70 main : IO ()
71 main = run hello
73As usual, the entry point is ``main``. All ``main`` has to do is invoke the
74``hello`` function which supports the ``STDIO`` effect for console I/O, and
75returns the unit value. All programs using the ``Effects`` library must
76``import Effects``. The details of the ``Eff`` type will be presented in the
77remainder of this tutorial.
79To compile and run this program, Idris needs to be told to include
80the ``Effects`` package, using the ``-p effects`` flag (this flag is
81required for all examples in this tutorial):
83.. code-block:: sh
85 idris hello.idr -o hello -p effects
86 ./hello Hello world!
88Outline
89=======
91The tutorial is structured as follows: first, in Section
92:ref:`sect-state`, we will discuss state management, describing why it
93is important and introducing the ``effects`` library to show how it
94can be used to manage state. This section also gives an overview of
95the syntax of effectful programs. Section :ref:`sect-simpleff` then
96introduces a number of other effects a program may have: I/O;
97Exceptions; Random Numbers; and Non-determinism, giving examples for
98each, and an extended example combining several effects in one
99complete program. Section :ref:`sect-depeff` introduces *dependent*
100effects, showing how states and resources can be managed in
101types. Section :ref:`sect-impleff` shows how new effects can be
102implemented. Section :ref:`sect-hangman` gives an extended example
103showing how to implement a “mystery word” guessing game, using effects
104to describe the rules of the game and ensure they are implemented
105accurately. References to further reading are given in Section
106:ref:`sect-further`.
108.. [1]
109 You do not, however, need to know what a monad is!