Abusing the continuation monad

(Recall that monads are not a good topic for your first blog post.)

I intend to bootstrap a blog by writing about 2 of my old papers, Monad Transformers for Backtracking Search and The Selection Monad as a CPS Transformation. (Wall Street will be spared for the time being.)

I’m going to write about this little bit of Haskell code:

import Control.Monad.Cont
sat n = runCont $ sequence $ replicate n $ cont $ \k -> k $ k True

It’s a SAT solver: you give it a boolean function, and the number of variables to search, and it decides whether that function will ever return true for any values of those variables.

How does this work? Haven’t the foggiest. If anyone can explain what it does at runtime, there’s probably a research paper in it for you. If you can also predict how long it takes, that’s a big deal.

So where does this come from? It’s a demonstration I wrote of the work of Martin Escardó and Paulo Oliva on selection functions. For Haskell programmers, good places to start are Seemingly Impossible Functional Programs and What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift Have in Common. I removed all traces of selection functions, using only the continuation monad that we all know and love, to make it as short and magical-looking as I could.

The first bit of magic is the function \k -> k $ k True. Let’s call it e, as in

e k = k $ k True

This function e is an existential quantifier. That is to say it takes a predicate (a function k into booleans), and decides whether there exists an input making the predicate true. For example, on natural numbers, applying an existential quantifier to the predicate \n -> n^2 == 4 should return True, but applying it to \n -> n^2 == 2 should return False.

The function e can’t exactly do that. In fact, the existential quantifier for natural numbers isn’t computable. What it does is to compute the existential quantifier for booleans.

I don’t have a slick way to demonstrate this counter-intuitive fact. There’s an awkward case-based argument, starting from the fact that k True is either true, or it’s false. But this is only ε more enlightening than just brute-forcing it: there are precisely 4 (total) functions Bool -> Bool, so it’s easy to just evaluate e on each of them and check that it does the right thing.

So, we have the function \k -> k $ k True :: (Bool -> Bool) -> Bool. We hit that with cont which, despite not beginning with a capital letter, is the constructor of the Cont monad. So it doesn’t actually do anything, except changing the type to Cont Bool Bool. (The runCont on the outside is the corresponding deconstructor, and also does nothing except change the type.)

Next we use replicate n, which creates a list of n identical copies. So at this point, we have a list containing n instances of the existential quantifier, each one wrapped inside Cont, the whole thing having type [Cont Bool Bool].

The actual deep magic in the code snippet is the use of sequence, possibly the most magical function in Prelude. What sequence does, in general, is fold the monoidal product of a monoidal monad. For example, a useful little idiom in functional programming is to use sequence to find the cartesian product of lists (because cartesian product is the monoidal product of the list monad).

It turns out that if you take the monoidal product of existential quantifiers in the Cont monad, you get one big existential quantifier for the product type. Which means, we get an existential quantifier for boolean lists of length n. Which is to say, if we give it a predicate k :: [Bool] -> Bool, it will decide if there is an input of length n making the predicate true. Which is another way of saying, it is a SAT solver for boolean functions with n inputs.

No, I’m not going to prove that here.

There are some pretty big open questions about this code I alluded to earlier, of which the biggest is that there doesn’t seem to be any sort of complexity theory even capable of asking the question of what its runtime is. (The real difficulty is that sequence used this way is a third-order function, that is, its input is a function which itself takes a function as input.)

Instead, I’m going to ask a more manageable and concrete question: Can this code be written in continuation-passing style? By that I mean, can it be written in a way that doesn’t use cont, but instead uses call/cc? Equivalently, can this code be translated to Scheme?