Typelevel N Queen in PureScript

Main.purs

module Main where

import Prelude

import Effect (Effect)
import Effect.Console (log)
import Data.Ord (abs)
import Data.List (List(Nil), range, (:), length)
import Data.Traversable (traverse)

-- define type level natural number
foreign import kind Nat
foreign import data Zero :: Nat
foreign import data Succ :: Nat -> Nat

-- type level addition
class Add (a :: Nat) (b :: Nat) (r :: Nat) | a b -> r
instance addZero :: Add Zero b b
instance addSucc :: Add (Succ a1) b (Succ b)

-- type level boolean
foreign import kind Bool
foreign import data True :: Bool
foreign import data False :: Bool

-- type level nat eq function
class Equal (a :: Nat) (b :: Nat) (r :: Bool) | a b -> r
instance equalZero       :: Equal a a True
else instance equalOther :: Equal a b False

class Not (a :: Bool) (r :: Bool) | a -> r
instance notTrue :: Not True False
else instance notFalse :: Not False True

class NotEqual (a :: Nat) (b :: Nat) (r :: Bool) | a b -> r
instance notEqual' :: (Equal a b r1, Not r1 r2) => NotEqual a b r2

class And (a :: Bool) (b :: Bool) (r :: Bool) | a b -> r
instance andTrueTrue :: And True True True
else instance andOther :: And a b False

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type N4 = Succ Three
type N5 = Succ N4
type N6 = Succ N5
type N7 = Succ N6
type N8 = Succ N7

data NProxy (n :: Nat) = NProxy
data BProxy (b :: Bool) = BProxy

class NatToValue (t :: Nat) where toIntVal :: NProxy t -> Int
instance zeroToValue :: NatToValue Zero where toIntVal _ = 0
else instance succToValue
  :: NatToValue n
  => NatToValue (Succ n)
  where toIntVal _ = 1 + toIntVal (NProxy :: NProxy n)

class BoolToValue (t :: Bool) where toBoolVal :: BProxy t -> Boolean
instance trueToValue :: BoolToValue True where toBoolVal _ = true
else instance falseToValue :: BoolToValue False where toBoolVal _ = false

doesOnePlusOneEqualTwo
  :: forall n r. Add One One n
  => Equal n Two r
  => BProxy r
doesOnePlusOneEqualTwo = BProxy

onePlusTwo :: forall n. Add One Two n => NProxy n
onePlusTwo = NProxy

doesOnePlusTwoEqualTwo
  :: forall n r. Add One Two n
  => Equal n Two r
  => BProxy r
doesOnePlusTwoEqualTwo = BProxy

foreign import kind NatList
foreign import data NNil :: NatList
foreign import data NCon :: Nat -> NatList -> NatList

infixr 5 type NCon as :::

type LL = Three ::: Zero ::: Two ::: NNil

ll :: NLProxy LL
ll = NLProxy

class CheckVertical (l :: NatList) (n :: Nat) (r :: Bool) | l n -> r
instance checkVerticalEmpty :: CheckVertical NNil n True
else instance checkVerticalOther ::
  ( NotEqual a n r1
  , CheckVertical as n r2
  , And r1 r2 r3
  ) => CheckVertical (a ::: as) n r3

twoNotInLL :: forall r. CheckVertical LL Two r => BProxy r
twoNotInLL = BProxy

threeNotInLL :: forall r. CheckVertical LL Three r => BProxy r
threeNotInLL = BProxy

checkVertical :: List Int -> Int -> Boolean
checkVertical Nil n = true
checkVertical (a : as) n = n /= a && checkVertical as n

class AbsMinus (a :: Nat) (b :: Nat) (r :: Nat) | a b -> r
instance absMinusZeroA      :: AbsMinus Zero a a
else instance absMinusAZero :: AbsMinus a Zero a
else instance absMinusSucc ::
  ( AbsMinus a1 b1 r
  ) => AbsMinus (Succ a1) (Succ b1) r

