Pure functional languages with dependent types such as Idris support reasoning about programs directly in the type system, promising that we can know a program will run correctly (i.e. according to the specification in its type) simply because it compiles. Realistically, though, things are not so simple: programs have to interact with the outside world, with user input, input from a network, mutable state, and so on. In this tutorial I will introduce the library, which is included with the distribution and supports programming and reasoning with side-effecting programs, supporting mutable state, interaction with the outside world, exceptions, and verified resource management.
This tutorial assumes familiarity with pure programming in Idris, as described in Sections 1–6 of the main tutorial . The examples presented are tested with Idris and can be found in the examples directory of the Idris repository.
Consider, for example, the following introductory function which illustrates the kind of properties which can be expressed in the type system:
vadd : Vect n Int -> Vect n Int -> Vect n Int vadd   =  vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
This function adds corresponding elements in a pair of vectors. The type
guarantees that the vectors will contain only elements of type
and that the input lengths and the output length all correspond. A
natural question to ask here, which is typically neglected by
introductory tutorials, is “How do I turn this into a program?” That is,
given some lists entered by a user, how do we get into a position to be
able to apply the
vadd function? Before doing so, we will have to:
- Read user input, either from the keyboard, a file, or some other input device.
- Check that the user inputs are valid, i.e. contain only
Intand are the same length, and report an error if not.
- Write output
The complete program will include side-effects for I/O and error handling, before we can get to the pure core functionality. In this tutorial, we will see how Idris supports side-effects. Furthermore, we will see how we can use the dependent type system to reason about stateful and side-effecting programs. We will return to this specific example later.
To give an idea of how programs with effects look, here is the
ubiquitous “Hello world” program, written using the
module Main import Effects import Effect.StdIO hello : Eff () [STDIO] hello = putStrLn “Hello world!” main : IO () main = run hello
As usual, the entry point is
main has to do is invoke the
hello function which supports the
STDIO effect for console I/O, and
returns the unit value. All programs using the
Effects library must
import Effects. The details of the
Eff type will be presented in the
remainder of this tutorial.
To compile and run this program, Idris needs to be told to include
Effects package, using the
-p effects flag (this flag is
required for all examples in this tutorial):
idris hello.idr -o hello -p effects ./hello Hello world!
The tutorial is structured as follows: first, in Section
State, we will discuss state management, describing why it
is important and introducing the
effects library to show how it
can be used to manage state. This section also gives an overview of
the syntax of effectful programs. Section Simple Effects then
introduces a number of other effects a program may have: I/O;
Exceptions; Random Numbers; and Non-determinism, giving examples for
each, and an extended example combining several effects in one
complete program. Section Dependent Effects introduces dependent
effects, showing how states and resources can be managed in
types. Section Creating New Effects shows how new effects can be
implemented. Section Example: A “Mystery Word” Guessing Game gives an extended example
showing how to implement a “mystery word” guessing game, using effects
to describe the rules of the game and ensure they are implemented
accurately. References to further reading are given in Section
|||You do not, however, need to know what a monad is!|