pepega

type.hs

{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilyDependencies   #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}

import Prelude (Bool (True, False))

import           Data.Kind     (Type)
import           GHC.TypeLits  (ErrorMessage (..), TypeError)

-- I considered using a typeclass here instead (with an associated type family).
-- But there's no real way to get full type safety with it. It'd be possible to write bogus instances.
type ($) :: TLam a r -> a -> r
type family f $ a

infixr 0 $

data TFunSym :: Type -> Type -> Type

data LiftCon :: (a -> r) -> TLam a r
type instance LiftCon con $ x = con x

data LiftCon2 :: (a -> b -> r) -> TLam a (TLam b r)
type instance LiftCon2 con $ x = LiftCon (con x)

-- You literally can't give any of these type families below the wrong kinds.
-- sound type systems!!!
type TLam a r = TFunSym a r -> Type

type Id :: a -> a
type family Id x = r | r -> x where
  Id x = x

type Id0 :: TLam a a
data Id0 lam
type instance Id0 $ x = Id x

type Flip :: TLam a (TLam b c) -> b -> a -> c
type family Flip f b a where
  Flip f b a = (f $ a) $ b

type Flip2 :: TLam a (TLam b c) -> b -> TLam a c
data Flip2 f a lam
type instance Flip2 f a $ b = Flip f a b

data List x = Nil | Cons x (List x)

type First :: List k -> k
type family First l where
  -- Haskell is a dynamically typed language with runtime type errors.
  First Nil        = TypeError (Text "First: empty list")
  First (Cons x _) = x

type (++) :: List k -> List k -> List k
type family a ++ b where
  Nil       ++ b = b
  Cons x xs ++ b = Cons x (xs ++ b)

infixr 5 ++

-- Concatenate all lists in a list
type ListConcatAll :: List (List k) -> List k
type family ListConcatAll ll = r where
  ListConcatAll Nil         = Nil
  ListConcatAll (Cons x xs) = x ++ ListConcatAll xs

-- Is any element of this list True?
type AnyTrue :: List Bool -> Bool
type family AnyTrue l = r where
  AnyTrue Nil             = False
  AnyTrue (Cons False xs) = AnyTrue xs
  AnyTrue (Cons True xs)  = True

type Not :: Bool -> Bool
type family Not b = r | r -> b where
  Not True  = False
  Not False = True

type (||) :: Bool -> Bool -> Bool
type family a || b where
  True  || _     = True
  False || other = other

infixr 2 ||

type IfThenElse :: Bool -> a -> a -> a
type family IfThenElse b x y = r where
  IfThenElse True x _ = x
  IfThenElse False _ y = y

data Nat = Z | S Nat

type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7

type (==) :: Nat -> Nat -> Bool
type family a == b where
  Z     == Z     = True
  (S a) == Z     = False
  Z     == (S b) = False
  (S a) == (S b) = a == b

infixr 4 ==

type (<) :: Nat -> Nat -> Bool
type family a < b where
  Z     < Z     = False
  (S a) < Z     = False
  Z     < (S b) = True
  (S a) < (S b) = a < b

infixr 4 <

type (~-) :: Nat -> Nat -> Nat
type family a ~- b where
  Z     ~- Z     = Z
  Z     ~- (S b) = S b
  (S a) ~- Z     = S a
  (S a) ~- (S b) = a ~- b

infixl 6 ~-

type Range :: Nat -> List Nat
type family Range n = r | r -> n where
  Range Z     = Nil
  Range (S n) = Cons n (Range n)

type (<$>) :: TLam a r -> List a -> List r
type family f <$> l where
  f <$> Nil       = Nil
  f <$> Cons x xs = Cons (f $ x) (f <$> xs)

infixl 4 <$>

-- GHC actually managed to infer this kind signature, with the nice TLam kind synonym and everything.
-- I am very scared of GHC now.
type MapCat :: TLam a (List x) -> List a -> List x
type family MapCat f l where
  MapCat f Nil = Nil
  MapCat f xs = ListConcatAll (f <$> xs)

type Filter :: TLam a Bool -> List a -> List a
type family Filter pred l where
  Filter pred Nil = Nil
  Filter pred (Cons x xs) =
    IfThenElse
      (pred $ x)
      (LiftCon (Cons x))
      Id0
    $ Filter pred xs

data Queen x y = Queen x y

type QueenPos = Queen Nat Nat
type Config = List QueenPos
type Configs = List Config

type QueensInRow :: Nat -> Nat -> Config
type family QueensInRow n a where
  QueensInRow n x = LiftCon ('Queen x) <$> Range n

type Threatens :: QueenPos -> QueenPos -> Bool
type family Threatens a b where
  Threatens ('Queen ax ay) ('Queen bx by) =
    ax == bx
      || ay == by
      || ax ~- bx == ay ~- by

type Threatens1 :: QueenPos -> TLam QueenPos Bool
data Threatens1 a lam
type instance Threatens1 a $ b = Threatens a b

type Safe :: Config -> QueenPos -> Bool
type family Safe config queen where
  Safe config queen = Not (AnyTrue (Threatens1 queen <$> config))

type Safe1 :: Config -> TLam QueenPos Bool
data Safe1 as lam
type instance Safe1 xs $ ys = Safe xs ys

type AddQueen :: Nat -> Nat -> Config -> Configs
type family AddQueen n x config where
  AddQueen n x config = Flip2 (LiftCon2 'Cons) config <$> Filter (Safe1 config) (QueensInRow n x)

type AddQueen2 :: Nat -> Nat -> TLam Config Configs
data AddQueen2 n x lam
type instance AddQueen2 n x $ c = AddQueen n x c

type AddQueenToAll :: Nat -> Nat -> Configs -> Configs
type family AddQueenToAll n x cs where
  AddQueenToAll n x cs = MapCat (AddQueen2 n x) cs

type AddQueensIf :: Bool -> Nat -> Nat -> Configs -> Configs
type family AddQueensIf pred n x cs where
  AddQueensIf False _ _ cs = cs
  AddQueensIf True n x cs = AddQueens n (S x) (AddQueenToAll n x cs)

type AddQueens :: Nat -> Nat -> Configs -> Configs
type family AddQueens n x cs where
  AddQueens n x cs = AddQueensIf (x < n) n x cs