absOneMinusThree :: forall d. AbsMinus One Three d => NProxy d
absOneMinusThree = NProxy

class CheckDiagonalGo (l :: NatList) (row :: Nat) (cc :: Nat) (r :: Bool) | l row cc -> r
instance checkDiagonalGoNil      :: CheckDiagonalGo NNil r n True
else instance checkDiagonalGoCon ::
  ( Add One row r1
  , AbsMinus c cc r2
  , NotEqual r1 r2 r3
  , CheckDiagonalGo cs r1 cc r4
  , And r3 r4 r5
  ) => CheckDiagonalGo (c ::: cs) row cc r5

class CheckDiagonal (l :: NatList) (cc :: Nat) (r :: Bool) | l cc -> r
instance checkDiagonal' :: CheckDiagonalGo l Zero cc r => CheckDiagonal l cc r

checkDiagonal :: List Int -> Int -> Boolean
checkDiagonal arr cc = go arr 0
  where
    go Nil r = true
    go (c : cs) r = r + 1 /= abs (c - cc) && go cs (r + 1)

class Check (l :: NatList) (cc :: Nat) (r :: Bool) | l cc -> r
instance check' ::
  ( CheckDiagonal l cc r1
  , CheckVertical l cc r2
  , And r1 r2 r3
  ) => Check l cc r3

-- check whether n can be prepend to the arr
check :: List Int -> Int -> Boolean
check arr n = checkDiagonal arr n && checkVertical arr n

foreign import kind ListList
foreign import data LNil :: ListList
foreign import data LCon :: NatList -> ListList -> ListList

infixr 5 type LCon as ::>

class IfElseListList (c :: Bool) (a :: ListList) (b :: ListList) (r :: ListList) | c a b -> r
instance ifElseTrue  :: IfElseListList True a b a
else instance ifElseFalse :: IfElseListList False a b b

class PlaceOneGo (n :: Nat) (i :: Nat) (arr :: NatList) (acc :: ListList) (r :: ListList) | n i arr acc -> r
instance placeOneGoTerminal :: PlaceOneGo n n arr acc acc
else instance placeOneGoCheck ::
  ( Add One i i1
  , PlaceOneGo n i1 arr ((i ::: arr) ::> acc) r1
  , PlaceOneGo n i1 arr acc r2
  , Check arr i c
  , IfElseListList c r1 r2 r3
  ) => PlaceOneGo n i arr acc r3
else instance placeOneGoOther ::
  ( Add One i i1
  , PlaceOneGo n i1 arr acc r
  ) => PlaceOneGo n i arr acc r

class PlaceOne (n :: Nat) (arr :: NatList) (r :: ListList) | n arr -> r
instance placeOne' :: PlaceOneGo n Zero arr LNil r => PlaceOne n arr r

data NLProxy (l :: NatList) = NLProxy

class NatListToVal (ll :: NatList) where toNatListVal :: NLProxy ll -> List Int
instance nlToValNil :: NatListToVal NNil where toNatListVal _ = Nil
else instance nlToValCon ::
  ( NatToValue n
  , NatListToVal ns
  ) => NatListToVal (n ::: ns)
  where toNatListVal _ = toIntVal (NProxy :: NProxy n) : toNatListVal (NLProxy :: NLProxy ns)

data LLProxy (l :: ListList) = LLProxy

class ListListToVal (ll :: ListList) where toListListVal :: LLProxy ll -> List (List Int)
instance llToValNil :: ListListToVal LNil where toListListVal _ = Nil
else instance llToValCon ::
  ( NatListToVal nl
  , ListListToVal nls
  ) => ListListToVal (nl ::> nls)
  where toListListVal _ = toNatListVal (NLProxy :: NLProxy nl) : toListListVal (LLProxy :: LLProxy nls)

-- place one by prepend
placeOne :: Int -> List Int -> List (List Int)
placeOne n arr = go 0 Nil
  where
    go i acc
      | i == n      = acc
      | check arr i = go (i + 1) ((i : arr) : acc)
      | otherwise   = go (i + 1) acc

