IOSpec: a pure specification of the IO monad

IOSpec is a library containing a pure specification of several functions in the IO monad. You can use these specifications to test, debug, and reason about impure code.

Introduction

To get a taste of what you can do, consider an implementation of an 'imperative' queue that uses pointers to build a linked list:


import Test.IOSpec

data Queue = Queue {front :: IORef Cell, back :: IORef Cell}  

data Cell = Cell Int (IORef Cell) | NULL

emptyQueue :: IOSpec IORefS Queue
enqueue :: Queue -> Int -> IOSpec IORefS () ()
dequeue :: Queue -> IOSpec IORefS (Maybe Int)

Values of type IOSpec IORefS a correspond to computations that use IORefs, but no other parts of the IO monad, and return a value of type a. By convention, a trailing 'S' is used to denote a specification. For example, values of type IOSpec MVarS a correspond to IO computations using just MVars.

These specifications are pure functions, running on a pure Virtual Machine, that behave the same as their IO counterparts. Using tools such as QuickCheck and the GHCi debugger we can test and debug our implementation of queues as if it was pure. For example, we may want to check that the following property holds:


fifoProp :: [Int] -> Bool
fifoProp xs = evalIOSpec enqDeq singleThreaded == Done xs
  where
  enqDeq :: IOSpec IORefS [Int]
  enqDeq = do
    q <- emptyQueue
    forM_ xs (enqueue q)
    unfoldM dequeue q

That is, starting from an empty queue, enqueuing and subsequently dequeuing any list of integers should return the original list. Note that this property does not require unsafePerformIO or any such hacks: the evalIOSpec function is entirely pure. It is parameterized by the scheduler, allowing you to test your code with different scheduling algorithms to maximize code coverage. Once we are satisfied with our implementation, we can import Data.IORef and use real IORefs, instead of the pure specification provided by IOSpec.

The IOSpec library is not restricted to IORefs. There are also pure specifications of concurrency, STM, and teletype primitives. These specifications can be combined as you see fit: you can define your own IOSpec monad à la carte. For example, when writing concurrent code you may want use just MVars and forkIO:

 type Concurrent a = IOSpec (MVarS :+: ForkS) a

Functions of type Concurrent a may use IO functions such as newEmptyMVar or forkIO. But using putStr in the Concurrent monad, for example, will cause a type error. You may want to browse the API to get a better idea of how the library is organized.

Haskell's careful treatment of IO shows how being precise about effects can help you write more reliable code. I'd like to think that the IOSpec library takes some of these ideas one step further.

Download

A tarball containing the sources is available.

Alternatively, you may want to check out the following darcs repository:

  darcs get http://www.cs.nott.ac.uk/~wss/repos/IOSpec

Installation

You need to install IOSpec using Cabal. Essentially, you need to download the sources and issue the following commands:

runhaskell Setup.lhs configure
runhaskell Setup.lhs build
runhaskell Setup.lhs install

If you want to customize the installation process, you may want to read more about installing packages using Cabal.

Documentation

Browse the Haddock-ed source code.

The examples directory that comes with the sources contains several well-documented examples.

The ideas underlying the implementation are described in the following papers:

Beauty in the Beast: A Functional Semantics for the Awkward Squad. Haskell Workshop 2007.
Data types à la carte. Accepted for publication in JFP.

Feedback

If you have any comments or suggestions, please don't hesitate to get in touch!

Wouter Swierstra