Non-determinism, backtracking and Monads

[Andrew J Bromage]

G'day all.

On Wed, Jun 11, 2003 at 12:36:30PM +0200, Jerzy Karczmarczuk wrote:

> It is possible, instead of implementing the *data backtracking* through lazy
> lists, to make lazy "backtrackable" continuations, permitting to redirect 
> the flow of control to produce something else. The two ways are - perhaps not
> entirely equivalent, but essentially two orchestrations of the same 
>                          theme.
> I lost my references, perhaps somebody?...

If you're referring to the paper(s) by Ralf Hinze, they are most
certainly equivalent.

WARNING: Long post follows.

Consider the simplified term implementation of a nondeterminism monad,
which basically operates on lists:

	data Nondet1 a
	    = Cons a (Nondet1 a)
	    | Fail

	-- This is the "observer" method
	runNondet1 :: (Monad m) => Nondet1 a -> m a
	runNondet1 m = case m of
			Cons x _ -> return x
			Fail     -> fail "no solutions"

	return a = Cons a Fail

	m >>= k  = case m of
			Cons a n -> mplus (k a) (n >>= k)
			Fail     -> Fail

	mzero     = Fail

	mplus m n = case m of
			Cons a m' -> Cons a (mplus m' n)
			Fail      -> n

You can derive a continuation-passing implementation by transforming
away the data structures.  This is a technique well-known to
practitioners of traditional lambda calculus.

We'll start by abstracting the data structures out.  We need replacements
for both constructor functions (i.e. Cons and Fail) and the pattern
matching used above.

	data Nondet1 a = Fail | Cons a (Nondet1 a)

	cons1 :: a -> Nondet1 a -> Nondet1 a
	cons1 a m = Cons a m

	fail1 :: Nondet1 a
	fail1 = Fail

	unpack1 :: Nondet1 a -> (a -> Nondet1 a -> b) -> b -> b
	unpack1 (Cons a m) c f = c a m
	unpack1 Fail       c f = f

The monad can now be re-implemented in terms of these operations:

	runNondet1 :: (Monad m) => Nondet1 a -> m a
	runNondet1 m = unpack1 m
			(\x _ -> return x)
			(fail "no solutions")

	return a = cons1 a fail1

	m >>= k  = unpack1 m
			(\a n -> k a `mplus` n >>= k)
			fail1

	mzero     = fail1

	mplus m n = unpack1 m
			(\a m' -> cons1 a (mplus m' n))
			n

Note that there are now no data structures in here, only calls to
fail1, cons1 and unpack1.  We can implement these how we like so
long as these properties hold:

	unpack1 fail1 c f = f
	unpack1 (cons1 x xs) c f = c x xs

The lambda calculus solution is to make unpack1 the identity function.
Unfortunately that doesn't entirely work in Haskell because of the
type system, but we can get pretty close by using rank-2 types and
a newtype constructor:

		-- Compare this with the type of unpack1 above
	newtype Nondet2 a
	    = Nondet2 (forall b. (a -> Nondet2 a -> b) -> b -> b)

	fail2 :: Nondet2 a
	fail2 = Nondet2 (\c f -> f)

	cons2 :: a -> Nondet2 a -> Nondet2 a
	cons2 a m = Nondet2 (\c f -> c a m)

	unpack2 :: Nondet2 a -> (a -> Nondet2 a -> b) -> b -> b
	unpack2 (Nondet2 m) = m

We can inline these functions everywhere to get:

	runNondet2 :: (Monad m) => Nondet2 a -> m a
	runNondet2 (Nondet2 m)
	    = m (\x _ -> return x) (fail "no solutions")

	return a = Nondet2 (\c _ -> c a (Nondet2 (\_ f -> f)))

	(Nondet2 m) >>= k
	    = m (\a n -> mplus (k a) (n >>= k)) (Nondet2 (\_ f -> f))

	mzero     = Nondet2 (\_ f -> f)

	mplus (Nondet2 m) n
	    = m (\a m' -> Nondet2 (\c _ -> c a (mplus m' n))) n

...and we have a continuation-passing implementation.

Note that this is not 100% identical to the one from Ralf's paper and
tech report.  Transforming the above code into Ralf's is left as an
exercise.  (It's tricky but mechanical.)

Cheers,
Andrew Bromage