diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2018 Andrey Mokhov
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,23 @@
+# Build Systems à la Carte
+
+[![Linux & OS X status](https://img.shields.io/travis/snowleopard/build/master.svg?label=Linux%20%26%20OS%20X)](https://travis-ci.org/snowleopard/build) [![Windows status](https://img.shields.io/appveyor/ci/snowleopard/build/master.svg?label=Windows)](https://ci.appveyor.com/project/snowleopard/build)
+
+This project provides an executable framework for developing and comparing build systems, viewing them as related points in landscape rather than as isolated phenomena. The code derives from the ICFP 2018 paper ["Build Systems à la Carte"](https://github.com/snowleopard/build-systems/releases/download/icfp-submission/build-systems.pdf).
+
+## Getting Started
+
+To install from a Docker image do _TODO: Insert instuctions here_. After that you should have a copy of GHC and a standard Cabal project.
+
+You may be interested to:
+
+* Run `cabal test` to execute all the provided build systems on a very simple example.
+* Run `cabal haddock` to generate HTML documentation of all the interfaces.
+* Read the code, particularly [System.hs](src/Build/System.hs) which is the concrete implementation of all build systems. Following the imports (or the Haddock documentation) will lead you to all the consistuent parts.
+
+## Further Activities
+
+There aren't really any. The code served as a proving ground for ideas, and it's existence both allows confirmation that our conclusions are valid, and opportunity to cheaply conduct further experiments. However, the code is a useful adjoint to the paper, it is not essential to it (other than we wouldn't have been able to discover what we did without an executable specification).
+
+## Background Information
+
+The task abstraction is explored more completely in [this blog post](https://blogs.ncl.ac.uk/andreymokhov/the-task-abstraction/), and the motivation behind the project in [an earlier blog post](https://blogs.ncl.ac.uk/andreymokhov/cloud-and-dynamic-builds/).
diff --git a/build.cabal b/build.cabal
new file mode 100644
--- /dev/null
+++ b/build.cabal
@@ -0,0 +1,75 @@
+name:                build
+version:             0.0.1
+synopsis:            Build systems a la carte
+homepage:            https://github.com/snowleopard/build
+license:             MIT
+license-file:        LICENSE
+author:              Andrey Mokhov, Neil Mitchell, Simon Peyton Jones
+maintainer:          Andrey Mokhov <andrey.mokhov@gmail.com>, github: @snowleopard
+copyright:           Andrey Mokhov, Neil Mitchell, Simon Peyton Jones, 2018
+category:            Algorithms, Data Structures
+build-type:          Simple
+extra-source-files:  README.md
+description:         A library for experimenting with build systems and
+                     incremental computation frameworks, based on the ideas
+                     presented in the ICFP 2018 paper "Build systems a la carte".
+cabal-version:       >=1.10
+
+source-repository head
+  type:     git
+  location: https://github.com/snowleopard/build
+
+library
+  hs-source-dirs:       src
+  exposed-modules:      Build,
+                        Build.Multi,
+                        Build.Rebuilder,
+                        Build.SelfTracking,
+                        Build.Scheduler,
+                        Build.Store,
+                        Build.Task,
+                        Build.Task.Applicative,
+                        Build.Task.Depend,
+                        Build.Task.Functor,
+                        Build.Task.Monad,
+                        Build.Task.MonadPlus,
+                        Build.Task.Typed,
+                        Build.Task.Wrapped,
+                        Build.Trace,
+                        Build.System
+  other-modules:        Build.Utilities
+  build-depends:        algebraic-graphs >= 0.1.1,
+                        base             >= 4.7 && < 5,
+                        containers       >= 0.5.7.1,
+                        extra            >= 1.5.3,
+                        filepath         >= 1.4.1.0,
+                        mtl              >= 2.2.1,
+                        random           >= 1.1,
+                        transformers     >= 0.5.2.0
+  default-language:     Haskell2010
+  GHC-options:          -Wall
+                        -fno-warn-name-shadowing
+                        -Wcompat
+                        -Wincomplete-record-updates
+                        -Wincomplete-uni-patterns
+                        -Wredundant-constraints
+
+test-suite test
+    hs-source-dirs:     test
+    type:               exitcode-stdio-1.0
+    main-is:            Main.hs
+    other-modules:      Examples
+                        Spreadsheet
+    build-depends:      build,
+                        base         >= 4.7     && < 5,
+                        extra        >= 1.5.3,
+                        containers   >= 0.5.7.1,
+                        mtl          >= 2.2.1,
+                        transformers >= 0.5.2.0
+    default-language:   Haskell2010
+    GHC-options:        -Wall
+                        -fno-warn-name-shadowing
+                        -Wcompat
+                        -Wincomplete-record-updates
+                        -Wincomplete-uni-patterns
+                        -Wredundant-constraints
diff --git a/src/Build.hs b/src/Build.hs
new file mode 100644
--- /dev/null
+++ b/src/Build.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE ConstraintKinds, RankNTypes, TypeApplications #-}
+
+-- | Build systems and the properties they should ensure.
+module Build (
+    -- * Build
+    Build,
+
+    -- * Properties
+    correct, correctBuild, idempotent
+    ) where
+
+import Build.Task
+import Build.Task.Monad
+import Build.Task.Wrapped
+import Build.Store
+import Build.Utilities
+
+-- | A build system takes a description of 'Tasks', a target key, and a store,
+-- and computes a new store, where the key and its dependencies are up to date.
+type Build c i k v = Tasks c k v -> k -> Store i k v -> Store i k v
+
+-- | Given a description of @tasks@, an initial @store@, and a @result@ produced
+-- by running a build system on a target @key@, this function returns 'True' if
+-- the @result@ is a correct build outcome. Specifically:
+-- * @result@ and @store@ must agree on the values of all inputs. In other words,
+--   no inputs were corrupted during the build.
+-- * @result@ is /consistent/ with the @tasks@, i.e. for every non-input key,
+--   the result of recomputing its task matches the value stored in the @result@.
+correctBuild :: (Ord k, Eq v) => Tasks Monad k v -> Store i k v -> Store i k v -> k -> Bool
+correctBuild tasks store result = all correct . reachable deps
+  where
+    deps = maybe [] (\t -> snd $ track (unwrap @Monad t) (flip getValue result)) . tasks
+    correct k = case tasks k of
+        Nothing -> getValue k result == getValue k store
+        Just t  -> getValue k result == compute (unwrap @Monad t) (flip getValue result)
+
+-- | Given a @build@ and @tasks@, check that @build@ produces a correct result
+-- for any initial store and a target key.
+correct :: (Ord k, Eq v) => Build Monad i k v -> Tasks Monad k v -> Bool
+correct build tasks = forall $ \(key, store) ->
+    correctBuild tasks store (build tasks key store) key
+
+-- | Check that a build system is /idempotent/, i.e. running it once or twice in
+-- a row leads to the same resulting 'Store'.
+idempotent :: Eq v => Build Monad i k v -> Tasks Monad k v -> Bool
+idempotent build tasks = forall $ \(key, store1) ->
+    let store2 = build tasks key store1
+        store3 = build tasks key store2
+    in forall $ \k -> getValue k store2 == getValue k store3
diff --git a/src/Build/Multi.hs b/src/Build/Multi.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Multi.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE RankNTypes #-}
+
+-- | Given a build system that can work with single keys, generalise that to one
+-- that deals with multiple keys at a time.
+module Build.Multi (multi) where
+
+import Data.Maybe
+import Build.Task
+
+-- | Defines a set partition. For a function to be a valid partition,
+--   if @f k == ks@, then:
+--
+-- * @k \in ks@
+--
+-- * @forall i \in ks . f i == ks@
+type Partition k = k -> [k]
+
+-- | Given a build rule where you can build some combinations of multiple rules,
+-- use a partition to enable building lots of multiple rule subsets.
+multi :: Eq k => Partition k -> Tasks Applicative [k] [v] -> Tasks Applicative [k] [v]
+multi partition tasks keys
+    | k:_ <- keys, partition k == keys = tasks keys
+    | otherwise = Just $ \fetch ->
+        sequenceA [ select k <$> fetch (partition k) | k <- keys ]
+  where
+    select k = fromMaybe (error msg) . lookup k . zip (partition k)
+    msg = "Partition invariants violated"
diff --git a/src/Build/Rebuilder.hs b/src/Build/Rebuilder.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Rebuilder.hs
@@ -0,0 +1,118 @@
+{-# LANGUAGE ConstraintKinds, RankNTypes, TupleSections #-}
+
+-- | Rebuilders take care of deciding whether a key needs to be rebuild and
+-- running the corresponding task if need be.
+module Build.Rebuilder (
+    Rebuilder, perpetualRebuilder,
+    modTimeRebuilder, Time, MakeInfo,
+    approximationRebuilder, DependencyApproximation (..), ApproximationInfo,
+    vtRebuilder, stRebuilder, ctRebuilder, dctRebuilder
+    ) where
+
+import Control.Monad.State
+import Data.Map (Map)
+
+import qualified Data.Map as Map
+
+import Build.Store
+import Build.Task
+import Build.Task.Applicative
+import Build.Task.Monad
+import Build.Trace
+
+-- | Given a key-value pair and the corresponding task, a rebuilder returns a
+-- new task that has access to the build information and can use it to skip
+-- rebuilding a key if it is up to date.
+type Rebuilder c i k v = k -> v -> Task c k v -> Task (MonadState i) k v
+
+-- | Always rebuilds the key.
+perpetualRebuilder :: Rebuilder Monad () k v
+perpetualRebuilder _key _value task = task
+
+------------------------------------- Make -------------------------------------
+type Time = Integer
+type MakeInfo k = (Map k Time, Time)
+
+-- | This rebuilder uses modification time to decide whether a key is dirty and
+-- needs to be rebuilt. Used by Make.
+modTimeRebuilder :: Ord k => Rebuilder Applicative (MakeInfo k) k v
+modTimeRebuilder key value task fetch = do
+    (modTime, now) <- get
+    let dirty = case Map.lookup key modTime of
+            Nothing -> True
+            time -> any (\d -> Map.lookup d modTime > time) (dependencies task)
+    if not dirty
+    then return value
+    else do
+        put (Map.insert key now modTime, now + 1)
+        task fetch
+
+--------------------------- Dependency approximation ---------------------------
+data DependencyApproximation k = SubsetOf [k] | Unknown
+
+type ApproximationInfo k = (k -> Bool, k -> DependencyApproximation k)
+
+-- | This rebuilders uses approximate dependencies to decide whether a key
+-- needs to be rebuilt. Used by Excel.
+approximationRebuilder :: Ord k => Rebuilder Monad (ApproximationInfo k) k v
+approximationRebuilder key value task fetch = do
+    (isDirty, deps) <- get
+    let dirty = isDirty key || case deps key of SubsetOf ks -> any isDirty ks
+                                                Unknown     -> True
+    if not dirty
+    then return value
+    else do
+        put (\k -> k == key || isDirty k, deps)
+        task fetch
+
+------------------------------- Verifying traces -------------------------------
+-- | This rebuilder relies on verifying traces.
+vtRebuilder :: (Eq k, Hashable v) => Rebuilder Monad (VT k v) k v
+vtRebuilder key value task fetch = do
+    vt <- get
+    dirty <- not <$> verifyVT key value (fmap hash . fetch) vt
+    if not dirty
+    then return value
+    else do
+        (newValue, deps) <- trackM task fetch
+        put =<< recordVT key newValue deps (fmap hash . fetch) =<< get
+        return newValue
+
+------------------------------ Constructive traces -----------------------------
+-- | This rebuilder relies on constructive traces.
+ctRebuilder :: (Eq k, Hashable v) => Rebuilder Monad (CT k v) k v
+ctRebuilder key value task fetch = do
+    ct <- get
+    maybeCachedValue <- constructCT key value (fmap hash . fetch) ct
+    case maybeCachedValue of
+        Just cachedValue -> return cachedValue
+        Nothing -> do
+            (newValue, deps) <- trackM task fetch
+            put =<< recordCT key newValue deps (fmap hash . fetch) =<< get
+            return newValue
+
+----------------------- Deterministic constructive traces ----------------------
+-- | This rebuilder relies on deterministic constructive traces.
+dctRebuilder :: (Hashable k, Hashable v) => Rebuilder Monad (DCT k v) k v
+dctRebuilder key _value task fetch = do
+    dct <- get
+    maybeCachedValue <- constructDCT key (fmap hash . fetch) dct
+    case maybeCachedValue of
+        Just cachedValue -> return cachedValue
+        Nothing -> do
+            (newValue, deps) <- trackM task fetch
+            put =<< recordDCT key newValue deps (fmap hash . fetch) =<< get
+            return newValue
+
+------------------------------- Version traces -------------------------------
+-- | This rebuilder relies on version/step traces.
+stRebuilder :: (Eq k, Hashable v) => Rebuilder Monad (Step, ST k v) k v
+stRebuilder key value task fetch = do
+    dirty <- not <$> verifyST key value (void . fetch) (gets snd)
+    if not dirty
+    then return value
+    else do
+        (newValue, deps) <- trackM task fetch
+        (step, st) <- get
+        put . (step,) =<< recordST step key newValue deps st
+        return newValue
diff --git a/src/Build/Scheduler.hs b/src/Build/Scheduler.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Scheduler.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE FlexibleContexts, RankNTypes, ScopedTypeVariables, TupleSections #-}
+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications, GeneralizedNewtypeDeriving #-}
+
+-- | Build schedulers execute task rebuilders in the right order.
+module Build.Scheduler (
+    topological,
+    reordering, Chain,
+    restarting,
+    recursive,
+    independent
+    ) where
+
+import Control.Monad.State
+import Control.Monad.Trans.Except
+import Data.Set (Set)
+
+import Build
+import Build.Task
+import Build.Task.Monad
+import Build.Task.Wrapped
+import Build.Store
+import Build.Rebuilder
+import Build.Utilities
+
+import qualified Data.Set               as Set
+import qualified Build.Task.Applicative as A
+
+-- | Update the value of a key in the store. The function takes both the current
+-- value (the first parameter of type @v@) and the new value (the second
+-- parameter of type @v@), and can potentially avoid touching the store if the
+-- value is unchanged. The current implementation simply ignores the current
+-- value, but in future this may be optimised, e.g. by comparing their hashes.
+updateValue :: Eq k => k -> v -> v -> Store i k v -> Store i k v
+updateValue key _value newValue = putValue key newValue
+
+---------------------------------- Topological ---------------------------------
+-- | This scheduler constructs the dependency graph of the target key by
+-- extracting all (static) dependencies upfront, and then traversing the graph
+-- in the topological order, rebuilding keys using the supplied rebuilder.
+topological :: Ord k => Rebuilder Applicative i k v -> Build Applicative i k v
+topological rebuilder tasks key = execState $ forM_ chain $ \k ->
+    case tasks k of
+        Nothing   -> return ()
+        Just task -> do
+            value <- gets (getValue k)
+            let newTask = rebuilder k value (unwrap @Applicative task)
+                newFetch :: k -> StateT i (State (Store i k v)) v
+                newFetch = lift . gets . getValue
+            info <- gets getInfo
+            (newValue, newInfo) <- runStateT (newTask newFetch) info
+            modify $ putInfo newInfo . updateValue k value newValue
+  where
+    deps  = maybe [] (\t -> A.dependencies $ unwrap @Applicative t) . tasks
+    chain = case topSort (graph deps key) of
+        Nothing -> error "Cannot build tasks with cyclic dependencies"
+        Just xs -> xs
+
+---------------------------------- Restarting ----------------------------------
+-- | Convert a task with a total lookup function @k -> m v@ into a task
+-- with a lookup function that can throw exceptions @k -> m (Either e v)@. This
+-- essentially lifts the task from the type of values @v@ to @Either e v@,
+-- where the result @Left e@ indicates that the task failed, e.g. because of a
+-- failed dependency lookup, and @Right v@ yeilds the value otherwise.
+try :: Task (MonadState i) k v -> Task (MonadState i) k (Either e v)
+try task fetch = runExceptT $ task (ExceptT . fetch)
+
+-- | The so-called @calculation chain@: the order in which keys were built
+-- during the previous build, which is used as the best guess for the current
+-- build by Excel and other similar build systems.
+type Chain k = [k]
+
+-- | A model of the scheduler used by Excel, which builds keys in the order used
+-- in the previous build. If a key cannot be build because its dependencies have
+-- changed and a new dependency is still dirty, the corresponding build task is
+-- abandoned and the key is moved at the end of the calculation chain, so it can
+-- be restarted when all its dependencies are up to date.
+reordering :: forall i k v. Ord k => Rebuilder Monad i k v -> Build Monad (i, Chain k) k v
+reordering rebuilder tasks key = execState $ do
+    chain    <- snd . getInfo <$> get
+    newChain <- go Set.empty $ chain ++ [key | key `notElem` chain]
+    modify . mapInfo $ \(i, _) -> (i, newChain)
+  where
+    go :: Set k -> Chain k -> State (Store (i, Chain k) k v) (Chain k)
+    go _    []     = return []
+    go done (k:ks) = case tasks k of
+        Nothing -> (k :) <$> go (Set.insert k done) ks
+        Just task -> do
+            store <- get
+            let value = getValue k store
+                newTask :: Task (MonadState i) k v
+                newTask = rebuilder k value (unwrap @Monad task)
+                newFetch :: k -> State i (Either k v)
+                newFetch k | k `Set.member` done = return $ Right (getValue k store)
+                           | otherwise           = return $ Left k
+            case runState (try newTask newFetch) (fst $ getInfo store) of
+                (Left dep, _) -> go done $ [ dep | dep `notElem` ks ] ++ ks ++ [k]
+                (Right newValue, newInfo) -> do
+                    modify $ putInfo (newInfo, []) . updateValue k value newValue
+                    (k :) <$> go (Set.insert k done) ks
+
+-- | An item in the queue comprises a key that needs to be built and a list of
+-- keys that are blocked on it. More efficient implementations are possible,
+-- e.g. storing blocked keys in a @Map k [k]@ would allow faster queue updates.
+type Queue k = [(k, [k])]
+
+-- | Add a key with a list of blocked keys to the queue. If the key is already
+-- in the queue, extend its list of blocked keys.
+enqueue :: Eq k => k -> [k] -> Queue k -> Queue k
+enqueue key blocked [] = [(key, blocked)]
+enqueue key blocked ((k, bs):q)
+    | k == key  = (k, blocked ++ bs) : q
+    | otherwise = (k, bs) : enqueue key blocked q
+
+-- | Extract a key and a list of blocked keys from the queue, or return
+-- @Nothing@ if the queue is empty.
+dequeue :: Queue k -> Maybe (k, [k], Queue k)
+dequeue []          = Nothing
+dequeue ((k, bs):q) = Just (k, bs, q)
+
+-- | Check if a key is dirty by examining its dependencies, as well as the
+-- stored build information.
+type IsDirty i k v = k -> Store i k v -> Bool
+
+-- | A model of the scheduler used by Bazel. We extract a key K from the queue
+-- and try to build it. There are now two cases:
+-- 1. The build fails because one of the dependencies of K is dirty. In this
+--    case we add the dirty dependency to the queue, listing K as blocked by it.
+-- 2. The build succeeds, in which case we add all keys that were previously
+--    blocked by K to the queue.
+restarting :: forall i k v. Eq k => IsDirty i k v -> Rebuilder Monad i k v -> Build Monad i k v
+restarting isDirty rebuilder tasks key = execState $ go (enqueue key [] mempty)
+  where
+    go :: Queue k -> State (Store i k v) ()
+    go queue = case dequeue queue of
+        Nothing -> return ()
+        Just (k, bs, q) -> case tasks k of
+            Nothing -> return () -- Never happens: we have no inputs in the queue
+            Just task -> do
+                store <- get
+                let value = getValue k store
+                    upToDate k = isInput tasks k || not (isDirty k store)
+                    newTask :: Task (MonadState i) k v
+                    newTask = rebuilder k value (unwrap @Monad task)
+                    newFetch :: k -> State i (Either k v)
+                    newFetch k | upToDate k = return (Right (getValue k store))
+                               | otherwise  = return (Left k)
+                case runState (try newTask newFetch) (getInfo store) of
+                    (Left dirtyDependency, _) -> go (enqueue dirtyDependency (k:bs) q)
+                    (Right newValue, newInfo) -> do
+                        modify $ putInfo newInfo . updateValue k value newValue
+                        go (foldr (\b -> enqueue b []) q bs)
+
+----------------------------------- Recursive ----------------------------------
+-- | This scheduler builds keys recursively: to build a key it first makes sure
+-- that all its dependencies are up to date and then executes the key's task.
+-- It stores the set of keys that have already been built as part of the state
+-- to avoid executing the same task twice.
+recursive :: forall i k v. Ord k => Rebuilder Monad i k v -> Build Monad i k v
+recursive rebuilder tasks key store = fst $ execState (fetch key) (store, Set.empty)
+  where
+    fetch :: k -> State (Store i k v, Set k) v
+    fetch key = case tasks key of
+        Nothing -> gets (getValue key . fst)
+        Just task -> do
+            done <- gets snd
+            when (key `Set.notMember` done) $ do
+                value <- gets (getValue key . fst)
+                let newTask = rebuilder key value (unwrap @Monad task)
+                    newFetch :: k -> StateT i (State (Store i k v, Set k)) v
+                    newFetch = lift . fetch
+                info <- gets (getInfo . fst)
+                (newValue, newInfo) <- runStateT (newTask newFetch) info
+                modify $ \(s, done) ->
+                    ( putInfo newInfo $ updateValue key value newValue s
+                    , Set.insert key done )
+            gets (getValue key . fst)
+
+-- | An incorrect scheduler that builds the target key without respecting its
+-- dependencies. It produces the correct result only if all dependencies of the
+-- target key are up to date.
+independent :: forall i k v. Eq k => Rebuilder Monad i k v -> Build Monad i k v
+independent rebuilder tasks key store = case tasks key of
+    Nothing -> store
+    Just task ->
+        let value   = getValue key store
+            newTask = rebuilder key value (unwrap @Monad task)
+            newFetch :: k -> State i v
+            newFetch k = return (getValue k store)
+            (newValue, newInfo) = runState (newTask newFetch) (getInfo store)
+        in putInfo newInfo $ updateValue key value newValue store
diff --git a/src/Build/SelfTracking.hs b/src/Build/SelfTracking.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/SelfTracking.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE ConstraintKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+-- | This module defines two different strategies of self-tracking, based
+-- around the idea of storing task descriptions that can be parsed into a Task.
+--
+-- * For Monad it works out beautifully. You just store the rule on the disk,
+--   and depend on it.
+--
+-- * For Applicative, we generate a fresh Task each time, but have that Task
+--   depend on a fake version of the rules. This is a change in the Task, but
+--   it's one for which the standard implementations tend to cope with just fine.
+--   Most Applicative systems with self-tracking probably do it this way.
+module Build.SelfTracking (
+    Key (..), Value (..), selfTrackingM, selfTrackingA
+    ) where
+
+import Build.Task
+
+-- We assume that the fetch passed to a Task is consistent and returns values
+-- matching the keys. It is possible to switch to typed tasks to check this
+-- assumption at compile time, e.g. see "Build.Task.Typed".
+data Key k     = Key k   | KeyTask k
+data Value v t = Value v | ValueTask t
+
+-- Fetch a value
+fetchValue :: Functor f => (Key k -> f (Value v t)) -> k -> f v
+fetchValue fetch key = extract <$> fetch (Key key)
+  where
+    extract (Value v) = v
+    extract _ = error "Inconsistent fetch"
+
+-- Fetch a task description
+fetchValueTask :: Functor f => (Key k -> f (Value v t)) -> k -> f t
+fetchValueTask fetch key = extract <$> fetch (KeyTask key)
+  where
+    extract (ValueTask t) = t
+    extract _ = error "Inconsistent fetch"
+
+-- | A model using Monad, works beautifully and allows storing the key on the disk.
+selfTrackingM :: (t -> Task Monad k v) -> Tasks Monad k t -> Tasks Monad (Key k) (Value v t)
+selfTrackingM _      _     (KeyTask _) = Nothing -- Task keys are inputs
+selfTrackingM parser tasks (Key     k) = runTask <$> tasks k
+  where
+    -- Fetch the task description, parse it, and then run the obtained task
+    runTask act fetch = do
+        task <- parser <$> act (fetchValueTask fetch)
+        Value <$> task (fetchValue fetch)
+
+-- | The Applicative model requires every key to be able to associate with its
+-- environment (e.g. a reader somewhere). Does not support cutoff if a key changes.
+selfTrackingA :: (t -> Task Applicative k v) -> (k -> t) -> Tasks Applicative (Key k) (Value v t)
+selfTrackingA _      _   (KeyTask _) = Nothing -- Task keys are inputs
+selfTrackingA parser ask (Key k) = Just $ \fetch ->
+    fetch (KeyTask k) *> (Value <$> parser (ask k) (fetchValue fetch))
diff --git a/src/Build/Store.hs b/src/Build/Store.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Store.hs
@@ -0,0 +1,72 @@
+-- | An abstract key/value store.
+module Build.Store (
+    -- * Hashing
+    Hash, Hashable (..),
+
+    -- * Store
+    Store, getValue, putValue, getHash, getInfo, putInfo, mapInfo,
+    initialise
+    ) where
+
+-- | A 'Hash' is used for efficient tracking and sharing of build results. We
+-- use @newtype Hash a = Hash a@ for prototyping.
+newtype Hash a = Hash a deriving (Eq, Ord,Show)
+
+instance Functor Hash where
+    fmap f (Hash a) = Hash (f a)
+
+instance Applicative Hash where
+    pure = Hash
+    Hash f <*> Hash a = Hash (f a)
+
+class Ord a => Hashable a where
+    -- | Compute the hash of a given value. We typically assume cryptographic
+    -- hashing, e.g. SHA256.
+    hash :: a -> Hash a
+
+instance Hashable Int where
+    hash = Hash
+
+instance Hashable Integer where
+    hash = Hash
+
+instance Hashable a => Hashable [a] where
+    hash = Hash
+
+instance Hashable a => Hashable (Hash a) where
+    hash = Hash
+
+instance (Hashable a, Hashable b) => Hashable (a, b) where
+    hash = Hash
+
+-- | An abstract datatype for a key/value store with build information of type @i@.
+data Store i k v = Store { info :: i, values :: k -> v }
+
+-- | Read the build information.
+getInfo :: Store i k v -> i
+getInfo = info
+
+-- | Read the value of a key.
+getValue :: k -> Store i k v -> v
+getValue = flip values
+
+-- | Read the hash of a key's value. In some cases may be implemented more
+-- efficiently than @hash . getValue k@.
+getHash :: Hashable v => k -> Store i k v -> Hash v
+getHash k = hash . getValue k
+
+-- | Write the build information.
+putInfo :: i -> Store i k v -> Store i k v
+putInfo i s = s { info = i }
+
+-- | Modify the build information.
+mapInfo :: (i -> j) -> Store i k v -> Store j k v
+mapInfo f (Store i kv) = Store (f i) kv
+
+-- | Update the value of a key.
+putValue :: Eq k => k -> v -> Store i k v -> Store i k v
+putValue k v s = s { values = \key -> if key == k then v else values s key }
+
+-- | Initialise the store.
+initialise :: i -> (k -> v) -> Store i k v
+initialise = Store
diff --git a/src/Build/System.hs b/src/Build/System.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/System.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+-- | Models of several build systems.
+module Build.System (
+    -- * Toy build systems
+    dumb, busy, memo,
+
+    -- * Applicative build systems
+    make, ninja, bazel, buck,
+
+    -- * Monadic build systems
+    excel, shake, cloudShake, nix
+    ) where
+
+import Control.Monad.State
+
+import Build
+import Build.Scheduler
+import Build.Store
+import Build.Rebuilder
+import Build.Trace
+
+-- | This is not a correct build system: given a target key, it simply rebuilds
+-- it, without rebuilding any of its dependencies.
+dumb :: Eq k => Build Monad () k v
+dumb = independent perpetualRebuilder
+
+-- | This is a correct but non-minimal build system: given a target key it
+-- recursively rebuilds its dependencies, even if they are already up to date.
+-- There is no memoisation, therefore the a key may be built multiple times.
+busy :: forall k v. Eq k => Build Monad () k v
+busy tasks key store = execState (fetch key) store
+  where
+    fetch :: k -> State (Store () k v) v
+    fetch k = case tasks k of
+        Nothing   -> gets (getValue k)
+        Just task -> do v <- task fetch; modify (putValue k v); return v
+
+-- | This is a correct but non-minimal build system: it will rebuild keys even
+-- if they are up to date. However, it performs memoization, therefore it never
+-- builds a key twice.
+memo :: Ord k => Build Monad () k v
+memo = recursive perpetualRebuilder
+
+-- | A model of Make: an applicative build system that uses file modification
+-- times to check if a key is up to date.
+make :: forall k v. Ord k => Build Applicative (MakeInfo k) k v
+make = topological modTimeRebuilder
+
+-- | A model of Ninja: an applicative build system that uses verifying traces
+-- to check if a key is up to date.
+ninja :: (Ord k, Hashable v) => Build Applicative (VT k v) k v
+ninja = topological vtRebuilder
+
+type ExcelInfo k = (ApproximationInfo k, Chain k)
+
+-- | A model of Excel: a monadic build system that stores the calculation chain
+-- from the previuos build and approximate dependencies.
+excel :: Ord k => Build Monad (ExcelInfo k) k v
+excel = reordering approximationRebuilder
+
+-- | A model of Shake: a monadic build system that uses verifying traces to
+-- check if a key is up to date.
+shake :: (Ord k, Hashable v) => Build Monad (Step, ST k v) k v
+shake = recursive stRebuilder
+
+-- | A model of Bazel: a monadic build system that uses constructive traces
+-- to check if a key is up to date as well as for caching build results. Note
+-- that Bazel currently does not allow users to write monadic build rules: only
+-- built-in rules have access to dynamic dependencies.
+bazel :: (Ord k, Hashable v) => Build Monad (CT k v) k v
+bazel = restarting isDirtyCT ctRebuilder
+
+-- | A model of Cloud Shake: a monadic build system that uses constructive
+-- traces to check if a key is up to date as well as for caching build results.
+cloudShake :: (Ord k, Hashable v) => Build Monad (CT k v) k v
+cloudShake = recursive ctRebuilder
+
+-- | A model of Buck: an applicative build system that uses deterministic
+-- constructive traces to check if a key is up to date as well as for caching
+-- build results.
+buck :: (Hashable k, Hashable v) => Build Applicative (DCT k v) k v
+buck = topological dctRebuilder
+
+-- | A model of Nix: a monadic build system that uses deterministic constructive
+-- traces to check if a key is up to date as well as for caching build results.
+nix :: (Hashable k, Hashable v) => Build Monad (DCT k v) k v
+nix = recursive dctRebuilder
diff --git a/src/Build/Task.hs b/src/Build/Task.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE ConstraintKinds, RankNTypes, StandaloneDeriving #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+-- | The Task abstractions.
+module Build.Task (Task, Tasks) where
+
+import Control.Applicative
+import Control.Monad.Trans.Reader
+
+-- Ideally we would like to write:
+--
+--    type Tasks c k v = k -> Maybe (Task c k v)
+--    type Task  c k v = forall f. c f => (k -> f v) -> f v
+--
+-- Alas, we can't since it requires impredicative polymorphism and GHC currently
+-- does not support it.
+--
+-- A usual workaround is to wrap 'Task' into a newtype, but this leads to the
+-- loss of higher-rank polymorphism: for example, we can no longer apply a
+-- monadic build system to an applicative task description or apply a monadic
+-- 'trackM' to trace the execution of a 'Task Applicative'. This leads to severe
+-- code duplication.
+--
+-- Our workaround is inspired by the @lens@ library, which allows us to keep
+-- higher-rank polymorphism at the cost of inserting 'unwrap' in a few places
+-- in our code and using slightly strange definitions of 'Tasks' and 'Task'.
+-- See "Build.Task.Wrapped".
+
+-- | 'Tasks' associates a 'Task' with every non-input key. @Nothing@ indicates
+-- that the key is an input.
+type Tasks c k v = forall f. c f => k -> Maybe ((k -> f v) -> f v)
+
+-- | A task is used to compute the value of a key, by finding the necessary
+-- dependencies using the provided @fetch :: k -> f v@ callback.
+type Task c k v = forall f. c f => (k -> f v) -> f v
+
+-- | Compose two task descriptions, preferring the first one in case there are
+-- two tasks corresponding to the same key.
+compose :: Tasks Monad k v -> Tasks Monad k v -> Tasks Monad k v
+compose t1 t2 key = t1 key <|> t2 key
+
+-- | An alternative type for task descriptions, isomorphic to 'Tasks' as
+-- demonstrated by functions 'fromTasks' and 'toTasks'.
+type Tasks2 c k v = forall f. c f => (k -> f v) -> k -> Maybe (f v)
+
+fromTasks :: Tasks Monad k v -> Tasks2 Monad k v
+fromTasks tasks fetch key = ($fetch) <$> tasks key
+
+toTasks :: Tasks2 Monad k v -> Tasks Monad k v
+toTasks tasks2 key = runReaderT <$> tasks2 (\k -> ReaderT ($k)) key
diff --git a/src/Build/Task/Applicative.hs b/src/Build/Task/Applicative.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/Applicative.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+
+-- | Applicative tasks, as used by Make, Ninja and other applicative build
+-- systems. Dependencies of applicative tasks are known statically, before their
+-- execution.
+module Build.Task.Applicative (dependencies) where
+
+import Control.Applicative
+
+import Build.Task
+
+-- | Find the dependencies of an applicative task.
+dependencies :: Task Applicative k v -> [k]
+dependencies task = getConst $ task (\k -> Const [k])
diff --git a/src/Build/Task/Depend.hs b/src/Build/Task/Depend.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/Depend.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DeriveFunctor, RankNTypes #-}
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+-- | The \"free\" structures for dependencies, providing either an applicative
+-- interface (for 'Depend') or a monadic interface (for 'Depends'). By passing
+-- them to a suitable 'Task' you can reconstruct all necessary dependencies.
+module Build.Task.Depend (toDepend, Depend (..), toDepends, Depends (..)) where
+
+import Build.Task
+
+----------------------------- Free Task Applicative ----------------------------
+
+-- | A list of dependencies, and a function that when applied to those
+-- dependencies produces the result.
+data Depend k v r = Depend [k] ([v] -> r)
+    deriving Functor
+
+instance Applicative (Depend k v) where
+    pure v = Depend [] (\[] -> v)
+    Depend d1 f1 <*> Depend d2 f2 = Depend (d1++d2) $
+        \vs -> let (v1,v2) = splitAt (length d1) vs in f1 v1 $ f2 v2
+
+toDepend :: Task Applicative k v -> Depend k v v
+toDepend f = f $ \k -> Depend [k] $ \[v] -> v
+
+-------------------------------- Free Task Monad -------------------------------
+
+-- | A list of dependencies, and a function that when applied to those
+-- dependencies either the result or more dependencies.
+data Depends k v r = Depends [k] ([v] -> Depends k v r)
+                   | Done r
+    deriving Functor
+
+instance Applicative (Depends k v) where
+    pure = return
+    f1 <*> f2 = f2 >>= \v -> ($ v) <$> f1
+
+instance Monad (Depends k v) where
+    return = Done
+    Done x >>= f = f x
+    Depends ds op >>= f = Depends ds $ \vs -> f =<< op vs
+
+toDepends :: Task Monad k v -> Depends k v v
+toDepends f = f $ \k -> Depends [k] $ \[v] -> Done v
diff --git a/src/Build/Task/Functor.hs b/src/Build/Task/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/Functor.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+
+-- | Functorial tasks, which have exactly one statically known dependency.
+-- Docker is an example of a functorial build system: Docker containers are
+-- organised in layers, where each layer makes changes to the previous one.
+module Build.Task.Functor (dependency) where
+
+import Data.Functor.Const
+
+import Build.Task
+
+-- | Find the dependency of a functorial task.
+dependency :: Task Functor k v -> k
+dependency task = getConst $ task Const
diff --git a/src/Build/Task/Monad.hs b/src/Build/Task/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/Monad.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeApplications #-}
+
+-- | Monadic tasks, as used by Excel, Shake and other build systems.
+-- Dependencies of monadic tasks can only be discovered dynamically, i.e. during
+-- their execution.
+module Build.Task.Monad (track, trackM, isInput, compute, partial, exceptional) where
+
+import Control.Monad.Trans
+import Control.Monad.Trans.Except
+import Control.Monad.Trans.Maybe
+import Control.Monad.Writer
+import Data.Functor.Identity
+import Data.Maybe
+
+import Build.Task
+
+-- | Execute a monadic task on a pure store @k -> v@, tracking the dependencies.
+track :: Task Monad k v -> (k -> v) -> (v, [k])
+track task fetch = runWriter $ task (\k -> writer (fetch k, [k]))
+
+-- | Execute a monadic task using an effectful fetch function @k -> m v@,
+-- tracking the dependencies.
+trackM :: forall m k v. Monad m => Task Monad k v -> (k -> m v) -> m (v, [k])
+trackM task fetch = runWriterT $ task trackingFetch
+  where
+    trackingFetch :: k -> WriterT [k] m v
+    trackingFetch k = tell [k] >> lift (fetch k)
+
+-- | Given a description of tasks, check if a key is input.
+isInput :: forall k v. Tasks Monad k v -> k -> Bool
+isInput tasks key = isNothing (tasks key :: Maybe ((k -> Maybe v) -> Maybe v))
+
+-- | Run a task with a pure lookup function.
+compute :: Task Monad k v -> (k -> v) -> v
+compute task store = runIdentity $ task (Identity . store)
+
+-- | Convert a task with a total lookup function @k -> m v@ into a task with a
+-- partial lookup function @k -> m (Maybe v)@. This essentially lifts the task
+-- from the type of values @v@ to @Maybe v@, where the result @Nothing@
+-- indicates that the task failed because of a missing dependency.
+partial :: Task Monad k v -> Task Monad k (Maybe v)
+partial task fetch = runMaybeT $ task (MaybeT . fetch)
+
+-- | Convert a task with a total lookup function @k -> m v@ into a task with a
+-- lookup function that can throw exceptions @k -> m (Either e v)@. This
+-- essentially lifts the task from the type of values @v@ to @Either e v@, where
+-- the result @Left e@ indicates that the task failed because of a failed
+-- dependency lookup, and @Right v@ yeilds the value otherwise.
+exceptional :: Task Monad k v -> Task Monad k (Either e v)
+exceptional task fetch = runExceptT $ task (ExceptT . fetch)
diff --git a/src/Build/Task/MonadPlus.hs b/src/Build/Task/MonadPlus.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/MonadPlus.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE RankNTypes, TypeApplications #-}
+
+-- | A version of monadic tasks with some support for non-determinism.
+module Build.Task.MonadPlus (random, computeND, correctBuildValue) where
+
+import Control.Monad
+
+import Build.Task
+import Build.Task.Wrapped
+import Build.Store
+
+-- | An example of a non-deterministic task: generate a random number from a
+-- specified interval.
+random :: (Int, Int) -> Task MonadPlus k Int
+random (low, high) = const $ foldr mplus mzero $ map pure [low..high]
+
+-- | Run a non-deterministic task with a pure lookup function, listing all
+-- possible results.
+computeND :: Task MonadPlus k v -> (k -> v) -> [v]
+computeND task store = task (return . store)
+
+-- | Given a description of @tasks@, an initial @store@, and a @result@ produced
+-- by running a build system on a target @key@, this function returns 'True' if
+-- the @key@'s value is a possible result of running the associated task.
+correctBuildValue :: Eq v => Tasks MonadPlus k v -> Store i k v -> Store i k v -> k -> Bool
+correctBuildValue tasks store result k = case tasks k of
+    Nothing -> getValue k result == getValue k store
+    Just t -> getValue k result `elem` computeND (unwrap @MonadPlus t) (flip getValue store)
diff --git a/src/Build/Task/Typed.hs b/src/Build/Task/Typed.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/Typed.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE ConstraintKinds, RankNTypes, GADTs, TypeFamilies #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
+
+-- | A Typed version of dependencies where the value type depends on the key.
+-- See the source for an example.
+module Build.Task.Typed (Task, Key (..), showDependencies) where
+
+import Data.Functor.Const
+import Data.Functor.Identity
+
+-- | A type class for keys, equipped with an associated type family that
+-- can be used to determine the type of value corresponding to the key.
+class Key k where
+    type Value k :: *
+    -- | The name of the key. Useful for avoiding heterogeneous lists of keys.
+    showKey :: k -> String
+
+-- | A typed build task.
+type Task c k = forall f. c f => (forall k. Key k => k -> f (Value k)) -> k -> Maybe (f (Value k))
+
+-- | Extract the names of dependencies.
+showDependencies :: Task Applicative k -> k -> [String]
+showDependencies task = maybe [] getConst . task (\k -> Const [showKey k])
+
+------------------------------------ Example -----------------------------------
+data ExampleKey a where
+    Base       :: ExampleKey Int
+    Number     :: ExampleKey Int
+    SplitDigit :: ExampleKey (Int, Int)
+    LastDigit  :: ExampleKey Int
+    BaseDigits :: ExampleKey [Int]
+
+instance Show (ExampleKey a) where
+    show key = case key of
+        Base       -> "Base"
+        Number     -> "Number"
+        SplitDigit -> "SplitDigit"
+        LastDigit  -> "LastDigit"
+        BaseDigits -> "BaseDigits"
+
+instance Key (ExampleKey a) where
+    type Value (ExampleKey a) = a
+    showKey = show
+
+digits :: Task Applicative (ExampleKey a)
+digits fetch SplitDigit = Just $ divMod <$> fetch Number <*> fetch Base
+digits fetch LastDigit  = Just $ snd <$> fetch SplitDigit
+digits fetch BaseDigits = Just $ enumFromTo 1 <$> fetch Base
+digits _ _ = Nothing
+
+fetch :: ExampleKey t -> Identity (Value (ExampleKey t))
+fetch key = Identity $ case key of
+    Base       -> 10
+    Number     -> 2018
+    SplitDigit -> (201, 8)
+    LastDigit  -> 8
+    BaseDigits -> [0..9]
diff --git a/src/Build/Task/Wrapped.hs b/src/Build/Task/Wrapped.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Task/Wrapped.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE ConstraintKinds, DeriveFunctor, FlexibleInstances #-}
+{-# LANGUAGE RankNTypes, StandaloneDeriving #-}
+
+-- | This whole module is just a tiresome workaround for the lack of impredicative
+-- polymorphism. If GHC adds impredicative polymorphism, we can drop it entirely
+-- and simplify the rest of the code by removing unnecessary task unwrapping.
+module Build.Task.Wrapped (GTask (..), Wrapped, unwrap) where
+
+import Control.Applicative
+import Control.Monad
+
+import Build.Task
+
+-- | GTask is a generalised Task wrapped in a newtype. It is generalised in the
+-- sense that it computes a value of type @a@ given a fetch of type @k -> f v@.
+newtype GTask c k v a =
+    GTask { runGTask :: forall f. c f => (k -> f v) -> f a }
+
+type Wrapped c k v = (k -> GTask c k v v) -> GTask c k v v
+
+unwrap :: forall c k v. Wrapped c k v -> Task c k v
+unwrap wrapped = runGTask (wrapped f)
+  where
+    f :: k -> GTask c k v v
+    f k = GTask $ \f -> f k
+
+-- Thanks to the generalisation, we can make GTask an instance of many classes
+deriving instance Functor (GTask Functor     k v)
+deriving instance Functor (GTask Applicative k v)
+deriving instance Functor (GTask Alternative k v)
+deriving instance Functor (GTask Monad       k v)
+deriving instance Functor (GTask MonadPlus   k v)
+
+instance Applicative (GTask Applicative k v) where
+    pure x = GTask $ \_ -> pure x
+    GTask f <*> GTask x = GTask $ \fetch -> f fetch <*> x fetch
+
+instance Applicative (GTask Alternative k v) where
+    pure x = GTask $ \_ -> pure x
+    GTask f <*> GTask x = GTask $ \fetch -> f fetch <*> x fetch
+
+instance Applicative (GTask Monad k v) where
+    pure x = GTask $ \_ -> pure x
+    GTask f <*> GTask x = GTask $ \fetch -> f fetch <*> x fetch
+
+instance Applicative (GTask MonadPlus k v) where
+    pure x = GTask $ \_ -> pure x
+    GTask f <*> GTask x = GTask $ \fetch -> f fetch <*> x fetch
+
+instance Monad (GTask Monad k v) where
+    return x = GTask $ \_ -> return x
+    GTask x >>= f = GTask $ \fetch -> x fetch >>= \a -> runGTask (f a) fetch
+
+instance Monad (GTask MonadPlus k v) where
+    return x = GTask $ \_ -> return x
+    GTask x >>= f = GTask $ \fetch -> x fetch >>= \a -> runGTask (f a) fetch
+
+instance Alternative (GTask Alternative k v) where
+    empty = GTask $ \_ -> empty
+    GTask x <|> GTask y = GTask $ \fetch -> x fetch <|> y fetch
+
+instance Alternative (GTask MonadPlus k v) where
+    empty = GTask $ \_ -> empty
+    GTask x <|> GTask y = GTask $ \fetch -> x fetch <|> y fetch
+
+instance MonadPlus (GTask MonadPlus k v) where
+    mzero = empty
+    mplus = (<|>)
diff --git a/src/Build/Trace.hs b/src/Build/Trace.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Trace.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables #-}
+{-# LANGUAGE DeriveTraversable, TupleSections #-}
+
+-- | Build traces that are used for recording information from previuos builds.
+module Build.Trace (
+    Trace (..),
+
+    -- * Verifying traces
+    VT, recordVT, verifyVT,
+
+    -- * Constructive traces
+    CT, isDirtyCT, recordCT, constructCT,
+
+    -- * Constructive traces optimised for deterministic tasks
+    DCT, recordDCT, constructDCT,
+
+    -- * Step traces
+    Step, ST, recordST, verifyST
+    ) where
+
+import Build.Store
+
+import Control.Monad.Extra
+import Data.Maybe
+import Data.List
+import Data.Semigroup
+
+-- | A trace is parameterised by the types of keys @k@, hashes @h@, as well as the
+-- result @r@. For verifying traces, @r = h@; for constructive traces, @Hash r = h@.
+data Trace k h r = Trace
+    { key     :: k
+    , depends :: [(k, h)]
+    , result  :: r }
+    deriving Show
+
+------------------------------- Verifying traces -------------------------------
+
+-- | An abstract data type for a set of verifying traces equipped with 'recordVT',
+-- 'verifyVT' and a 'Monoid' instance.
+newtype VT k v = VT [Trace k (Hash v) (Hash v)] deriving (Monoid, Semigroup)
+
+-- | Record a new trace for building a @key@ with dependencies @deps@, obtaining
+-- the hashes of up-to-date values by using @fetchHash@.
+recordVT :: (Hashable v, Monad m) => k -> v -> [k] -> (k -> m (Hash v)) -> VT k v -> m (VT k v)
+recordVT key value deps fetchHash (VT ts) = do
+    hs <- mapM fetchHash deps
+    return $ VT $ Trace key (zip deps hs) (hash value) : ts
+
+-- | Given a function to compute the hash of a key's current value,
+-- a @key@, and a set of verifying traces, return 'True' if the @key@ is
+-- up-to-date.
+verifyVT :: (Monad m, Eq k, Hashable v) => k -> v -> (k -> m (Hash v)) -> VT k v -> m Bool
+verifyVT key value fetchHash (VT ts) = anyM match ts
+  where
+    match (Trace k deps result)
+        | k /= key || result /= hash value = return False
+        | otherwise = andM [ (h==) <$> fetchHash k | (k, h) <- deps ]
+
+------------------------------ Constructive traces -----------------------------
+
+-- | An abstract data type for a set of constructive traces equipped with
+-- 'recordCT', 'isDirtyCT', 'constructCT' and a 'Monoid' instance.
+newtype CT k v = CT [Trace k (Hash v) v] deriving (Monoid, Semigroup, Show)
+
+-- | Check if a given @key@ is dirty w.r.t a @store@.
+isDirtyCT :: (Eq k, Hashable v) => k -> Store (CT k v) k v -> Bool
+isDirtyCT key store = let CT ts = getInfo store in not (any match ts)
+  where
+    match (Trace k deps result) = k == key
+                               && result == getValue key store
+                               && and [ getHash k store == h | (k, h) <- deps ]
+
+-- | Record a new trace for building a @key@ with dependencies @deps@, obtaining
+-- the hashes of up-to-date values by using @fetchHash@.
+recordCT :: Monad m => k -> v -> [k] -> (k -> m (Hash v)) -> CT k v -> m (CT k v)
+recordCT key value deps fetchHash (CT ts) = do
+    hs <- mapM fetchHash deps
+    return $ CT $ Trace key (zip deps hs) value : ts
+
+-- | Given a function to compute the hash of a key's current value,
+-- a @key@, and a set of constructive traces, return @Just newValue@ if it is
+-- possible to reconstruct it from the traces. Prefer reconstructing the
+-- currenct value, if it matches one of the traces.
+constructCT :: (Monad m, Eq k, Eq v) => k -> v -> (k -> m (Hash v)) -> CT k v -> m (Maybe v)
+constructCT key value fetchHash (CT ts) = do
+    candidates <- catMaybes <$> mapM match ts
+    if value `elem` candidates then return $ Just value
+                               else return $ listToMaybe candidates
+  where
+    match (Trace k deps result)
+        | k /= key  = return Nothing
+        | otherwise = do
+            sameInputs <- andM [ (h==) <$> fetchHash k | (k, h) <- deps ]
+            return $ if sameInputs then Just result else Nothing
+
+----------------------- Deterministic constructive traces ----------------------
+
+-- | A tree of dependencies. It would be more efficient to use graphs, but
+-- trees are simpler and are sufficient for our model.
+data Tree a = Leaf a | Node [Tree a]
+    deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
+
+instance Hashable a => Hashable (Tree a) where
+    hash (Leaf x) = Leaf <$> hash x
+    hash (Node x) = Node <$> hash x
+
+-- | Invariant: if a DCT contains a trace for a key @k@, then it must also
+-- contain traces for each of its non-input dependencies. Input keys cannot
+-- appear in a DCT because they are never built.
+newtype DCT k v = DCT [Trace k (Hash (Tree (Hash v))) v] deriving (Monoid, Semigroup)
+
+-- | Extract the tree of input dependencies of a given key.
+inputTree :: Eq k => DCT k v -> k -> Tree k
+inputTree dct@(DCT ts) key = case [ deps | Trace k deps _ <- ts, k == key ] of
+    [] -> Leaf key
+    deps:_ -> Node $ map (inputTree dct . fst) deps
+
+-- | Like 'inputTree', but replaces each key with the hash of its current value.
+inputHashTree :: (Eq k, Monad m) => DCT k v -> (k -> m (Hash v)) -> k -> m (Tree (Hash v))
+inputHashTree dct fetchHash = traverse fetchHash . inputTree dct
+
+-- | Record a new trace for building a @key@ with dependencies @deps@, obtaining
+-- the hashes of up-to-date values from the given @store@.
+recordDCT :: forall k v m. (Hashable k, Hashable v, Monad m)
+          => k -> v -> [k] -> (k -> m (Hash v)) -> DCT k v -> m (DCT k v)
+recordDCT key value deps fetchHash (DCT ts) = do
+    hs <- mapM depHash deps
+    return $ DCT $ Trace key (zip deps hs) value : ts
+  where
+    depHash :: k -> m (Hash (Tree (Hash v)))
+    depHash depKey = case [ deps | Trace k deps _ <- ts, k == depKey ] of
+        [] -> hash . Leaf <$> fetchHash depKey -- depKey is an input
+        deps:_ -> return $ fmap Node $ sequenceA $ map snd deps
+
+-- | Given a function to compute the hash of a key's current value,
+-- a @key@, and a set of deterministic constructive traces, return
+-- @Just newValue@ if it is possible to reconstruct it from the traces.
+constructDCT :: forall k v m. (Hashable k, Hashable v, Monad m)
+             => k -> (k -> m (Hash v)) -> DCT k v -> m (Maybe v)
+constructDCT key fetchHash dct@(DCT ts) = do
+    candidates <- catMaybes <$> mapM match ts
+    case candidates of
+        []  -> return Nothing
+        [v] -> return (Just v)
+        _   -> error "Non-determinism detected"
+  where
+    match :: Trace k (Hash (Tree (Hash v))) v -> m (Maybe v)
+    match (Trace k deps result)
+        | k /= key  = return Nothing
+        | otherwise = do
+            sameInputs <- andM [ ((h ==) . hash) <$> inputHashTree dct fetchHash k | (k, h) <- deps ]
+            return $ if sameInputs then Just result else Nothing
+
+----------------- Step traces: a refinement of verifying traces ----------------
+
+newtype Step = Step Int deriving (Enum, Eq, Ord, Show)
+instance Semigroup Step where Step a <> Step b = Step $ a + b
+instance Monoid Step where mempty = Step 0; mappend = (<>)
+
+-- | A step trace, records the resulting value, the step it last build, the step
+-- where it changed.
+newtype ST k v = ST [Trace k () (Hash v, Step, Step)]
+    deriving (Monoid, Semigroup, Show)
+
+latestST :: Eq k => k -> ST k v -> Maybe (Trace k () (Hash v, Step, Step))
+latestST k (ST ts) = fmap snd $ listToMaybe $ reverse $ sortOn fst
+    [(step, t) | t@(Trace k2 _ (_, step, _)) <- ts, k == k2]
+
+-- | Record a new trace for building a @key@ with dependencies @deps@.
+recordST :: (Hashable v, Eq k, Monad m) => Step -> k -> v -> [k] -> ST k v -> m (ST k v)
+recordST step key value deps (ST ts) = do
+    let hv = hash value
+    let lastChange = case latestST key (ST ts) of
+            -- I rebuilt, didn't change, so use the old change time
+            Just (Trace _ _ (hv2, _, chng)) | hv2 == hv -> chng
+            _ -> step
+    return $ ST $ Trace key (map (,()) deps) (hash value, step, lastChange) : ts
+
+-- | Given a function to compute the hash of a key's current value,
+-- a @key@, and a set of verifying traces, return 'True' if the @key@ is
+-- up-to-date.
+verifyST :: (Monad m, Eq k, Hashable v) => k -> v -> (k -> m ()) -> m (ST k v) -> m Bool
+verifyST key value demand st = do
+    me <- latestST key <$> st
+    case me of
+        Just (Trace _ deps (hv, built, _)) | hash value == hv -> do
+            mapM_ (demand . fst) deps
+            st <- st
+            -- things with no traces must be inputs, which I'm going to ignore for now...
+            return $ and [ built >= chng | Just (Trace _ _ (_, _, chng)) <- map (flip latestST st . fst) deps]
+        _ -> return False
diff --git a/src/Build/Utilities.hs b/src/Build/Utilities.hs
new file mode 100644
--- /dev/null
+++ b/src/Build/Utilities.hs
@@ -0,0 +1,76 @@
+-- | General utilities useful in the rest of the package
+module Build.Utilities (
+    -- * Graph operations
+    graph, reachable, topSort, reach, reachM,
+
+    -- * Logic combinators
+    forall, forallM, exists, existsM, (==>)
+    ) where
+
+import Algebra.Graph
+import qualified Algebra.Graph.AdjacencyMap as AM
+import qualified Algebra.Graph.Class        as C
+
+import Data.Functor.Identity
+import qualified Data.Set as Set
+
+-- | Build a dependency graph given a function for computing dependencies of a
+-- key and a target key.
+graph :: Ord k => (k -> [k]) -> k -> Graph k
+graph deps key = transpose $ overlays [ star k (deps k) | k <- keys Set.empty [key] ]
+  where
+    keys seen []   = Set.toList seen
+    keys seen (x:xs)
+        | x `Set.member` seen = keys seen xs
+        | otherwise           = keys (Set.insert x seen) (deps x ++ xs)
+
+-- | Compute all keys reachable via dependecies from a target key.
+reachable :: Ord k => (k -> [k]) -> k -> [k]
+reachable deps key = vertexList (graph deps key)
+
+-- | Compute the topological sort of a graph or return @Nothing@ if the graph
+-- has cycles.
+topSort :: Ord k => Graph k -> Maybe [k]
+topSort = AM.topSort . C.toGraph
+
+-- | Given a function to compute successors of a vertex, apply it recursively
+-- starting from a given vertex. Returns @Nothing@ if this process does not
+-- terminate because of cycles. Note that the current implementation is very
+-- inefficient: it trades efficiency for simplicity. The resulting list is
+-- likely to contain an exponential number of duplicates.
+reach :: Eq a => (a -> [a]) -> a -> Maybe [a]
+reach successors = runIdentity . reachM (return . successors)
+
+-- | Given a monadic function to compute successors of a vertex, apply it
+-- recursively starting from a given vertex. Returns @Nothing@ if this process
+-- does not terminate because of cycles. Note that the current implementation is
+-- very inefficient: it trades efficiency for simplicity. The resulting list is
+-- likely to contain an exponential number of duplicates.
+reachM :: (Eq a, Monad m) => (a -> m [a]) -> a -> m (Maybe [a])
+reachM successors a = fmap (filter (/= a)) <$> go [] a
+  where
+    go xs x | x `elem` xs = return Nothing -- A cycle is detected
+            | otherwise   = do res <- traverse (go (x:xs)) =<< successors x
+                               return $ ((x:xs)++) . concat <$> sequence res
+
+-- | Check that a predicate holds for all values of @a@.
+forall :: (a -> Bool) -> Bool
+forall = undefined
+
+-- | Check that a monadic predicate holds for all values of @a@.
+forallM :: (a -> m Bool) -> m Bool
+forallM = undefined
+
+-- | Check that a predicate holds for some value of @a@.
+exists :: (a -> Bool) -> Bool
+exists = undefined
+
+-- | Check that a monadic predicate holds for some value of @a@.
+existsM :: (a -> m Bool) -> m Bool
+existsM = undefined
+
+-- | Logical implication.
+(==>) :: Bool -> Bool -> Bool
+x ==> y = not x || y
+
+infixr 0 ==>
diff --git a/test/Examples.hs b/test/Examples.hs
new file mode 100644
--- /dev/null
+++ b/test/Examples.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE Rank2Types #-}
+
+module Examples where
+
+import Build.Task
+import Control.Applicative
+import Control.Monad.Fail (MonadFail)
+
+
+-- | A useful fetch for experimenting with build systems in interactive GHC.
+fetchIO :: (Show k, Read v) => k -> IO v
+fetchIO k = do putStr (show k ++ ": "); read <$> getLine
+
+--------------------------- Task Functor: Collatz ---------------------------
+
+-- Collatz sequence:
+-- c[0] = n
+-- c[k] = f(c[k - 1]) where
+-- For example, if n = 12, the sequence is 3, 10, 5, 16, 8, 4, 2, 1, ...
+collatz :: Tasks Functor Integer Integer
+collatz n | n <= 0    = Nothing
+          | otherwise = Just $ \fetch -> f <$> fetch (n - 1)
+  where
+    f k | even k    = k `div` 2
+        | otherwise = 3 * k + 1
+
+-- A good demonstration of early cut-off:
+-- * Task Collatz sequence from n = 6: 6, 3, 10, 5, 16, 8, 4, 2, 1, ...
+-- * Change n from 6 to 40 and rebuild: 40, 20, 10, 5, 16, 8, 4, 2, 1, ...
+-- * The recomputation should be cut-off after 10.
+
+------------------------ Task Applicative: Fibonacci ------------------------
+
+-- Generalised Fibonacci sequence:
+-- f[0] = n
+-- f[1] = m
+-- f[k] = f[k - 1] + f[k - 2]
+-- For example, with (n, m) = (0, 1) we get usual Fibonacci sequence, and if
+-- (n, m) = (2, 1) we get Lucas sequence: 2, 1, 3, 4, 7, 11, 18, 29, 47, ...
+fibonacci :: Tasks Applicative Integer Integer
+fibonacci n
+    | n >= 2 = Just $ \fetch -> (+) <$> fetch (n-1) <*> fetch (n-2)
+    | otherwise = Nothing
+
+-- Fibonacci numbers are a classic example of memoization: a non-minimal build
+-- system will take ages to compute f[100], doing O(f[100]) recursive calls.
+-- The right approach is to build the dependency graph and execute computations
+-- in the topological order.
+
+--------------------------- Task Monad: Ackermann ---------------------------
+
+-- Ackermann function:
+-- a[0, n] = n + 1
+-- a[m, 0] = a[m - 1, 1]
+-- a[m, n] = a[m - 1, a[m, n - 1]]
+-- Formally, it has no inputs, but we return Nothing for negative inputs.
+-- For example, a[m, 1] = 2, 3, 5, 13, 65535, ...
+ackermann :: Tasks Monad (Integer, Integer) Integer
+ackermann (n, m)
+    | m < 0 || n < 0 = Nothing
+    | m == 0    = Just $ const $ pure (n + 1)
+    | n == 0    = Just $ \fetch -> fetch (m - 1, 1)
+    | otherwise = Just $ \fetch -> do index <- fetch (m, n - 1)
+                                      fetch (m - 1, index)
+
+-- Unlike Collatz and Fibonacci computations, the Ackermann computation cannot
+-- be statically analysed for dependencies. We can only find the first dependency
+-- statically (Ackermann m (n - 1)), but not the second one.
+
+----------------------------- Spreadsheet examples -----------------------------
+
+sprsh1 :: Tasks Applicative String Integer
+sprsh1 "B1" = Just $ \fetch -> ((+)  <$> fetch "A1" <*> fetch "A2")
+sprsh1 "B2" = Just $ \fetch -> ((*2) <$> fetch "B1")
+sprsh1 _    = Nothing
+
+sprsh2 :: Tasks Monad String Integer
+sprsh2 "B1" = Just $ \fetch -> do c1 <- fetch "C1"
+                                  if c1 == 1 then fetch "B2" else fetch "A2"
+sprsh2 "B2" = Just $ \fetch -> do c1 <- fetch "C1"
+                                  if c1 == 1 then fetch "A1" else fetch "B1"
+sprsh2 _ = Nothing
+
+sprsh3 :: Tasks Alternative String Integer
+sprsh3 "B1" = Just $ \fetch -> (+) <$> fetch "A1" <*> (pure 1 <|> pure 2)
+sprsh3 _    = Nothing
+
+sprsh4 :: Tasks MonadFail String Integer
+sprsh4 "B1" = Just $ \fetch -> do
+    a1 <- fetch "A1"
+    a2 <- fetch "A2"
+    if a2 == 0 then fail "division by 0" else return (a1 `div` a2)
+sprsh4 _ = Nothing
+
+indirect :: Tasks Monad String Integer
+indirect key | key /= "B1" = Nothing
+             | otherwise   = Just $ \fetch -> do c1 <- fetch "C1"
+                                                 fetch ("A" ++ show c1)
+
+staticIF :: Bool -> Tasks Applicative String Int
+staticIF b "B1" = Just $ \fetch ->
+    if b then fetch "A1" else (+) <$> fetch "A2" <*> fetch "A3"
+staticIF _ _    = Nothing
+
+-------------------------- Dynamic programming example -------------------------
+
+data Key = A Integer | B Integer | D Integer Integer
+
+editDistance :: Tasks Monad Key Integer
+editDistance (D i 0) = Just $ const $ pure i
+editDistance (D 0 j) = Just $ const $ pure j
+editDistance (D i j) = Just $ \fetch -> do
+    ai <- fetch (A i)
+    bj <- fetch (B j)
+    if ai == bj
+        then fetch (D (i - 1) (j - 1))
+        else do
+            insert  <- fetch (D  i      (j - 1))
+            delete  <- fetch (D (i - 1)  j     )
+            replace <- fetch (D (i - 1) (j - 1))
+            return (1 + minimum [insert, delete, replace])
+editDistance _ = Nothing
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE OverloadedStrings, RankNTypes, ConstraintKinds #-}
+import Control.Monad
+import Data.Bool
+import Data.List.Extra
+import Data.Maybe
+import System.Exit
+
+import qualified Data.Map as Map
+
+import Build
+import Build.Rebuilder
+import Build.Store
+import Build.System
+import Build.Task
+
+import Spreadsheet
+import Examples()
+
+-- | A build system that acceptes a list of target keys.
+type MultiBuild c i k v = Tasks c k v -> [k] -> Store i k v -> Store i k v
+
+sequentialMultiBuild :: Build Monad i k v -> MultiBuild Monad i k v
+sequentialMultiBuild build task outputs store = case outputs of
+    []     -> store
+    (k:ks) -> sequentialMultiBuild build task ks (build task k store)
+
+sequentialMultiBuildA :: Build Applicative i k v -> MultiBuild Applicative i k v
+sequentialMultiBuildA build task outputs store = case outputs of
+    []     -> store
+    (k:ks) -> sequentialMultiBuildA build task ks (build task k store)
+
+inputs :: i -> Store i Cell Int
+inputs i = initialise i $ \cell -> fromMaybe 0 $ lookup cell
+    [ ("A1", 1)
+    , ("A2", 2)
+    , ("A3", 3) ]
+
+spreadsheet :: Spreadsheet
+spreadsheet cell = case name cell of
+    "B1"  -> Just $ 1                       --          1
+    "B2"  -> Just $ "B1" + 1                -- 1 + 1 == 2
+    "B3"  -> Just $ "A3" * abs "B2"         -- 3 * 2 == 6
+    "C1"  -> Just $ IfZero "B3" "C2" 1000   --          1000
+    "C2"  -> Just $ IfZero "B3" 2000 "C1"   --          1000
+    "C3"  -> Just $ Random 1 6              --          1..6
+    "F0"  -> Just $ 0                       --          0
+    "F1"  -> Just $ 1                       --          1
+    'F':_ -> Just $ rel (-1) 0 + rel (-2) 0 --          Fn = F(n - 1) + F(n - 2)
+    _     -> Nothing
+
+acyclicSpreadsheet :: Spreadsheet
+acyclicSpreadsheet cell = case name cell of
+    "B1"  -> Just $ 1                       --          1
+    "B2"  -> Just $ "B1" + 1                -- 1 + 1 == 2
+    "B3"  -> Just $ "A3" * abs "B2"         -- 3 * 2 == 6
+    "C1"  -> Just $ IfZero "B3" "B2" 1000   --          1000
+    "C2"  -> Just $ IfZero "B3" 2000 "C1"   --          1000
+    "C3"  -> Just $ Random 1 6              --          1..6
+    "F0"  -> Just $ 0                       --          0
+    "F1"  -> Just $ 1                       --          1
+    'F':_ -> Just $ rel (-1) 0 + rel (-2) 0 --          Fn = F(n - 1) + F(n - 2)
+    _     -> Nothing
+
+targets :: [Cell]
+targets = [ "A1", "A2", "A3", "B1", "B2", "B3", "C1", "C2", "F0", "F1", "F4" ]
+
+tasks :: Tasks Monad Cell Int
+tasks = spreadsheetTask spreadsheet
+
+tasksA :: Tasks Applicative Cell Int
+tasksA = spreadsheetTaskA acyclicSpreadsheet
+
+test :: String -> Build Monad i Cell Int -> i -> IO Bool
+test name build i = do
+    let store   = inputs i
+        result  = sequentialMultiBuild build tasks targets store
+        correct = all (correctBuild tasks store result) targets
+    putStr $ name ++ " is "
+    case (trim name, correct) of
+        ("dumb", False) -> do putStr "incorrect, which is [OK]\n"; return True
+        (_     , False) -> do putStr "incorrect: [FAIL]\n"       ; return False
+        (_     , True ) -> do putStr "correct: [OK]\n"           ; return True
+
+testA :: String -> Build Applicative i Cell Int -> i -> IO Bool
+testA name build i = do
+    let store   = inputs i
+        result  = sequentialMultiBuildA build tasksA targets store
+        correct = all (correctBuild tasks store result) targets
+    putStrLn $ name ++ " is " ++ bool "incorrect: [FAIL]" "correct: [OK]" correct
+    return correct
+
+testSuite :: IO Bool
+testSuite = and <$> sequence
+    [ test  "dumb      " dumb       ()
+    , test  "busy      " busy       ()
+    , test  "memo      " memo       ()
+    , testA "make      " make       (Map.empty, 0)
+    , testA "ninja     " ninja      mempty
+    , test  "excel     " excel      ((const True, const Unknown), mempty)
+    , test  "shake     " shake      mempty
+    , test  "bazel     " bazel      mempty
+    , test  "cloudShake" cloudShake mempty
+    , testA "buck      " buck       mempty
+    , test  "nix       " nix        mempty ]
+
+main :: IO ()
+main = do
+    success <- testSuite
+    unless success $ die "\n========== At least one test failed! ==========\n"
diff --git a/test/Spreadsheet.hs b/test/Spreadsheet.hs
new file mode 100644
--- /dev/null
+++ b/test/Spreadsheet.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE RankNTypes #-}
+module Spreadsheet where
+
+import Data.Bool
+import Data.Char
+import Data.Maybe
+import Data.String
+import Build.Store
+import Build.Task
+import Text.Read
+
+-- | A 'Cell' is described by a pair integers: 'row' and 'column'. We provide
+-- @IsString@ instance for convenience, so @"A8"@ corresponds to @Cell 8 0@.
+data Cell = Cell { row :: Int, column :: Int } deriving (Eq, Ord, Show)
+
+-- | Get the name of a 'Cell', e.g. @name (Cell 8 0) == "A8"@.
+name :: Cell -> String
+name (Cell r c) | c >= 0 && c < 26 = chr (c + ord 'A') : show r
+                | otherwise        = show (Cell r c)
+
+instance IsString Cell where
+    fromString string = case string of
+        columnChar : rowIndex -> Cell r c
+            where
+              r = fromMaybe fail (readMaybe rowIndex)
+              c | isAsciiUpper columnChar = ord columnChar - ord 'A'
+                | otherwise               = fail
+        _ -> fail
+      where
+        fail = error $ "Cannot parse cell name " ++ string
+
+instance Hashable Cell where
+    hash (Cell row column) = Cell <$> hash row <*> hash column
+
+-- | Some cells contain formulas for computing values from other cells. Formulas
+-- include:
+-- * 'Constant' integer values.
+-- * References to cells.
+-- * Simple arithmetic functions, such as 'Unary' negation and 'Binary' addition.
+-- * Conditional expressions 'IfZero' @x y z@ that evaluate to @y@ if @x@ is zero
+--   and to @z@ otherwise. Conditionals require dynamic dependencies to be handled
+--   correctly, because their static dependencies may form cycles. Example:
+--
+--   A1 = IfZero B1 A2 C1
+--   A2 = IfZero B1 C2 A1
+--
+--   Statically there is a mutual dependency between A1 and A2, but dynamically
+--   there is either A1 -> A2 or A2 -> A1.
+-- * Finally, there is a 'Random' formula that returns a random value in a
+--   specified range @[low..high]@. This introduces non-determinism, including
+--   failures when the range is empty.
+data Formula = Constant Int
+             | Reference Cell
+             | RelativeReference Int Int
+             | Unary (Int -> Int) Formula
+             | Binary (Int -> Int -> Int) Formula Formula
+             | IfZero Formula Formula Formula
+             | Random Int Int
+
+instance Num Formula where
+    fromInteger = Constant . fromInteger
+    (+)    = Binary (+)
+    (-)    = Binary (-)
+    (*)    = Binary (*)
+    abs    = Unary abs
+    signum = Unary signum
+
+instance IsString Formula where
+    fromString = Reference . fromString
+
+-- | A short alias for 'RelativeReference'.
+rel :: Int -> Int -> Formula
+rel = RelativeReference
+
+-- | A spreadsheet is a partial mapping of cells to formulas. Cells for which
+-- the mapping returns @Nothing@ are inputs.
+type Spreadsheet = Cell -> Maybe Formula
+
+-- TODO: Implement 'Random'.
+-- | Monadic spreadsheet computation.
+spreadsheetTask :: Spreadsheet -> Tasks Monad Cell Int
+spreadsheetTask spreadsheet cell@(Cell r c) = case spreadsheet cell of
+    Nothing      -> Nothing -- This is an input
+    Just formula -> Just $ evaluate formula
+  where
+    evaluate formula fetch = go formula
+      where go formula = case formula of
+                Constant x              -> pure x
+                Reference cell          -> fetch cell
+                RelativeReference dr dc -> fetch (Cell (r + dr) (c + dc))
+                Unary  op fx            -> op <$> go fx
+                Binary op fx fy         -> op <$> go fx <*> go fy
+                IfZero fx fy fz         -> do
+                    x <- go fx
+                    if x == 0 then go fy else go fz
+                Random _ _      -> error "Random not implemented"
+
+-- | Applicative spreadsheet computation.
+spreadsheetTaskA :: Spreadsheet -> Tasks Applicative Cell Int
+spreadsheetTaskA spreadsheet cell@(Cell r c) = case spreadsheet cell of
+    Nothing      -> Nothing -- This is an input
+    Just formula -> Just $ evaluate formula
+  where
+    evaluate formula fetch = go formula
+      where go formula = case formula of
+                Constant x              -> pure x
+                Reference cell          -> fetch cell
+                RelativeReference dr dc -> fetch (Cell (r + dr) (c + dc))
+                Unary  op fx            -> op <$> go fx
+                Binary op fx fy         -> op <$> go fx <*> go fy
+                IfZero fx fy fz         -> bool <$> go fz
+                                                <*> go fy
+                                                <*> ((==0) <$> go fx)
+                Random _ _      -> error "Random not implemented"