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