Not a monad (Programming Languages)

From Spivey's Corner
Jump to: navigation, search

This note gives an example of a structure that looks like a monad, but fails to obey the monad laws. The result of using it as the basis of an interpreter is a programming language that behaves in unpredictable ways.

A factoring program

Here's a program (written in the language FunNondet) that tries to factorize a given number in all possible ways:

rec choose(n) = n orelse choose(n+1);;

val factor(n) =
  let val a = choose(1) in let val b = choose(1) in
  if a * b = n then list(a, b) else fail();;

Sadly, however, if we type the expression choose(24), the answer [1, 24] appears, and then the evaluation goes into an infinite loop without printing anything more. This happens because the program first chooses a value of a, then runs through all possible values of b, trying each to find out if a * b = 24. This works for b = 24, but not for any values of b that are tried after that.

Of course, this program asks for an infinite search, so we can't expect the program to terminate – it must go into an infinite loop eventually. But it would be nice if it could find all the solutions before looping. We can try to do this by modifying the monad on which FunNondet is based. At present, the operator is defined by (something equivalent to)

xm f = concat (map f xm)

The expression map f xm here forms a list of lists; each list corresponds to a result x from xm, and the members of this list correspond to solutions from f x. The concat flattens this list of lists into a single list. If we imagine the list of lists laid out in a rectangular pattern, then concat takes the whole of the first row, followed by the whole of the second row, and so on. That behaviour becomes clear from a simple example:

>>> list(choose(1), choose(1));;
--> [1, 1]
--> [1, 2]
--> [1, 3]
--> [1, 4]
...

Diagonalization

But perhaps you remember the proof that the set of all rational numbers is countable: it involves enumerating a rectangular array of pairs by cutting it into diagonals. We can apply that idea here, by redefining the operator like this:

xm f = concat (diag (map f xm)).

[If I weren't so feeble-minded, I would write ( f) = concat . diag . map f.]

Here, diag is the function defined by

diag :: [[α]] [[α]]
diag [] = []
diag (xs:xss) = longZipWith (++) [ [x] | x xs ] ([] : diag xss),

with longZipWith defined by

longZipWith :: (α α α) [α] [α] [α]
longZipWith f [] ys = ys
longZipWith f xs [] = xs
longZipWith f (x:xs) (y:ys) = f x y : longZipWith f xs ys.

The details don't matter, but these definitions set things up so that if

xss = [[x11, x12, x13, x14, ...], [x21, x22, x23, ...], [x31, x32, ...], ...],

then

diag xs = [[x11], [x12, x21], [x13, x22, x31], [x14, x23, ...], ...].

We can also redefine the orelse operation on the monad so that it gives both arguments a fair chance:

orelse [] ys = ys
orelse (x:xs) ys = x : orelse ys xs

Again, the details don't matter, but the effect is that

orelse [x1, x2, x3, ...] [y1, y2, ...] = [x1, y1, x2, y2, x3, ...].

These changes make the language behave in a way that looks promising. For example:

>>> list(choose(1), choose(1));;
--> [1, 1]
--> [1, 2]
--> [2, 1]
--> [1, 3]
--> [2, 2]
--> [3, 1]
--> [1, 4]
...

Back to factoring

So let's try our original example again, with the same definition of factor as before:

>>> factor(24);;
--> [1, 24]

Oops! The results are just the same as before, with one solution printed before the program enters an infinite loop. Why should that be? And why does the following program give a better result?

>>> let val p = list(choose(1), choose(1)) in
>   if first(p) * second(p) = 24 then p else fail();;
--> [4, 6]
--> [6, 4]
--> [3, 8]
--> [8, 3]
--> [2, 12]
--> [12, 2]
--> [1, 24]
--> [24, 1]

Here the program finds all the factor-pairs of 24 before looping, and that is the best we can hope for, given that the search space to be explored is infinite. Actually, it's possible to make the contrast between a working and a non-working program more stark, if we add to our language the simultaneous declarations that are mentioned in Exercise 1.13 (it's a worthwhile exercise to work out the details of how to do this in a monadic interpreter). Then we find that the program,

let val a = choose(1) and b = choose(1) in
if a * b = 24 then list(a, b) else fail();;

works nicely, though the apparently equivalent program,

let val a = choose(1) in let val b = choose(1) in
if a * b = 24 then list(a, b) else fail();;

does not work as we want.

The reason behind all this is a failure of the associative law for monads: in fact, the last two programs illustrate this nicely. If we take d1 to be the delaration val a = choose(1) and d2 to be the declaration val b = choose(1) and e to be the if expression, then the first program has a meaning that is something like

(elab d1 env  (λenv1  elab d2 env1))  (λenv2  eval e env2).

Here the second and outer joins the declaration to the final expression, and the first and inner joins the two declarations into one. Meanwhile, the second program has the meaning,

elab d1 env  (λenv1  elab d2 env1  (λenv2  eval e env2)),

where now the main operator separates the declaration of a from its body, which contains both the decaration of b and the final if expression. These two meanings should be equal, but they are not.

The reason why associativity fails for this 'monad' is easily explained. In the version of the program that works, the results of the two calls to choose are shuffled together in a fair way, and then the final if expression filters out the pairs that multiply to give 24. In the version that doesn't work, we first make a list of values of a. For each of them, we list the values of b that fit with it to make 24, and this gives a list of lists:

[(1, 24):⊥, (2, 12):⊥, (3, 8):⊥, (4, 6):⊥, ⊥, (6, 4):⊥, ⊥, ...],

where the occurrences of ⊥ show the infinite loop that results from (e.g.) looking for a number b greater than 12 such that 2 * b = 24. Attempting to traverse the diagonals of this list of lists quickly leads to an infinite loop itself, and only the solution (1, 24) is found before this happens.

There do exist ways of fitting fair search into a monadic setting: see, for more detail, the chapter by Silvija Seres and myself in The Fun of Programming (J. Gibbons and O. de Moor, eds.), Palgrave MacMillan, 2003. However, these monads are not based on any form of shuffling of simple lists of solutions.

Personal tools

Variants
Actions
Navigation
Tools