WIP: Chess in Dhall

Chess.dhall

let List/replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate in

let File = Natural in
let Rank = Natural in
let Square = { file : File, rank : Rank } in
let Move = { from : Square, to : Square } in

let Side = < white : {} | black : {} > in
let white = < white = {=} | black : {} > in
let black = < black = {=} | white : {} > in

let Pawn = { hasMoved : Bool } in
let Rook = {} in
let Knight = {} in
let Bishop = {} in
let Queen = {} in
let King = { hasMoved : Bool } in
let defaultPawn : Pawn = { hasMoved = False } in
let defaultRook : Rook = {=} in
let defaultKnight : Knight = {=} in
let defaultBishop : Bishop = {=} in
let defaultQueen : Queen = {=} in
let defaultKing : King = { hasMoved = False } in
let PieceKind = < pawn : Pawn
                | rook : Rook
                | knight : Knight
                | bishop : Bishop
                | queen : Queen
                | king : King
                > in
let PK = constructors PieceKind in
let Piece = { side : Side, kind : PieceKind } in

-- TODO: Explore ways to enforce uniqueness. This approach doesn't
-- work because (==) isn't defined over Natural. Constraining the
-- domain also isn't a (simple) option because there's no Fin type.

-- Meanwhile I'm using List and giving up convincing Dhall to prevent
-- multiple pieces from occupying the same square.

{-
let Board = ∀(square : Square) → Optional Piece in
let emptyBoard : Board = λ(square : Square) → ([] : Optional Piece) in
let nonEmptyBoard : Board = λ(square : Square) →
    if square.file == +4 && square.rank == +0
    then [{ side = white
          , kind = < king = { hasMoved = False }
                   | pawn : Pawn
                   | rook : Rook
                   | knight : Knight
                   | queen : Queen
                   >
          }]
    else emptyBoard in
-}

let Position = { piece : Piece, square : Square } in
let Board = List Position in
let board : Board =
    let elites = [ PK.rook defaultRook
                 , PK.knight defaultKnight
                 , PK.bishop defaultBishop
                 , PK.queen defaultQueen
                 , PK.king defaultKing
                 , PK.bishop defaultBishop
                 , PK.knight defaultKnight
                 , PK.rook defaultRook
                 ] in
    let pawns = List/replicate +8 PieceKind (PK.pawn defaultPawn) in
    let fillRank =
          λ(rank : Rank)
        → λ(side : Side)
        → λ(kinds : List PieceKind)
        → List/fold PieceKind kinds (List Position)
            (λ(kind : PieceKind) → λ(positions : List Position) →
                positions # [{ piece = { side = side, kind = kind }
                             , square = { file = List/length Position positions
                                        , rank = rank
                                        }}])
            ([] : List Position) in
    fillRank +0 white elites #
    fillRank +1 white pawns #
    fillRank +6 black pawns #
    fillRank +7 black elites
in
let Game = { board : Board
           , turn : Side
           , pastMoves : List Move
           , legalMove : ∀(move : Move) → Bool
           } in
let newGame = { board = board
              , turn = white
              , pastMoves = ([] : List Move)
              -- TODO
              , legalMove = λ(move : Move) → False
              } in
let PlayGame = ∀(game : Game)
             → ∀(move : Move)
             → Optional Game in
board