This is a tutorial introduction demonstrating the use of the `cflp`

package by solving the *n*-queens problem with a lazy functional-logic program: place *n* queens on an *n* × *n* chessboard such that no queen can hit another in one move.

Installation instructions can be found on the `cflp`

website. Once you have installed the package you can execute this tutorial which is Literate Haskell. If you are reading the HTML version, you find the plain `.lhs`

file on the mentioned website (and vice versa).

`{-# LANGUAGE`

NoMonomorphismRestriction,

MultiParamTypeClasses,

FlexibleInstances,

NoMonoPatBinds,

TypeFamilies

#-}

import CFLP

import CFLP.Strategies

import CFLP.Types.Bool

import CFLP.Types.List hiding ( map )

import Prelude hiding ( not )

After importing the `CFLP`

library, we can access combinators to define non-deterministic datatypes and operations.

In order to demonstrate how to define lazy non-deterministic datatypes, we use natural numbers in Peano notation to denote rows and columns of a chessboard:

`data Nat = Zero | Suc Nat`

deriving Show

For convenience, we define functions that convert between Peano numbers and integers.

`nat2int :: Nat -> Int`

nat2int Zero = 0

nat2int (Suc n) = nat2int n + 1

int2nat :: Int -> Nat

int2nat 0 = Zero

int2nat (n+1) = Suc (int2nat n)

A functional-logic program will use numbers of type `Data s Nat`

where `Nondet`

is an abstract type constructor for non-deterministic data, cs is a constraint store and `m`

is a constraint solver monad. We don't care about what exactly a constraint solver or a constraint solver monad is but simply notice, that we might use different ones in order to use different search strategies.

We can define constructor functions for values of type `Data s Nat`

using combinators from the `CFLP`

library. To do so, we need to define type-class instances that describe the structure of our datatype. The definitions are completely mechanic and could probably be automated.

First, we define an instance of the class `ApplyCons`

:

`instance ApplyCons Nat where type Result Nat = Nat; applyCons = const`

All user-defined instances of `ApplyCons`

look like this.

The structure of our datatype is captured by the class `Generic`

:

`instance Generic Nat`

where constr = cons "Zero" Zero dZero ! cons "Suc" Suc dSuc

We only need to list the constructors and destructors of our datatype. Destructors are also defined mechanically:

`dZero, dSuc :: Decons Nat`

dZero zero Zero = Just (zero [])

dZero _ _ = Nothing

dSuc suc (Suc n) = Just (suc [generic n])

dSuc _ _ = Nothing

The `Generic`

instance allows to convert between non-deterministic and primitive Haskell values and to define constructors and destructors for non-deterministic data.

`zero :: Monad s => Nondet c s Nat`

suc :: Monad s => Nondet c s Nat -> Nondet c s Nat

zero :! suc :! () = constructors

Here, it is important to list the constructors in the same order as in the instance declaration for the class `Generic`

. We get constructor functions of arbitrary aritiy where all types are lifted to the `Nondet`

type.

In order to define operations on non-deterministic numbers, we also need helpers for pattern matching that are defined similarly.

`pZero :: (Context c -> Nondet c s a) -> Match Nat c s a`

pSuc :: (Context c -> Nondet c s Nat -> Nondet c s a) -> Match Nat c s a

pZero :! pSuc :! () = patterns

A matcher takes a function that takes an evaluation context and non-deterministic values that correspond to the arguments of the matched constructor and yields an arbitrary non-deterministic value.

No we can define operations on non-deterministic numbers. As an example consider addition:

`add :: CFLP s`

=> Data s Nat -> Data s Nat -> Context (Ctx s) -> Data s Nat

add n m = caseOf n

[ pZero (\_ -> m)

, pSuc (\cs n' -> suc (add n' m cs)) ]

The function `add`

takes two non-deterministic numbers and - as additional argument - a constraint store that is passed to the combinator `caseOf`

for pattern matching. The case alternatives are given as a list of matchers that can access an updated constraint store and pass it down in the computation^{1}. The context `CFLP s`

states that `cs`

is a constraint store and `m`

is a constraint solver monad suitable for functional-logic programming.

Once we have defined addition, we can use logic programming to define subtraction! In the functional-logic programming language Curry, we could define the function `sub`

as follows:

`sub :: Nat -> Nat -> Nat`

sub n m | n =:= add m x = x

where x free

This definition uses the *constraint-equality operation* `(=:=) :: a -> a -> Success`

to state that the sum of the second argument of `sub`

and its result should equal its first argument. The result of `sub`

is introduced as free (logic) variable.

We can define how to generate logic variables of type `Data s Nat`

by instantiating the type class `Narrow`

.

