Monad Transformers for Backtracking Search
Jules Hedges
Queen Mary University of London
j.hedges@qmul.ac.uk
This paper extends Escardó and Oliva’s selection monad to the selection monad transformer, a general monadic framework for expressing backtracking search algorithms in Haskell. The use of the
closely related continuation monad transformer for similar purposes is also discussed, including an
implementation of a DPLL-like SAT solver with no explicit recursion. Continuing a line of work
exploring connections between selection functions and game theory, we use the selection monad
transformer with the nondeterminism monad to obtain an intuitive notion of backward induction for
a certain class of nondeterministic games.

1

Introduction

Selection functions are higher-order functions related to continuations, introduced by Martin Escardó
and Paulo Oliva in [6], with many remarkable properties. There are many intuitions that can be used to
understand selection functions, including viewing them as
• a generalised form of search algorithm
• a generalised notion of rationality
Selection functions form a monad, called the selection monad, which has an important intuition as a
refinement of the continuation monad that carries additional information. All of these intuitions will
be used in this paper. The monoidal product of the selection monad, called the product of selection
functions, can be used for several seemingly unrelated purposes:
1. In proof theory, it gives a computational meaning to the negative translation of the axiom of countable choice [6]
2. In synthetic topology, it is a computational form of Tychonoff’s theorem [4]
3. In functional programming, it provides a monadic framework for backtracking search problems
[7]
4. In game theory, it is a generalisation of the backward induction algorithm [9]
In this paper we are concerned with points (3) and (4).
The intuition behind (3) is that a selection function is a generalised search algorithm, inputting a ‘generalised predicate’ characterising objects to be found, and outputting an object that satisfies the predicate
if one exists. The purpose of the product of selection functions is to combine search algorithms for
simple search spaces into search algorithms for more complex search spaces. This has been used to derive so-called seemingly impossible functional programs which search certain infinite (but topologically
compact) data types in finite time [3].
For (4) we have a powerful intuition that a selection function is a generalised form of preference
for rational agents in game theory [10]. Indeed the arg max operator, which characterises the behaviour
of classical economic agents, is one of the canonical examples of a selection function. The product
N.R. Krishnaswami and P.B. Levy (Eds.):
Mathematically Structured Functional Programming 2014 (MSFP 2014).
EPTCS 153, 2014, pp. 31–50, doi:10.4204/EPTCS.153.3

Monad Transformers for Backtracking Search

32

of selection functions applied to copies of arg max is precisely the backward induction algorithm, used
to compute subgame-perfect Nash equilibria of sequential games [9], and we can transfer this gametheoretic intuition to other instances of the product of selection functions. An introduction to selection
functions written from this point of view is [8].
Part 2 of this paper is an introduction to selection functions and the Haskell implementation of the
continuation and selection monads. In part 3 we show the use of the continuation monad, rather than
the selection monad, for writing search algorithms in Haskell, and the use of the continuation monad
transformer to express more advanced search algorithms such as DPLL. In part 4 we define the selection
monad transformer and show its relationship to the ordinary selection monad and the continuation monad
transformer. Part 5 defines nondeterministic sequential games, and in part 6 we use the monoidal product
of the selection monad transformer, applied to the nondeterminism monad, to give an intuitive notion of
backward induction for these games.
This paper uses two different notations, namely Haskell and ‘naive type theory’, which can be read
either as ordinary set theory or as functional pseudocode. To make it easy to distinguish the notations, Haskell code is set in a box . There are three appendices listing Haskell code verbatim: appendix
Appendix A contains the DPLL implementation (part 3), Appendix B contains the selection monad transformer library (part 4) and Appendix C contains an example nondeterministic game (parts 5 and 6). All
of this code can be downloaded from the author’s homepage1 .

2

Quantifiers and selection functions

A selection function is defined to be any function with a type of the form

ε : JR X
where the selection monad JR is defined as
JR X = (X → R) → X
or, in Haskell notation,

data Sel r x = Sel {runSel :: (x → r) → x}

There is a close relationship between the selection monad and the well-known continuation monad
KR X = (X → R) → R
which in Haskell is

data Cont r x = Cont {runCont :: (x → r) → r}

1 http://www.eecs.qmul.ac.uk/

~ julesh/

Jules Hedges

33

(Note that in Haskell the constructor of Cont is written cont as a consequence of the continuation monad
being, in reality, defined in terms of the continuation monad transformer.) A function ϕ : KR X is called
a quantifier. Every selection function ε : JR X induces a quantifier ε : KR X by

ε p = p(ε p)
This operation is a monad morphism from JR to KR . When ϕ is a quantifier satisfying ϕ = ε we say
that ε attains ϕ . Not every quantifier is attainable, for example a constant quantifier ϕ p = r0 is not
attainable because we can find some p : X → R such that r0 is not in the image of p. However many
important quantifiers are attainable, and in those cases selection functions offer several advantages.
The canonical examples of quantifiers are the maximum operator max : KR X for a finite set X defined
by
max p = max px
x∈X

