% The n-Queens Problem
% Sebastian Fischer (sebf@informatik.uni-kiel.de)

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\times n$ chessboard such that no
queen can hit another in one move.

Installation instructions can be found on the [`cflp`
website][cflp]. 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).

[cflp]: http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html

> {-# 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. 

Non-Deterministic Data
----------------------

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.

Operations on Non-Deterministic Data
------------------------------------

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.

[^1]: 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.

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

[curry-language]: http://www.curry-language.org/

~~~ { .Haskell }
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:

~~~ { .Haskell }
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

~~~ { .Haskell }
 > 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:

~~~ { .Haskell }
 > 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!

Safely Placing Queens
---------------------

We represent a placement of $n$ queens on an $n\times 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:

~~~ { .Haskell }
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.

~~~ { .Haskell }
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.

~~~ { .Haskell }
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.

~~~ { .Haskell }
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.

Placing Queens with the `CFLP` library
--------------------------------------

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:

~~~ { .Haskell }
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

~~~ { .Haskell }
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].

[^2]: 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`.

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\times 8$ chessboard:

> main :: IO ()
> main = do
>   qs <- eval dfs (placement 8 :: Computation [Nat])
>   mapM_ print . map (map nat2int) $ qs

Notes on Efficiency
-------------------

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.