I came up with a solution that uses the Haskell type system. I googled a bit for an existing solution to the problem at the value level, changed it a bit, and then lifted it to the type level. It took a lot of reinventing. I also had to enable a bunch of GHC extensions.
First, since integers are not allowed at the type level, I needed to reinvent the natural numbers once more, this time as types:
data Zero -- type that represents zero
data S n -- type constructor that constructs the successor of another natural number
-- Some numbers shortcuts
type One = S Zero
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type Six = S Five
type Seven = S Six
type Eight = S Seven
The algorithm I adapted makes additions and subtractions on naturals, so I had to reinvent these as well. Functions at the type level are defined with resort to type classes. This requires the extensions for multiple parameter type classes and functional dependencies. Type classes cannot "return values", so we use an extra parameter for that, in a manner similar to PROLOG.
class Add a b r | a b -> r -- last param is the result
instance Add Zero b b -- 0 + b = b
instance (Add a b r) => Add (S a) b (S r) -- S(a) + b = S(a + b)
class Sub a b r | a b -> r
instance Sub a Zero a -- a - 0 = a
instance (Sub a b r) => Sub (S a) (S b) r -- S(a) - S(b) = a - b
Recursion is implemented with class assertions, so the syntax looks a bit backward.
Next up were booleans:
data True -- type that represents truth
data False -- type that represents falsehood
And a function to do inequality comparisons:
class NotEq a b r | a b -> r
instance NotEq Zero Zero False -- 0 /= 0 = False
instance NotEq (S a) Zero True -- S(a) /= 0 = True
instance NotEq Zero (S a) True -- 0 /= S(a) = True
instance (NotEq a b r) => NotEq (S a) (S b) r -- S(a) /= S(b) = a /= b
And lists...
data Nil
data h ::: t
infixr 0 :::
class Append xs ys r | xs ys -> r
instance Append Nil ys ys -- [] ++ _ = []
instance (Append xs ys rec) => Append (x ::: xs) ys (x ::: rec) -- (x:xs) ++ ys = x:(xs ++ ys)
class Concat xs r | xs -> r
instance Concat Nil Nil -- concat [] = []
instance (Concat xs rec, Append x rec r) => Concat (x ::: xs) r -- concat (x:xs) = x ++ concat xs
class And l r | l -> r
instance And Nil True -- and [] = True
instance And (False ::: t) False -- and (False:_) = False
instance (And t r) => And (True ::: t) r -- and (True:t) = and t
if
s are also missing at the type level...
class Cond c t e r | c t e -> r
instance Cond True t e t -- cond True t _ = t
instance Cond False t e e -- cond False _ e = e
And with that, all the supporting machinery I used was in place. Time to tackle the problem itself!
Starting with a function to test if adding a queen to an existing board is ok:
-- Testing if it's safe to add a queen
class Safe x b n r | x b n -> r
instance Safe x Nil n True -- safe x [] n = True
instance (Safe x y (S n) rec,
Add c n cpn, Sub c n cmn,
NotEq x c c1, NotEq x cpn c2, NotEq x cmn c3,
And (c1 ::: c2 ::: c3 ::: rec ::: Nil) r) => Safe x (c ::: y) n r
-- safe x (c:y) n = and [ x /= c , x /= c + n , x /= c - n , safe x y (n+1)]
Notice the use of class assertions to obtain intermediate results. Because the return values are actually an extra parameter, we can't just call the assertions directly from each other. Again, if you've used PROLOG before you may find this style a bit familiar.
After I made a few changes to remove the need for lambdas (which I could have implemented, but I decided to leave for another day), this is what the original solution looked like:
queens 0 = [[]]
-- The original used the list monad. I "unrolled" bind into concat & map.
queens n = concat $ map f $ queens (n-1)
g y x = if safe x y 1 then [x:y] else []
f y = concat $ map (g y) [1..8]
map
is a higher order function. I thought implementing higher order meta-functions would be too much hassle (again the lambdas) so I just went with a simpler solution: since I know what functions will be mapped, I can implement specialized versions of map
for each, so that those are not higher-order functions.
-- Auxiliary meta-functions
class G y x r | y x -> r
instance (Safe x y One s, Cond s ((x ::: y) ::: Nil) Nil r) => G y x r
class MapG y l r | y l -> r
instance MapG y Nil Nil
instance (MapG y xs rec, G y x g) => MapG y (x ::: xs) (g ::: rec)
-- Shortcut for [1..8]
type OneToEight = One ::: Two ::: Three ::: Four ::: Five ::: Six ::: Seven ::: Eight ::: Nil
class F y r | y -> r
instance (MapG y OneToEight m, Concat m r) => F y r -- f y = concat $ map (g y) [1..8]
class MapF l r | l -> r
instance MapF Nil Nil
instance (MapF xs rec, F x f) => MapF (x ::: xs) (f ::: rec)
And the last meta-function can be written now:
class Queens n r | n -> r
instance Queens Zero (Nil ::: Nil)
instance (Queens n rec, MapF rec m, Concat m r) => Queens (S n) r
All that's left is some kind of driver to coax the type-checking machinery to work out the solutions.
-- dummy value of type Eight
eight = undefined :: Eight
-- dummy function that asserts the Queens class
queens :: Queens n r => n -> r
queens = const undefined
This meta-program is supposed to run on the type checker, so one can fire up ghci
and ask for the type of queens eight
:
> :t queens eight
This will exceed the default recursion limit rather fast (it's a measly 20). To increase this limit, we need to invoke ghci
with the -fcontext-stack=N
option, where N
is the desired stack depth (N=1000 and fifteen minutes is not enough). I haven't seen this run to completion yet, as it takes a very long time, but I've managed to run up to queens four
.
There's a full program on ideone with some machinery for pretty printing the result types, but there only queens two
can run without exceeding the limits :(