and the existential quantifier ∃ : KB X , where B = {⊥, ⊤}, defined by
(
⊤ if px = ⊤ for some x ∈ X
∃p =
⊥ otherwise
Both of these quantifiers are attained: max is attained by the operator arg max which produces a point at
which p attains its maximum, and ∃ is attained by Hilbert’s ε operator. Another interesting example is
the integral operator
Z
: KR [0, 1]

defined by

Z

p=

Z 1

px dx

0

A combination of the mean value theorem and the axiom of choice proves that this quantifier is attained.
This example is interesting because a computable quantifier is attained by a noncomputable selection
function (the selection function arg max also has this property if we replace the finite set X with a compact
topological space with infinitely many points, such as the unit interval).
All monads M (note the term monad will always mean strong monad in this paper) have a monoidal
product
⊗ : MX × MY → M(X ×Y )
which can be expressed in terms of unit and bind. (In fact there are always two monoidal products, but
we are interested only in one of them.) A monomorphic iterated form of this product is present in the
Haskell prelude as

sequence :: (Monad m) =⇒ [m a] → m [a]

It is important to note that due to the restrictions of Haskell’s type system we can only take the iterated
product of selection functions and continuations which have the same type. In a dependently typed
language we could express the general product, which for selection functions has type
O

: ∏ JR Xi → JR ∏ Xi
i

i

Monad Transformers for Backtracking Search

34

For the continuation monad the binary product is given by
(ϕ ⊗ ψ )q = ϕ (λ xX .ψ (λ yY .q(x, y)))
As special cases this includes min-maxes in game theory, composition of logical quantifiers such as
∃xX ∀yY .q(x, y), and multiple integration over products of [0, 1], as well as combinations of these such as
max
x∈X

Z 1

q(x, y) dy

0

The product of selection functions is a more complex operation, given in [8] by
(ε ⊗ δ )q = (a, ba )
where
a = ε (λ xX .q(x, bx ))
bx = δ (λ yY .q(x, y))
Because the overline operation is a monad morphism it commutes with the monoidal products:

ε ⊗δ = ε ⊗δ
In other words, if ε attains ϕ and δ attains ψ then ε ⊗ δ attains ϕ ⊗ ψ .
One of the most important and remarkable properties of selection functions is that the product of
selection functions is well-defined when iterated infinitely, so long as R is compact and q is continuous.
Moreover the Haskell function sequence specialised to the selection monad will terminate on an infinite
list, provided the Haskell datatype r is compact in the sense of [4], since computable functions are
continuous. Other well-known monads, including the continuation monad, do not have this property.
Finite discrete types such as Bool are compact, and an example of an infinite compact type is Int → Bool,
which corresponds to the Cantor space 2ω . An example of a type which is not compact is Int.

3

SAT solving with the continuation monad transformer

In this section we investigate the use of the continuation monad transformer for structuring backtracking
search algorithms. (For the ordinary continuation monad this is implicit in the work of Escardó and
Oliva.) In general, for the decision version of a search problem the continuation monad can be used.
One advantage of this approach is that these monads are better-known and are part of a standard Haskell
installation. A more tangible advantage is that using the continuation monad is likely to be more efficient
(although the runtime of these algorithms is generally unknown). However, the main reason for this
section is simply to investigate putting the continuation monad transformer to a use for which it was not
originally intended.
The selection function

ε :: Sel Bool Bool
ε = Sel $ λ p → p True

Jules Hedges

35

will solve a simple optimisation problem: given a function p :: Bool → Bool the selection function ε
will find x making p x true, if one exists. Then

sequence $ repeat ε

will, given a function q :: [Bool] → Bool , find xs making q xs true, if one exists (recall that the Haskell
function repeat builds infinite lists). In other words, this function will find satisfying assignments of
propositional formulas. The correctness and totality of this function is far from obvious! The most
direct proof is by bar induction (specifically, induction on the modulus of continuity of q) but a far more
intuitive proof method is to view the search problem as an unbounded sequential game and apply theorem
6.2 of [8].
However, the classical SAT problem is only to decide whether a satisfying assignment exists, rather
than to actually compute one. By construction, if a formula q has a satisfying assignment then (⊗i ε )q is
a satisfying assignment. Therefore q is satisfiable iff q((⊗i ε )q) is true, that is, if (⊗i ε )q is true. If the
product is finite this is equal to (⊗i ∃)q, and ∃ can be written directly in Haskell as

∃ :: Cont Bool Bool
∃ = cont $ λ p → p $ p True

Using sequence for the monoidal product yields an extremely small, self-contained Haskell SAT solver:

import Control.Monad.Cont
sat n = runCont $ sequence $ replicate n $ cont $ λ p → p $ p True

The type is sat :: Int → ([Bool] → Bool) → Bool , so it is not a true SAT solver in the sense that
it takes its input as a function [Bool] → Bool rather than in a discrete form such as a clause-set. The
other input is the number of variables to search, which is necessary because sequence specialised to
continuations will diverge on infinite lists. It is also important to stress that this algorithm is not a SAT
solver written in continuation-passing style, rather it uses the continuation monad to directly represent
the recursion.
Using the continuation monad transformer we can begin to refine this algorithm, for example we can
write a DPLL-like algorithm using a state monad to store clause-sets. The DPLL algorithm, introduced
in [2], decides the satisfiability of CNF-formulas by successively extending the formula with either a
literal or its negation, and at each stage applying two simplifying transformations, namely unit clause
propagation and pure literal elimination. Most modern SAT solvers are based on DPLL combined with
various heuristics to improve average-case complexity, see for example [11].
For simplicity we implement only unit clause propagation. The algorithm we will implement is
represented in imperative pseudocode in algorithm 1.
We begin with a datatype representing literals:

Monad Transformers for Backtracking Search

36
Algorithm 1 Imperative DPLL algorithm
function DPLL(ϕ )
if ϕ is an empty clause-set then
return True
end if
if ϕ contains the empty clause then
return False
end if
while ϕ contains a unit clause l do
for each clause c in ϕ do
if c contains l then
ϕ ← remove c from ϕ
end if
if c contains l then
c ← remove l from c
end if
end for
end while
l ← next literal
return DPLL(ϕ ∧ l) ∨ DPLL(ϕ ∧ l)
end function

data Literal = Positive Int | Negative Int

so the type of a clause-set is [[Literal]]. The top-level function will be

dpll :: Int → [[Literal]] → Bool
dpll n = evalState s . initialState
where
s :: State DPLL Bool
s = runContT (sequence $ replicate n ϕ ) q

ϕ :: ContT Bool (State DPLL) Bool
ϕ = ContT $ λ p → p True >>= p

Notice that in ϕ the expression p $ p True is replaced by its monad transformer equivalent p True >>= p .
The type DPLL must represent the state used by the DPLL algorithm, and we need a function
initialState :: [[Literal]] → DPLL . Most of the actual algorithm is contained in the query function

Jules Hedges

37

q :: [Bool] → State DPLL Bool

The implementation of this function is given in appendix Appendix A. It is important to note that the
monad transformer stack ContT Bool (State DPLL) will thread a single state through an entire search,
however for the DPLL algorithm we want to create a new copy of the state for every recursive call. We
achieve this by representing the recursion tree explicitly, making the state type DPLL a type of binary
trees with leaves labelled by the necessary data. The idea is that the function q will move up the tree
according to its input, interpreting True as ‘go left’ and False as ‘go right’. If it finds a leaf labelled by
a clause set for which satisfiability is trivial, the function returns. If not, it extends the tree according to
the remaining input. A full implementation is presented in appendix Appendix A.
As written, this program is not particularly efficient. Potentially we could use the IO monad rather
than State, and produce an optimised SAT solving algorithm for example by storing the clause sets as
arrays rather than lists. However optimised SAT solvers and other search algorithms require explicit
control over the backtracking, which is precisely what the continuation and selection monads do not
allow. In [1] is presented an alternative implementation of the product of selection functions that allows
explicit control over backtracking. See the next section for a discussion of how sequence explores a
search space.

4

The selection monad transformer

In creating a selection monad transformer, our guiding example is the generalisation in the Haskell monad
transformer library from the continuation monad
KR X = (X → R) → R
to the continuation monad transformer
KRM X = KMR X = (X → MR) → MR
Paralleling this, the selection monad
JR X = (X → R) → X
is generalised to the selection monad transformer
JRM X = (X → MR) → MX
The Haskell code for the monad instance is

38

Monad Transformers for Backtracking Search

data SelT r m x = SelT {runSelT :: (x → m r) → m x}
instance (Monad m) =⇒ Monad (SelT r m)
where
return = SelT . const . return
ε >>= f = SelT $ λ p → let
g x = runSelT (f x) p
h x = g x >>= p
in
runSelT ε h >>= g

This comes from taking the instance declaration for the ordinary selection monad and replacing certain function applications with the monadic bind of m. Similarly we obtain a monad morphism from
selections to continuations by replacing a function application with monadic bind:

toCont :: (Monad m) =⇒ SelT r m x → ContT r m x
toCont ε = ContT $ λ p → runSelT ε p >>= p

In type-theoretic notation we continue to write this operation as an overline ε . A full code listing is given
in appendix Appendix B.
The proof that the selection monad satisfies the monad laws was found using an ad-hoc computer
program written by Martin Escardó based on an algorithm for deciding β η -equivalence of λ -terms,
and is linked from [5]. The author has verified by hand that the selection monad transformer preserves
the unit laws, however the proof for the associativity law appears to be unmanageable. The author is
currently working on a formally verified proof that the selection monad transformer preserves the monad
laws.
A simple but extremely useful example is to use JRIO to perform a verbose backtracking search,
laying bare the subtle behaviour of the product of selection functions which could previously only be
investigated using unsafePerformIO. For example we can write a function

verboseQuery :: ([Bool] → Bool) → [Bool] → IO Bool

which will print information about the query and its result before returning. Then a verbose SAT solver
is given by

Jules Hedges

39

verboseSat :: Int → ([Bool] → Bool) → IO [Bool]
verboseSat n = f . verboseQuery
where
f :: ([Bool] → IO Bool) → IO [Bool]
f = runSel $ sequence $ replicate n ε
ε :: SelT Bool IO Bool
ε = SelT ($ True)

Experiments with this function confirm that sequence will prune large parts of a search space when it is
able to, but it also duplicates a certain amount of work, potentially calling q on the same input several
times. It also sometimes continues to call q even after it has found a satisfying assignment (that is, after
verboseQuery has printed the result True). The problem of explaining exactly how sequence explores a
search space is still open, although the experimental data provided by verboseSAT and related functions
may make progress possible. The interested reader is encouraged to download the code samples and
experiment with this function interactively.

5

Nondeterministic sequential games

In the remaining two sections we write X ⇒ Y for the type of nondeterministic total functions from X
to Y . This is equal to the Kleisli arrow X → P>0Y where P>0 is the nondeterminism monad, whose
underlying functor is the covariant nonempty powerset functor. In Haskell we replace P>0 with the
list monad for simplicity. In order to distinguish between the use of the list monad as ‘poor man’s
nondeterminism’ and its ordinary use as an ordered data structure (such as for an ordered list of moves
in a game) we use a type synonym
type P>0 a = [a]
(From a software engineering point of view it would be far better to introduce P>0 as a newtype, but
using a type synonym allows us to use the usual list functions to manipulate sets without boilerplate
code.)
Definition 1 (Finite nondeterministic sequential game). An n-player sequential game consists of types
X1 , . . . , Xn of moves, a type R of outcomes and an outcome function
n

q : ∏ Xi → R
i=1

∏ni=1 Xi ,

and q(x1 , . . . , xn ) is called the outcome of the play.
A play of the game is a tuple (x1 , . . . , xn ) ∈
In a nondeterministic sequential game, we instead take the outcome function to be a nondeterministic
function
n

q : ∏ Xi ⇒ R
i=1

and we consider q(x1 , . . . , xn ) to be the set of all possible outcomes of the play (x1 , . . . , xn ).

Monad Transformers for Backtracking Search

40

In classical game theory the outcome type will be Rn , and then we interpret the ith element of the
tuple q(x1 , . . . , xn ) to be the profit of the ith player.
As a running example, we will consider a simple 2-player nondeterministic game implemented in
Haskell, the full code of which is presented in appendix Appendix C. Each player has a choice of moves
given by

data Move = Cautious | Risky

The game will be zero-sum, so its outcome will be a single integer with the first player maximising
and the second minimising. The nondeterministic outcome function will be given by

type Outcome = Int
q
:: [Move] → P>0 Outcome
q [Cautious, Cautious] = [0]
q [Cautious, Risky]
= [−1, 0, 1]
q [Risky, Cautious]
= [−1, 0, 1]
q [Risky, Risky]
= [−2, −1, 0, 1, 2]

Consider the ith player of a game deciding which moves to play, having observed the previous moves
x1 , . . . , xi−1 . Assuming that the players to follow are playing according to certain constraints (such as
rationality) which are common knowledge, the player can associate to each possible move xi a set of outcomes which may result after the other players’ moves. Thus the player has a nondeterministic function
Xi ⇒ R, which we call the context of player i’s move.
Definition 2 (Policies of players). An outcome policy for player i is a rule that associates each context
p : Xi ⇒ R with a set of outcomes which the player considers to be good following that context. Thus an
outcome policy for player i is a quantifier with type

ϕi : KRP>0 Xi
A move policy for player i is a rule which, given a context, nondeterministically chooses a move.
Thus a move policy for player i is a selection function with type

εi : JRP>0 Xi
A move policy εi is called rational for an outcome policy ϕi if for every context p and every move x
that may be selected by the move policy, every outcome that could result from the context given that move
is a good outcome. Symbolically,
{r ∈ px | x ∈ εi p} ⊆ ϕi p
The left hand side of this is precisely εi p, where · is the monad morphism JRP>0 → KRP>0 . (However
the subset relation prevents us from obtaining a game-theoretic interpretation of more general instances
of the selection monad transformer.)

Jules Hedges

41

An outcome policy is called realistic iff, for every context, there is a move such that every possible
outcome of that move in that context is a good outcome. In other words, an outcome policy is realistic iff
it has a rational move policy.
It was pointed out by an anonymous referee that this definition of realistic is equivalent, using the
axiom of choice, to the existence of an ordinary (deterministic) selection function εi : (X → P>0 R) → X
with the property that p(εi p) ⊆ ϕi p. It is then possible to replace P>0 R with an arbitrary poset and
continue using only ordinary quantifiers and selection functions. However, the point intuitively is that
since we are working with nondeterministic games it makes more sense to allow the players to choose
moves nondeterministically, rather than using the axiom of choice to ‘determinise’ the move choices.
More concretely, it should be possible to construct outcome policies with a computable rational move
policy but no computable selection function with this property, at least if we use true nondeterminism
rather than approximating it with lists.
For deterministic games there are canonical realistic outcome policies in the case when the outcome
type is Rn , namely maximisation with respect to the ordering of R:

ϕi p = max(px)i
x∈Xi

where (px)i is the ith coordinate projection of the vector px : Rn . However for nondeterministic games
there is no canonical policy, even when the outcome type is R: a player might always choose x such that
px contains the largest possible element, or they might have a more complicated policy to mitigate risk,
for example preferring possible outcomes {5} to {10, −100}. We leave this undetermined and allow the
policies to be arbitrary.
We will consider two pairs of move policies for the example game, also called cautious and risky.
For the implementation of these we begin with the type

type Choice = P>0 (Move, P>0 Outcome) → (Move, P>0 Outcome)

representing ‘choice functions’ which, given a set of move-outcome pairs, will choose one. Next we write
a function called argopt, which is a generic way to convert a choice function into a selection function.

argopt :: Choice → SelT Outcome P>0 Move
argopt f = SelT $ λ p → [fst $ f [(Cautious, p Cautious), (Risky, p Risky)]]

It should be noted that Haskell does not allow a type synonym with a free type variable to be used as a
parameter, so SelT Outcome P>0 Move must be written SelT Outcome [] Move in real code.
Now we implement our two pairs of choice functions:

riskymax, riskymin, cautiousmax, cautiousmin :: Choice
riskymax
= maximumBy $ comparing $ maximum . snd
riskymin
= minimumBy $ comparing $ minimum . snd

Monad Transformers for Backtracking Search

42

= riskymax . filter (all (≥ (−1)) . snd)
= riskymin . filter (all (≤ 1) . snd)

cautiousmax
cautiousmin

In words, the risky move policies will select moves to maximise the player’s maximum possible gain
(which for the second player is minimising the minimum outcome), ignoring the risk of bad outcomes.
The cautious move policies do likewise, but avoid moves that lead to the possibility of the worst possible
outcome, which is ±2. The risky move policies are deterministic in the sense that they always return
a list of length 1. The cautious move policies also have this property for the particular game we are
considering, but not in general (indeed, as written the functions cautiousmax and cautiousmin are partial
functions: if the filter returns an empty list then an exception will be thrown).
Definition 3 (Strategy). A strategy for player i in a game is a function
i−1

σi : ∏ X j → Xi
j=1

which chooses a move given the observed previous moves. For a nondeterministic sequential game we
take the strategies to be nondeterministic functions
i−1

σi : ∏ X j ⇒ Xi
j=1

Thus in particular a strategy for player 1 is σ1 : P>0 X1 . A tuple σ containing a strategy for each player
is called a strategy profile.
We can understand this definition intuitively by imagining that nondeterminism is resolved at several
points during the course of playing a game. First, player 1 nondeterministically chooses a move. Then
the nondeterminism resolves, and some concrete move is played. Player 2 observes the actual move
that was played, and nondeterministically chooses a move, and so on. Eventually, after all players have
moved, we obtain a concrete play (x1 , . . . , xn ). Then the rules of the game nondeterministically determine
an outcome, and finally this nondeterminism resolves to produce the actual outcome.

6

Backward induction for nondeterministic games

Now we need to define what it means for a strategy profile to be optimal. In game-theoretical language
an optimal strategy profile is called a subgame-perfect Nash equilibrium.
Intuitively, a strategy profile is optimal if for all players i and all partial plays up to player i − 1,
every outcome that could result from playing the strategy profile is a good outcome in the context which,
following player i’s move, the remaining players play according to the strategy profile.
We spell out this definition explicitly. Given a partial play ~x = (x1 , . . . , xi−1 ), the set all moves that
might be made by player i ≤ j ≤ n by playing the strategy profile σ is given inductively by
b~xj = {x ∈ σ j (~x, xi , . . . , x j−1 ) | xk ∈ b~xk , i ≤ k < j}
which in monad notation is
b~xj

=

j−1
O
k=i

b~xk

!

>>= σ j~x

Jules Hedges

43

where ⊗ is the monoidal product of M, which for M = P>0 is the cartesian product. The set of all
outcomes that might result from playing the strategies σ on the partial play ~x is
{r ∈ q(~x, xi , . . . , xn ) | xk ∈ b~xk , i ≤ k ≤ n}
Now we need to define the context in which player i chooses a move. Suppose after the partial play ~x,
player i chooses the move x ∈ Xi . The set of outcomes that could result from this is simply the result of
the previous calculation applied to the partial play (~x, x), namely
{r ∈ q(~x, x, xi+1 , . . . , xn ) | xk ∈ b~x,x
k , i < k ≤ n}
Definition 4 (Optimal strategy profile). A strategy profile σ is called optimal for given outcome policies
ϕi if for all partial plays ~x = (x1 , . . . , xi−1 ) for 1 ≤ i ≤ n we have
{r ∈ q(~x, xi , . . . , xn ) | xk ∈ b~xk , i ≤ k ≤ n} ⊆ ϕi p
where the context p : Xi ⇒ R is defined by
px = {r ∈ q(~x, x, xi+1 , . . . , xn ) | xk ∈ b~kx,x , i < k ≤ n}
Notice that an optimal strategy profile guarantees good outcomes for all players, despite the nondeterminism. In order for this to hold there must be enough good outcomes, for which it is sufficient that
the outcome policies are realistic.
Theorem 1. A nondeterministic sequential game in which all players’ outcome policies are realistic has
an optimal strategy profile.
If the players’ move policies are εi and the outcome function is q then an optimal strategy profile is
given by
!
!

σi~x = πi

n
O

ε j (q~x )

j=i

where ⊗ is the monoidal product in the monad JRP>0 , q~x is the partial application of q to ~x, and πi is the
projection onto Xi . These can be computed in Haskell by
strategy es q xs = head $ runSelT ε (q . (xs ++))
where
ε = sequence $ drop (length xs) es

Moreover the set of all plays which may occur from playing this strategy profile is given by
!
n
O
i=1

which is computed in list form by the program

εi q

Monad Transformers for Backtracking Search

44

plays = runSelT . sequence

The corresponding expression using the monoidal product in JR was shown in [9] to be a generalisation of backward induction, a standard and intuitive algorithm in classical game theory to find
equilibria of sequential games. By taking the monoidal product in JRP>0 , we also gain a generalisation
of backward induction to nondeterministic games.
It was remarked above that the appearance of the subset relation in the definition of rational move
policies and optimal strategy profiles prevents us from giving these definitions for an arbitrary monad M.
The definition given applies to submonads of the nondeterminism monad, which include finite nondeterminism (finite lists), the exception (Maybe) monad and the identity monad (in which case we get Escardó
and Oliva’s definitions). It might be possible to interpret the subset relation for some other monads in ad
hoc ways, for example as a refinement relation for the IO monad, which should have a game-theoretic
meaning as games which interact with an environment outside of the game. However, the given expressions and Haskell functions to compute optimal strategy profiles works for any M, so we can say that
this strategy profile is always optimal, despite having no general definition. It remains to be seen what
game-theoretic intuition exists for the many different monads that are available.
We need to find an explicit expression for the monoidal product
⊗ : JRM X × JRMY → JRM (X ×Y )
Starting with the usual expression for the product of selection functions
(ε ⊗ δ )q = (a, ba )
where
a = ε (λ xX .q(x, bx ))
bx = δ (λ yY .q(x, y))
we replace a function application with monadic bind, and the cartesian pairing with the monoidal product
⊗ of M, yielding
(ε ⊗ δ )q = a ⊗ (a >>= λ xX .bx )
where
a = ε (λ xX .(bx >>= λ yY .q(x, y)))
bx = δ (λ yY .q(x, y))
It will be helpful to write q in a curried form, in which case we have
a = ε (λ xX .(bx >>= qx))
bx = δ (qx)
We prove the theorem in the simple case of a 2-move sequential game. Let the move types be X
and Y , so the outcome function has type q : X × Y ⇒ R. Let the outcome policies be ϕ : KRP>0 X and

Jules Hedges

45

ψ : KRP>0 Y , and the rational move policies be ε : JRP>0 X and δ : JRP>0 Y . We need to prove that the
strategy profile
σX = {x ∈ X | (x, y) ∈ (ε ⊗ δ )q}
σY x = δ (qx)
is optimal. Using the explicit expression for the monoidal product we have
(ε ⊗ δ )q = {(x, y) ∈ X ×Y | x ∈ a, y ∈ bx }
where
a = ε (λ x.{r ∈ q(x, y) | y ∈ bx })
bx = δ (qx)
therefore the first player’s strategy is given directly by

σX = a
We can directly calculate
()

bX = a
()

bY = {y ∈ δ (qx) | x ∈ a}
(x)

bY = δ (qx)
The conditions we need to verify are
1. {r ∈ q(x, y) | x ∈ a, y ∈ δ (qx)} ⊆ ϕ (λ x.{r ∈ q(x, y) | y ∈ δ (qx)})
2. For all x : X , {r ∈ q(x, y) | y ∈ δ (qx)} ⊆ ψ (qx)
Since δ is a rational move policy for ψ we have {r ∈ py | y ∈ δ p} ⊆ ψ p for all contexts p : Y ⇒ R. Using
the context py = q(x, y) gives the second condition. For the first condition we take the context
px = {r ∈ q(x, y) | y ∈ δ (qx)}
so that a = ε p. Then we have
{r ∈ q(x, y) | x ∈ a, y ∈ δ (qx)}
= {r ∈ px | x ∈ ε p}
⊆ ϕp
= ϕ (λ x.{r ∈ q(x, y) | y ∈ δ (qx)})
This completes the proof.
For the example game the optimal plays can be computed interactively:

Monad Transformers for Backtracking Search

46

plays [argopt cautiousmax, argopt cautiousmin] q
=⇒ [[Risky, Cautious]]
plays [argopt cautiousmax, argopt riskymin] q
=⇒ [[Cautious, Risky]]
plays [argopt riskymax, argopt cautiousmin] q
=⇒ [[Risky, Cautious]]
plays [argopt riskymax, argopt riskymin] q
=⇒ [[Risky, Risky]]

Thus, each combination of cautious and risky move policies results in a different deterministic play. The
intuition behind these results is that the ‘personality’ defined by a move policy is common knowledge
of the players. The only possibly unexpected result is the first, when both players are cautious. In this
case the first player plays risky because she knows that the second player will avoid the maximum risk,
meaning the risky move is safe.
Acknowledgement The author gratefully acknowledges EPSRC grant EP/K50290X/1 which funded
this work.

Appendix A

DPLL implementation

import Data.List
import Control.Monad.State
import Control.Monad.Trans.Cont
-- Literals
data Literal = Positive Int | Negative Int deriving (Show, Eq)
negateLiteral :: Literal -> Literal
negateLiteral (Positive n) = Negative n
negateLiteral (Negative n) = Positive n
-- Internal state of algorithm
data DPLL = Leaf {simplified :: Bool, clauses :: [[Literal]]}
| Node {trueBranch :: DPLL, falseBranch :: DPLL}
-- Top level of algorithm
dpll :: Int -> [[Literal]] -> Bool
dpll n = evalState s . initialState where
s = runContT (sequence $ replicate n e) q
e :: ContT Bool (State DPLL) Bool

Jules Hedges

47

e = ContT $ \p -> p True >>= p
q :: [Bool] -> State DPLL Bool
q bs = do s <- get
let (s’, b) = queryState s bs 0
put s’
return b
-- Interactions with internal state
initialState :: [[Literal]] -> DPLL
initialState cs = Leaf {simplified = False, clauses = cs}
queryState
queryState
queryState
queryState
queryState

:: DPLL -> [Bool] -> Int -> (DPLL, Bool)
(Leaf False cs) bs n = queryState (Leaf True $ simplify cs) bs n
s@(Leaf True []) _ _ = (s, True)
s@(Leaf True [[]]) _ _ = (s, False)
(Leaf True cs) bs n = queryState (Node l r) bs n where
l = Leaf False ([Negative n] : cs)
r = Leaf False ([Positive n] : cs)
queryState (Node l r) (True : bs) n = (Node l’ r, b) where
(l’, b) = queryState l bs (n + 1)
queryState (Node l r) (False : bs) n = (Node l r’, b) where
(r’, b) = queryState r bs (n + 1)
-- Operations on clause sets
simplify :: [[Literal]] -> [[Literal]]
simplify cs = if null units
then cs
else simplify (foldl (flip propagateUnit) cs’ units) where
(units, cs’) = partition isUnitClause cs
isUnitClause :: [Literal] -> Bool
isUnitClause [_] = True
isUnitClause _ = False
propagateUnit :: [Literal] -> [[Literal]] -> [[Literal]]
propagateUnit [l] = (map $ filter (/= negateLiteral l))
. (filter $ notElem l)

Appendix B

The selection monad transformer library

-- Selection monad transformer library
-- A generic backtracking search and auto-pruning library

Monad Transformers for Backtracking Search

48

module SelT (SelT(..), Sel, toCont,
boundedBinarySearch, unboundedBinarySearch) where
import Control.Monad.Cont
import Data.Functor.Identity
-- Selection monad transformer
newtype SelT r m x = SelT {runSelT :: (x -> m r) -> m x}
instance (Monad m) => Monad (SelT r m) where
return = SelT . const . return
e >>= f = SelT $ \p -> let g x = runSelT (f x) p
h x = g x >>= p
in runSelT e h >>= g
instance (MonadIO m) => MonadIO (SelT r m) where
liftIO = lift . liftIO
instance MonadTrans (SelT r) where
lift = SelT . const
-- Monad morphism from selections to continuations
toCont :: (Monad m) => SelT r m x -> ContT r m x
toCont e = ContT $ \p -> runSelT e p >>= p
-- Vanilla selection monad
type Sel r = SelT r Identity
-- Generic search functions
unboundedBinarySearch :: (Monad m) => SelT Bool m [Bool]
unboundedBinarySearch = sequence $ repeat $ SelT ($ True)
boundedBinarySearch :: (Monad m) => Int -> SelT Bool m [Bool]
boundedBinarySearch n = sequence $ replicate n $ SelT ($ True)

Appendix C

Example game

import SelT
import Data.List (maximumBy, minimumBy)
import Data.Ord (comparing)

Jules Hedges

49

data Move
= Cautious | Risky deriving (Show)
type Outcome = Int
type P a = [a]
q
q
q
q
q

:: [Move] -> P Outcome
[Cautious, Cautious] =
[Cautious, Risky]
=
[Risky, Cautious]
=
[Risky, Risky]
=

[0]
[-1, 0, 1]
[-1, 0, 1]
[-2, -1, 0, 1, 2]

type Choice = P (Move, P Outcome) -> (Move, P Outcome)
argopt :: Choice -> SelT Outcome [] Move
argopt f = SelT $ \p -> [fst $ f [(Cautious, p Cautious), (Risky, p Risky)]]
riskymax, riskymin, cautiousmax, cautiousmin :: Choice
riskymax = maximumBy $ comparing $ maximum . snd
riskymin = minimumBy $ comparing $ minimum . snd
cautiousmax = riskymax . filter (all (>= (-1)) . snd)
cautiousmin = riskymin . filter (all (<= 1) . snd)
es1, es2, es3, es4 :: [SelT Outcome [] Move]
es1 = [argopt riskymax, argopt riskymin]
es2 = [argopt riskymax, argopt cautiousmin]
es3 = [argopt cautiousmax, argopt riskymin]
es4 = [argopt cautiousmax, argopt cautiousmin]
solve :: [SelT Outcome [] Move] -> P [Move]
solve es = runSelT (sequence es) q

References
[1] Andrej Bauer & Matija Pretnar (2012): Programming with algebraic effects and handlers. Available at
http://math.andrej.com/2012/03/08/programming-with-algebraic-effects-and-handlers/.
[2] Martin Davis, George Logemann & Donald Loveland (1960): A machine program for theorem proving.
Communications of the ACM 5(7), pp. 394–397, doi:10.1145/368273.368557.
[3] Martin Escardó (2007):
Seemingly impossible functional programs.
Available
http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/.

at

[4] Martin Escardó (2008): Exhaustible sets in higher-type computation. Logical methods in computer science
4(3:3), pp. 1–37, doi:10.2168/lmcs-4(3:3)2008.
[5] Martin Escardó (2008): A Haskell monad for infinite search in finite time.
Available at
http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/.
[6] Martin Escardó & Paulo Oliva (2010): Selection functions, bar recursion and backward induction. Mathematical structures in computer science 20(2), pp. 127–168, doi:10.1017/S0960129509990351.

50

Monad Transformers for Backtracking Search

[7] Martin Escardó & Paulo Oliva (2010): What sequential games, the Tychonoff theorem and the doublenegation shift have in common. Proc. of 3rd ACM SIGPLAN Wksh. on Mathematically Structured Functional
Programming, doi:10.1145/1863597.1863605.
[8] Martin Escardó & Paulo Oliva (2011): Sequential games and optimal strategies. Proc R Soc A 467, pp.
1519–1545, doi:10.1098/rspa.2010.0471.
[9] Martin Escardó & Paulo Oliva (2012): Computing Nash equilibria of unbounded games. Proceedings of the
Turing centenary conference.
[10] Jules Hedges (2013): A generalisation of Nash’s theorem with higher-order functionals. Proc R Soc A
469(2154), doi:10.1098/rspa.2013.0041.
[11] Joao Marques-Silva, Ines Lynce & Sharad Malik (2008): Conflict-driven clause learning SAT solvers. In
Armin Biere, Marijn Heule, Hans van Maaren & Toby Walsch, editors: Handbook of satisfiability, chapter 4,
IOS Press.

