Skip to content

Instantly share code, notes, and snippets.

@rayshih
Created September 2, 2018 18:24
Show Gist options
  • Save rayshih/fea2e98ca3da4049cba390e717fd4cbb to your computer and use it in GitHub Desktop.
Save rayshih/fea2e98ca3da4049cba390e717fd4cbb to your computer and use it in GitHub Desktop.
Typelevel N Queen in PureScript
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)
@rayshih
Copy link
Author

rayshih commented Sep 2, 2018

output:

1
0
0
2
10
4
40
92
352
oneQueen = 1
fiveQueen = 10
sixQueen = 4

@rayshih
Copy link
Author

rayshih commented Sep 2, 2018

the time to run

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment