At FLOPS 2008 Oleg Kiselyov showed me FBackTrack — a simple instantiation of the MonadPlus class in Haskell which is fair (like breadth-first search) and seems to consume considerably less memory than BFS. I immediately started following an obvious plan: implement a traversal on Curry’s SearchTree datatype treating choices like mplus and values like return.

Although the resulting search outperformed breadth-first search in some examples, I didn’t get the benefit that I expected from the Haskell experiments. A closer look revealed that the main trick to save memory was the implementation of the bind operator, that a search that doesn’t use bind is a worst case for the algorithm still taking exponential space, and that SearchTrees don’t have an equivalent to bind, unfortunately!

The bind operator takes a nondeterministic computation and passes one of its results to a function supplied as second argument, i.e., bind demands the computation of its first argument. The question arises, how we can model lazy functional-logic programming in Haskell, so instead of writing a traversal for SearchTrees, I tried to figure out how to translate Curry programs to Haskell such that under the hood, FBackTrack is used as search engine. The implementation uses the datatype Stream that is an instance of MonadPlus:

  data Stream a =
    Nil | One a | Choice a (Stream a) | Incomplete (Stream a)

The implementations of the mplus and bind operations use a tricky interleaving to compute a fair enumeration of all stream elements efficiently.

A naiv approach to translate Curry programs to Haskell where only the result type of functions is made monadic is not lazy enough (Curry code is given as a comment):

  -- const x _ = x
  const :: a → b → Stream b
  const x _ = return x

  -- loop = loop
  loop :: Stream a
  loop = loop

  -- main = const 42 loop
  main = do
    x ← return 42
    y ← loop
    const x y

The given program will fail to terminate with the implementation given in FBackTrack.hs and I couldn’t come up with another implementation that handles laziness in a sensible way.

Instead, I concluded to apply a different transformation scheme that uses bind only when the program demands evaluation, e.g., during pattern matching. With this transformation scheme the Haskell and Curry versions of the functions given above are identical (apart from type signatures). To see the difference consider the transformed version of the function not:

  -- not b = case b of False → True; True → False
  not b =
    match b $ λd →
    case d of
      Cons 0 [] → true
      Cons 1 [] → false

What is the (Haskell-)type of not? The function match used before pattern matching has the following type:

  match :: (Nondet a, Nondet b) ⇒ a → (Data → b) → b

The datatype Data represents head-normal forms of nondeterministic data values:

  data Data = Cons Int [Stream Data]

Data values are constructor rooted and have an arbitrary number of nondeterministic data values as arguments. The type class Nondet provides operations to convert between arbitrary data types and nondeterministic data values:

  class Nondet a
   where
    toData   :: a → Stream Data
    fromData :: Stream Data → a

The implementation of match simply calls these functions and the bind operation of the Stream monad appropriately:

  match :: (Nondet a, Nondet b) ⇒ a → (Data → b) → b
  match x f = fromData (toData x >>= toData . f)

The type of not is

  not :: FLP_Bool → FLP_Bool

where FLP_Bool is a newtype for Stream Data:

  newtype FLP_Bool = Bool { fromBool :: Stream Data }

The definition for the instance Nondet FLP_Bool simply uses the defined constructor and destructor:

  instance Nondet FLP_Bool
   where
    toData   = fromBool
    fromData = Bool

The functions false and true define the representation of False and True as data values:

  false, true :: FLP_Bool
  false = Bool (One (Cons 0 []))
  true  = Bool (One (Cons 1 []))

At run time, values of type FLP_Bool will be indistinguishable from values of type Stream Data — the newtype constructor will be eliminated. Why do we introduce the type FLP_Bool anyway? The type class Nondet has another method unknown which represents a logic variable and is usually implemented differently for different types:

  class Nondet a
   where
    …
    unknown :: a

For example, the instance for FLP_Bool implements unknown as follows:

  instance Nondet FLP_Bool
   where
    …
    unknown = choice [false,true]

The function choice is used to build the nondeterministic choice of arbitrary values of the same type:

  choice :: Nondet a ⇒ [a] → a
  choice xs = fromData (foldr1 mplus (mzero:map toData xs))

The implementation folds mplus over the list of choices. The additional mzero in front of the list ensures fairness even if left recursion is used.

If we evaluate the call not unknown we get the result

  Bool {fromBool =
         Incomplete (Choice (Cons 1 [])
                    (Incomplete (One (Cons 0 []))))}

which is a nondeterministic choice of true and false. Laziness is also no problem: const true loop yields Bool {fromBool = One (Cons 1 [])}. Unfortunately, we have a different problem now.

In order to examine nested terms, consider the datatype FLP_Pair of functional logic pairs:

  newtype FLP_Pair a b = Pair { fromPair :: Stream Data }

The constructor for pairs is defined as follows:

  pair :: (Nondet a, Nondet b) ⇒ a → b → FLP_Pair a b
  pair x y = Pair (One (Cons 0 [toData x,toData y]))

The problem of the presented transformation scheme is that it does not respect shared nondeterministic choices. For example, a call to main in the following Curry program should give the results (True,True) or (False,False) but neither (True,False) nor (False,True):

  main = dup (unknown::Bool)

  dup x = (x,x)

The restricted set of results corresponds to what would be evaluated with an eager strategy and we need to compute the same results lazily.

We can easily define the Haskel version of dup as

  dup :: Nondet a ⇒ a → FLP_Pair a a
  dup x = pair x x

but the call dup (unknown::FLP_Bool) yields

  Pair {fromPair =
         One (Cons 0 [Incomplete (Choice (Cons 0 [])
                                    (One (Cons 1 []))),
                      Incomplete (Choice (Cons 0 [])
                                    (One (Cons 1 [])))])}

which represents all four pairs of booleans. The information that the same choice should be taken in both components is lost.

Until now, I didn’t find a way to improve on this. Even the side-effectish way of associating unique references to choices in order to detect choices that where duplicated by sharing cannot easily be adopted because of the tricky interleavings in the implementation of the monadic operations that constantly restructure the choices.

The code in this post was taken from the following files:

  • Stream.hs — the fair Stream monad
  • FLP.hs — primitives for functional-logic programming
  • examples.hs — demonstrate laziness and (lack of) sharing support