Introduction

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 [1]. 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 Int, 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 Int and 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.

Hello world

To give an idea of how programs with effects look, here is the ubiquitous “Hello world” program, written using the Effects library:

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. All 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 the 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!

Outline

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 Further Reading.

[1]You do not, however, need to know what a monad is!