placeOneOnLL :: forall r. PlaceOne Three LL r => LLProxy r
placeOneOnLL = LLProxy

class Concat (as :: ListList) (bs :: ListList) (r :: ListList) | as bs -> r
instance concatNil :: Concat LNil bs bs
else instance concatOther :: Concat as bs r => Concat (a ::> as) bs (a ::> r)

llll :: forall r. Concat (LL ::> LNil) (LL ::> LNil) r => LLProxy r
llll = LLProxy

concat :: List (List Int) -> List (List Int) -> List (List Int)
concat Nil bs = bs
concat (a : as) bs = a : concat as bs

class PlaceOneMulti (n :: Nat) (ll :: ListList) (r :: ListList) | n ll -> r
instance placeOneMultiNil :: PlaceOneMulti n LNil LNil
else instance placeOneMultiOther ::
  ( PlaceOne n a r1
  , PlaceOneMulti n as r2
  , Concat r1 r2 r
  ) => PlaceOneMulti n (a ::> as) r

placeOneMulti :: Int -> List (List Int) -> List (List Int)
placeOneMulti n Nil = Nil
placeOneMulti n (a : as) = concat (placeOne n a) (placeOneMulti n as)

class NQueenGo (i :: Nat) (n :: Nat) (acc :: ListList) (r :: ListList) | i n acc -> r
instance nQueenGoTerminal :: NQueenGo n n acc acc
else instance nQueeGoOther ::
  ( Add One i i1
  , PlaceOneMulti n acc r1
  , NQueenGo i1 n r1 r
  ) => NQueenGo i n acc r

class NQueen (n :: Nat) (r :: ListList) | n -> r
instance nQueen' :: NQueenGo Zero n (NNil ::> LNil) r => NQueen n r

oneQueen :: forall r. NQueen One r => LLProxy r
oneQueen = LLProxy

fourQueen :: forall r. NQueen N4 r => LLProxy r
fourQueen = LLProxy

fiveQueen :: forall r. NQueen N5 r => LLProxy r
fiveQueen = LLProxy

sixQueen :: forall r. NQueen N6 r => LLProxy r
sixQueen = LLProxy

-- eightQueen :: forall r. NQueen N8 r => LLProxy r
-- eightQueen = LLProxy

nQueen :: Int -> List (List Int)
nQueen n = go 0 (Nil: Nil)
  where
    go i acc
      | i == n = acc
      | otherwise = go (i + 1) $ placeOneMulti n acc

logShow :: forall a. Show a => a -> Effect Unit
logShow = log <<< show

main :: Effect Unit
main = do
  void $ range 1 9 #
    traverse (logShow <<< length <<< nQueen)

  -- log $ "doesOnePlusOneEqualTwo = " <> show (toBoolVal doesOnePlusOneEqualTwo)
  -- log $ "onePlusTwo = " <> show (toIntVal onePlusTwo)
  -- log $ "doesOnePlusTwoEqualTwo = " <> show (toBoolVal doesOnePlusTwoEqualTwo)

  -- log $ "twoNotInLL = " <> show (toBoolVal twoNotInLL)
  -- log $ "threeNotInLL = " <> show (toBoolVal threeNotInLL)
  --
  -- log $ "absOneMinusThree = " <> show (toIntVal absOneMinusThree)
  -- log $ "LL = " <> show (toNatListVal ll)
  -- log $ "LLLL = " <> show (toListListVal llll)
  --
  -- log $ "placeOneOnLL = " <> show (toListListVal placeOneOnLL)

  log $ "oneQueen = " <> show (length $ toListListVal oneQueen)
  log $ "fiveQueen = " <> show (length $ toListListVal fiveQueen)
  log $ "sixQueen = " <> show (length $ toListListVal sixQueen)

the time to run

pulp run  432.91s user 215.26s system 292% cpu 3:41.68 total