`instance Narrow Nat`

where

narrow cs u = withUnique (\u' -> oneOf [zero, suc (unknown u')] cs u) u

A free variable is a non-deterministic generator of each possible value. The combinator `unknown`

is defined in terms of `narrow`

and can be used to obtain a free logic variable. We can narrow non-deterministic natural numbers in every constraint store that supports non-deterministic choices which is expressed using a corresponding class constraint in the instance definition.

Operations that cause non-deterministic branching - like `narrow`

does - need an additional argument of type `ID`

that is passed to the `oneOf`

combinator for non-deterministic choice. In order to simplify the distribution of unique identifiers, the `CFLP`

library provides an overloaded operation `withUnique`

that has all of the following types at the same time:

`withUnique :: Data s a -> ID -> Data s a`

withUnique :: (ID -> Data s a) -> ID -> Data s a

withUnique :: (ID -> ID -> Data s a) -> ID -> Data s a

withUnique :: (ID -> ID -> ID -> Data s a) -> ID -> Data s a

...

When using `withUnique`

we can access an arbitrary number of unique identifiers (even zero) without bothering about how they are generated.

The `CFLP`

library provides an operation `(===)`

(similar to `(=:=)`

in Curry but with a boolean result) that can be used to define the Haskell version of the function `sub`

.

`sub :: CFLP s`

=> Data s Nat -> Data s Nat

-> Context (Ctx s) -> ID -> Data s Nat

sub n m cs = withUnique $ \u ->

let x = unknown u in

caseOf ((n === add m x cs) cs)

[pTrue (\_ -> x)] cs

As `sub`

calls the combinator `unknown`

to generate a free variable, we need to pass a unique identifier in addition to the constraint store. The guard of the Curry program is expressed by a partial pattern matching on `True`

.

Now we can execute the call

` > eval dfs (sub(suc(suc zero)) (suc zero) :: Computation Nat)`

[Suc Zero]

to enumerate the results of subtracting one from two in depth first order. Note, that results are returned as primitive Haskell terms of type `Nat`

. We can also enumerate them interactively:

` > evalPrint dfs (sub(suc(suc zero)) (suc zero) :: Computation Nat)`

Suc Zero

more? [Y(es)|n(o)|a(ll)]: y

No more solutions.

This is useful if the number of results is infinite or we are not interested in all of them for some other reason.

The first argument `dfs ()`

is a strategy that should be used for the computation. Here, we use the list monad which implements depth first search. If you have your own implementation `m`

of `MonadPlus`

and an enumeration function of type `m a -> [a]`

then you can use this as a strategy as well!

We represent a placement of *n* queens on an *n* × *n* chessboard with a permutation of `[1..n]`

. A number *c* at position *r* of the permutation means that in row *r* of the chessboard, a queen is placed at column *c*. This representation ensures that every row and every colum contains exactly one queen, so we only need to check whether they can hit each other diagonally.

In Curry, we could compute safe placements of queens as follows:

`placement :: Int -> [Int]`

placement n = allSafe (permute [1..n])

The non-deterministic operation `permute`

computes permutations of its input by successively inserting its elements at arbitrary positions.

`permute :: [a] -> [a]`

permute [] = []

permute (x:xs) = insert x (permute xs)

insert :: a -> [a] -> [a]

insert x xs = x : xs

insert x (y:ys) = y : insert x ys

The operation `insert`

either inserts the given element as new head or somewhere in the tail of the given list, if it is non-empty.

Now, we only need to define when a placement of queens is safe.

`allSafe :: [Int] -> [Int]`

allSafe [] = []

allSafe (q:qs) = safe q qs 1 : allSafe qs

The operation `allSafe`

is a so called *constrained identity* function, i.e., it either returns its argument or fails. The operation `safe`

is another constrained identity (on the first argument) that checks whether one queen can hit another by comparing the remaining positions to the diagonally reachable positions of the given queen.

`safe :: Int -> [Int] -> Int -> Int`

safe p [] _ = p

safe p (q:qs) offset | noAttac p q offset = safe p qs (offset+1)

noAttac :: Int -> Int -> Int -> Bool

noAttac p q offset | p + offset /= q = p /= q + offset

A key feature of this program is laziness: the constrained identities may fail without consuming the complete placement of queens, i.e., without computing the whole permutation. For example, if the placement is of the form `1:2:qs`

then `qs`

(representing (*n*-2)! permutations) does not need to be computed.

`CFLP`

libraryWe can implement an equivalent program (featuring laziness!) in pure Haskell using the `CFLP`

library. The library provides constructors and matchers for non-deterministic lists with the following types:

`nil :: Monad s => Data s [a]`

