Posted on May 11, 2017

I heard of this problem recently, based on Aphyr’s eccentrically written typing the technical interview blog post. It’s an interesting read, but sadly, I am not a witch, so I found the functional dependency style used quite difficult to understand. I therefore thought I would spend a few minutes bashing out a simple solution at the term level, then attempt to port it to the type level using more modern Haskell techniques with the `singletons`

library and type families.

The question, which is apparently common in interviews, is to discover ways of placing 8 queens on a chessboard without any of them being able to attack one another.

Here’s my take at the term level version: my solution is a monadic fold using list’s monad instance, where the accumulator is keeping track of the Queens’ positions in each row we have placed already.

```
import Control.Monad
solution :: [[Int]]
solution = foldM place [] [1..8]
place :: [Int] -> a -> [[Int]]
place current _ =
(: current) <$> filter (safe current) [1..8]
safe :: [Int] -> Int -> Bool
safe xs x =
and
[ all (/= x) xs
, all (/= x) (zipWith (+) xs [1..])
, all (/= x) (zipWith (-) xs [1..])
]
```

It’s a simple solution. For the type level, I’ll be doing it quite differently to Aphyr.

```
{-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies, KindSignatures,
TemplateHaskell, GADTs, UndecidableInstances, RankNTypes,
ScopedTypeVariables, FlexibleContexts, TypeInType #-}
module Main where
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List
import Data.Singletons.TypeLits
```

With that out of the way I can define a type level `safe`

function which returns all the safe locations which a queen can go in a row, given the positions of queens in the previous rows.

```
type family Safe (b :: [Nat]) (a :: Nat) :: Bool where
Safe xs x =
And
'[ All ((:/=$$) x) xs
, All ((:/=$$) x)
( ZipWith (:+$) xs (EnumFromTo 1 8) )
, All ((:/=$$) ( 10 :+ x ))
( ZipWith (:-$) (Map ((:+$$) 10) xs) (EnumFromTo 1 8) ) ]
```

I was tripped up a few times writing this function. The first thing was just trying to find the right version of the equality functions to call. The `$$`

ending specifies the right number of partial applications to apply, but it’s a real pain to discover due to the template haskell generated haddocks of the `singletons`

library being terrible. The next thing was the natural number subtraction. My type families were getting stuck without the `+10`

when a negative number would have been produced, but it was quite hard to see what the problem really was.

Below I define my partial application for `Safe`

. Unfortunately, just like Aphyr I still need to do this as Haskell type application can’t be partially applied. But using data kinds and type in type makes this a lot safer here, with a proper type signature keeping everything in place.

```
data Safe1 :: [Nat] -> (Nat ~> Bool)
type instance Apply (Safe1 xs) x = Safe xs x
```

The `(~>)`

and the `Apply`

type family come from the `singletons`

library, and represent type level functions, and their application respectively. Next, we filter a candidate set of positions using the safe function, with the help of some additional type families from `Data.Singletons.Prelude.List`

.

```
type family Place (a :: [Nat]) (b :: k) :: [[Nat]] where
Place xs ignore =
Map (FlipCons1 xs) (Filter (Safe1 xs) (EnumFromTo 1 8))
data FlipCons1 :: [Nat] -> (Nat ~> [Nat])
type instance Apply (FlipCons1 xs) x = x ': xs
data Place1 :: [Nat] -> (ignore ~> [[Nat]])
type instance Apply (Place1 xs) b = Place xs b
data Place2 :: ([Nat] ~> ignore ~> [[Nat]])
type instance Apply (Place2) xs = Place1 xs
```

To write the FoldM we need to perform type application using the `Apply`

instances. This is actually pretty easy, and there is even a `(@@)`

operator to help us here. Again, we also need to define a function for the partially applied recursive term.

```
type family FoldM ( f :: b ~> a ~> [b] ) ( acc :: b ) ( over :: [a] ) :: [b] where
FoldM f acc '[] = '[ acc ]
FoldM f acc ( x ': xs) =
ConcatMap (FoldM1 f xs) (f @@ acc @@ x )
data FoldM1 :: ( b ~> a ~> [b] ) -> [a] -> ( b ~> [b] )
type instance Apply (FoldM1 f xs ) acc = FoldM f acc xs
```

Next up is the solution. It’s written almost identically to the term level code above, with a fold over placements.

```
type family Solutions :: [[Nat]] where
Solutions = FoldM Place2 '[] (EnumFromTo 1 8)
```

It appears to work too

```
*Main> :t Proxy :: Proxy Solutions
Proxy :: Proxy Solutions
:: Proxy
('[4, 2, 7, 3, 6, 8, 5, 1]
:$$$ '['[5, 2, 4, 7, 3, 8, 6, 1], '[3, 5, 2, 8, 6, 4, 7, 1],
...
```

Modern Haskell’s type level code is actually pretty succinct, and even has a good degree of type safety. Using less code, we are pretty easily able to get all the solutions (instead of one in the cited blog post), and my type errors when writing it actually existed, which was a plus.

Interestingly, a lot of what was written above can be generated for us by the `singletons`

library (indeed, this is how the `singletons`

library is written).

For example, the `FoldM`

type family above can be completely replaced with

```
import Data.Singletons.TH
$(singletonsOnly [d|
foldM :: (b -> a -> [b]) -> b -> [a] -> [b]
foldM _ acc [] = [acc]
foldM f acc (x : xs) =
concatMap (\acc' -> foldM f acc' xs) (f acc x)
|])
```

and the library will even generate for us the partially applied terms.

One can actually get very close to the result with just the code from my term level calculation in a `singletonsOnly`

splice. It is however a bit finicky, and often complains about functions not existing when there is a type family for them, so it’s a bit all or nothing. Plus, one loses a lot of readability in their error messages and the haddocks will be phenomenally bad.