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).
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
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
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
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
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
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)) ]
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 computation1. 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
instance Narrow Nat
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
withUnique we can access an arbitrary number of unique identifiers (even zero) without bothering about how they are generated.
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 :: 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
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
Now we can execute the call
> eval dfs (sub(suc(suc zero)) (suc zero) :: Computation Nat)
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)
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
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
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
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
qs (representing (n-2)! permutations) does not need to be computed.
We 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
permute, but only
permute needs a unique identifier -
allSafe does not introduce non-deterministic branching.
CFLP library provides a generic function
nondet :: (Monad m, Data a) => a -> Data s a
that generates non-deterministic data from primitive Haskell datatypes.
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
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 :: CFLP s
=> Data s Nat -> Data s [Nat]
-> Context (Ctx s) -> ID -> Data s [Nat]
insert x xs cs = withUnique $ \u ->
(x ^: xs) ?
[pCons (\cs y ys -> y ^: insert x ys cs u)] cs)
(?) 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 store2.
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.
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