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 `SearchTree`

s 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 `SearchTree`

s, 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