(^:) :: Monad s => Data s a -> Data s [a] -> Data s [a]

pNil :: (c -> Data s b) -> Match [a] c s b

pCons :: (c -> Data s a -> Data s [a] -> Data s b)

-> Match [a] c s b

The function that computes a safe placement of `n`

queens is defined as follows:

`placement :: CFLP s => Int -> Context (Ctx s) -> ID -> Data s [Nat]`

placement n cs u = allSafe (permute queens cs u) cs

where queens = nondet (map int2nat [1..n])

It takes a constraint store and a unique identifier. The constraint store is passed to both `allSafe`

and `permute`

, but only `permute`

needs a unique identifier - `allSafe`

does not introduce non-deterministic branching.

The `CFLP`

library provides a generic function

`nondet :: (Monad m, Data a) => a -> Data s a`

that generates non-deterministic data from primitive Haskell datatypes.

The operation `permute`

resembles the Curry definition given above. It uses `withUnique`

to access a sufficient number of fresh identifiers, the combinator `caseOf`

to match the given non-deterministic list, and passes updated constraint stores to the function `insert`

and the recursive call.

`permute :: CFLP s`

=> Data s [Nat] -> Context (Ctx s) -> ID -> Data s [Nat]

permute l cs = withUnique $ \u1 u2 -> caseOf l

[ pNil (\_ -> nil)

, pCons (\cs x xs -> insert x (permute xs cs u1) cs u2) ] cs

The `insert`

operation uses `oneOf`

to generate a non-deterministic choice between inserting the element as head or in the tail of the given list. Insertion in the tail is performed with a (partial) pattern matching on non-empty lists and a recursive call of `insert`

to `ys`

.

`insert :: CFLP s`

=> Data s Nat -> Data s [Nat]

-> Context (Ctx s) -> ID -> Data s [Nat]

insert x xs cs = withUnique $ \u ->

(x ^: xs) ?

(caseOf xs

[pCons (\cs y ys -> y ^: insert x ys cs u)] cs)

The operator `(?)`

is similar to `oneOf`

in that it declares a non-deterministic choice, but it takes exactly two arguments. More importantly, unlike `oneOf`

, the operator `(?)`

does not take a constraint store^{2}.

Now, we need to define the constrained identity `allSafe`

. All functions resemble the Curry definitions given above.

`allSafe :: CFLP s => Data s [Nat] -> Context (Ctx s) -> Data s [Nat]`

allSafe l = caseOf l

[ pNil (\_ -> nil)

, pCons (\cs q qs -> safe q qs (suc zero) cs ^: allSafe qs cs) ]

safe :: CFLP s

=> Data s Nat -> Data s [Nat] -> Data s Nat

-> Context (Ctx s) -> Data s Nat

safe p l offset = caseOf l

[ pNil (\_ -> p)

, pCons (\cs q qs -> caseOf (noAttac p q offset cs)

[ pTrue (safe p qs (suc offset)) ] cs) ]

noAttac :: CFLP s

=> Data s Nat -> Data s Nat -> Data s Nat

-> Context (Ctx s) -> Data s Bool

noAttac p q offset cs = caseOf ((add p offset cs === q) cs)

[ pFalse (\cs -> not ((p === add q offset cs) cs) cs) ] cs

Finally, we can define an operation `main`

that prints all possible placements of 8 queens on an 8 × 8 chessboard:

`main :: IO ()`

main = do

qs <- eval dfs (placement 8 :: Computation [Nat])

mapM_ print . map (map nat2int) $ qs

Although I have not investigated any effort yet in the efficiency of the `CFLP`

library, I have compared the runtime of this program with the run times of an equivalent Curry program in the Curry systems MCC, PAKCS, and KiCS. The results are depicted in the following table.

System | run time |
---|---|

MCC | 1.1s |

PAKCS | 5.4s |

KiCS | 8.4s |

CFLP | 5.8s |

I have also compared this implementation with a simple implementation using `MonadPlus`

without preserving laziness. Such an implementation is much faster, probably because laziness is not important when computing permutations of such short lists.

You may wonder, why we have to pass constraint stores explicitly and why they are not hidden in a state component of the monad. A significant feature of the

`CFLP`

library is, that monadic values are shared and not recomputed if the same monadic action occurs more than once in a computation because of sharing. Monadic values of a state-threading monad are functions and would need to be recomputed for each occurrence. ↩Choices that are build with

`(?)`

are recomputed according to the current constraint store whenever they are matched (like free variables). So you should use`(?)`

when you declare a non-deterministic choice (especially when you intend to share it). The combinator`oneOf`

is usually only used in the definitions of`narrow`

where reexecution is already handled before by`unknown`

. ↩