Knights

Knights.hs

{-# OPTIONS_GHC -Wno-missing-methods #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

nil = undefined
infixr 5 :::


-- Solution is a LIST of squares

data Nil
data h ::: tail
-- a ::: b ::: c ::: Nil


-- Solution is a list of SQUARES

data Square x y


-- Coords are NATURAL NUMBERS

data Z
data S n

type N1 = S Z
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 N9 = S N8


-- How does a knight MOVE?

class Apply func arg result | func arg -> result

-- (1, 2)
data Move1
instance Apply Move1 (Square x y) (Square (S x) (S (S y)))
-- (2, 1)
data Move2
instance Apply Move2 (Square x y) (Square (S (S x)) (S y))
-- (-1, 2)
data Move3
instance Apply Move3 (Square (S x) y) (Square x (S (S y)))
-- (2, -1)
data Move4
instance Apply Move4 (Square x (S y)) (Square (S (S x)) y)
-- (-2, 1)
data Move5
instance Apply Move5 (Square (S (S x)) y) (Square x (S y))
-- (1, -2)
data Move6
instance Apply Move6 (Square x (S (S y))) (Square (S x) y)
-- (-1, -2)
data Move7
instance Apply Move7 (Square (S x) (S (S y))) (Square x y)
-- (-2, -1)
data Move8
instance Apply Move8 (Square (S (S x)) (S y)) (Square x y)

class PossibleMoves sq moves | sq -> moves
instance (Apply Move1 sq move1,
          Apply Move2 sq move2,
          Apply Move3 sq move3,
          Apply Move4 sq move4,
          Apply Move5 sq move5,
          Apply Move6 sq move6,
          Apply Move7 sq move7,
          Apply Move8 sq move8) 
  => PossibleMoves sq (move1:::move2:::move3:::move4:::move5:::move6:::move7:::move8:::Nil)


-- A knight can move in all directions, positive and negative.
-- But we only have natural numbers. So let's SHIFT positions to stay natural.

data Shift
instance Apply Shift (Square x y) (Square (S (S x)) (S (S y)))

data Unshift
instance Apply Unshift (Square (S (S x)) (S (S y))) (Square x y)


-- But not all moves are safe. Our knight can fall off the board.
-- For each possible move we must determine whether it's SAFE.

-- Safe or not safe, it's a BOOLEAN

data True
data False


-- What is a safe shifted move?

data SafeShiftedMove
instance (LessThan x N2 smallx,
          LessThan y N2 smally,
          Or smallx smally small,
          LessThan N9 x largex,
          LessThan N9 y largey,
          Or largex largey large,
          Or small large bad,
          Not bad result)
  => Apply SafeShiftedMove (Square x y) result

class Or b1 b2 b | b1 b2 -> b
instance Or True  True  True
instance Or True  False True
instance Or False True  True
instance Or False False False

class Not b1 b | b1 -> b
instance Not False True
instance Not True  False

class LessThan a b t | a b -> t
instance LessThan Z     Z     False
instance LessThan (S a) Z     False
instance LessThan Z     (S b) True
instance (LessThan a b t)
  => LessThan (S a) (S b) t


-- First, we shift our initial square.
-- Second, we calculate all possible moves.
-- Third, we filter all unsafe moves.
-- Fourth, we unshift all safe moves back.

class SafePossibleMoves square moves | square -> moves
  where solution :: square -> moves
instance (Apply Shift square shiftedsquare,
          PossibleMoves shiftedsquare shiftedmoves,
          Filter SafeShiftedMove shiftedmoves safeshiftedmoves,
          Map Unshift safeshiftedmoves safemoves)
  => SafePossibleMoves square safemoves

class Filter func list list' | func list -> list'
instance Filter func Nil Nil
instance (Apply func h allowed,
          Filter func list list',
          AppendIf allowed h list' list'')
  => Filter func (h ::: list) list''

class AppendIf allowed h list list' | allowed h list -> list'
instance AppendIf True  h list (h ::: list)
instance AppendIf False h list list

class Map func list list' | func list -> list'
instance Map func Nil Nil
instance (Apply func h h', 
          Map func list list')
  => Map func (h ::: list) (h' ::: list')