Dark dependently-typed magic

Spells.hs

-- https://www.reddit.com/r/haskell/comments/dywiqx/question_about_disallowing_impossible_states/
-- and influenced by https://gist.github.com/gelisam/3dd536882296f672d3bcdfd88c98ac10

{-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies #-}

module Spells where

data Nat where
  Zero :: Nat
  Suc  :: Nat -> Nat

-- | A spellbook is isomorphic to a list of booleans indexed by the number of
-- bits that have been set (spells that have been cast).  It could be indexed by
-- length, if needed.
data Spellbook (castSpells :: Nat) where
  SbNil    :: Spellbook Zero
  SbCast   :: Spellbook castSpells -> Spellbook (Suc castSpells)
  SbUncast :: Spellbook castSpells -> Spellbook castSpells

-- | A single spell in a spellbook, which has not yet been cast.  The magic
-- incantation for a spell changes depending on whether preceding spells have
-- been cast.  Such is the nature of magic.
data Spell (spellbook :: Spellbook castSpells) where
  -- | Cast the spell on the current page (it cannot have been cast yet).
  Xyzzy  :: Spell (SbUncast spellbook)
  -- | Turn the page past a previously-cast spell.
  Plugh  :: Spell spellbook -> Spell (SbCast spellbook)
  -- | Turn the page past a not-yet-cast spell.
  Plover :: Spell spellbook -> Spell (SbUncast spellbook)

-- | Casting a spell transforms the spellbook and increments the number of cast
-- spells.  This definition is total, but sadly GHC does not even attempt to
-- verify this for us.
type family Cast (spellbook :: Spellbook castSpells) (spell :: Spell spellbook) :: Spellbook (Suc castSpells) where
  Cast (SbUncast spellbook) Xyzzy          = SbCast spellbook
  Cast (SbCast   spellbook) (Plugh  spell) = SbCast   (Cast spellbook spell)
  Cast (SbUncast spellbook) (Plover spell) = SbUncast (Cast spellbook spell)


data Result where
  P1Win :: Result
  P2Win :: Result
  Tie   :: Result

-- | Calculate the winner when the given spells are cast.  This does not depend
-- on previously-cast spells, though it could.
--
-- Here we assume there are only three spells in the spellbook.  Again, if we
-- miss any cases, GHC does not complain and we may not notice until this type
-- family gets stuck calculating scores.
type family ScoreSpell (spell1 :: Spell spellbook1) (spell2 :: Spell spellbook2) :: Result where
  ScoreSpell (p Xyzzy) Xyzzy = P1Win
  ScoreSpell (p (p' Xyzzy)) (p'' Xyzzy) = P1Win
  ScoreSpell Xyzzy (p (p' Xyzzy)) = P1Win

  ScoreSpell Xyzzy (p Xyzzy) = P2Win
  ScoreSpell (p Xyzzy) (p' (p'' Xyzzy)) = P2Win
  ScoreSpell (p (p' Xyzzy)) Xyzzy = P2Win

  ScoreSpell Xyzzy Xyzzy = Tie
  ScoreSpell (p Xyzzy) (p' Xyzzy) = Tie
  ScoreSpell (p (p' Xyzzy)) (p'' (p''' Xyzzy)) = Tie


-- | Record of the results up to the given turn, as a vector of 'Result's.
data Results (turn :: Nat) where
  Nil  :: Results Zero
  Cons :: Result -> Results n -> Results (Suc n)

-- | Count wins for player 1.
type family P1Score (results :: Results turn) :: Nat where
  P1Score Nil = Zero
  P1Score (Cons P1Win results) = Suc (P1Score results)
  P1Score (Cons _     results) = P1Score results

-- | Count wins for player 2.
type family P2Score (results :: Results turn) :: Nat where
  P2Score Nil = Zero
  P2Score (Cons P2Win results) = Suc (P2Score results)
  P2Score (Cons _     results) = P2Score results


-- | The state of the game on the given turn consists of the spellbooks of each
-- player, and the results so far.
data GameState (turn :: Nat) where
  MkGameState :: Spellbook turn -> Spellbook turn -> Results turn -> GameState turn

-- | Project out the spellbook for player 1.
type family P1Spellbook (game :: GameState turn) :: Spellbook turn where
  P1Spellbook (MkGameState spellbook1 _ _) = spellbook1

-- | Project out the spellbook for player 2.
type family P2Spellbook (game :: GameState turn) :: Spellbook turn where
  P2Spellbook (MkGameState _ spellbook2 _) = spellbook2

-- | Tot up the scores (so far) for each player.
type family Scores (game :: GameState turn) :: (Nat, Nat) where
  Scores (MkGameState _ _ results) = '(P1Score results, P2Score results)


-- | Play a round of the game, using the current state and spells cast by each
-- player to produce the new state.
type family Play (game :: GameState n) (spell1 :: Spell (P1Spellbook game)) (spell2 :: Spell (P2Spellbook game))
                 :: GameState (Suc n) where
  Play (MkGameState spellbook1 spellbook2 results) spell1 spell2
    = MkGameState (Cast spellbook1 spell1)
                  (Cast spellbook2 spell2)
                  (Cons (ScoreSpell spell1 spell2) results)


-- | The initial spellbook determines the number of spells available to each player.
type InitialSpellbook = SbUncast (SbUncast (SbUncast SbNil))

-- | The initial game state.
type InitialState = MkGameState InitialSpellbook InitialSpellbook Nil

-- | An example play through. Player 2 seems to have the upper hand.
type Example1Round1 = Play InitialState Xyzzy (Plover Xyzzy)
type Example1Round2 = Play Example1Round1 (Plugh Xyzzy) (Plover (Plugh Xyzzy))
type Example1Round3 = Play Example1Round2 (Plugh (Plugh Xyzzy)) Xyzzy
type FinalScore1    = Scores Example1Round3

{-
*Spells> :kind! Example1Round1
Example1Round1 :: GameState ('Suc 'Zero)
= 'MkGameState
    ('SbCast ('SbUncast ('SbUncast 'SbNil)))
    ('SbUncast ('SbCast ('SbUncast 'SbNil)))
    ('Cons 'P2Win 'Nil)

*Spells> :kind! Example1Round3
Example3 :: GameState ('Suc ('Suc ('Suc 'Zero)))
= 'MkGameState
    ('SbCast ('SbCast ('SbCast 'SbNil)))
    ('SbCast ('SbCast ('SbCast 'SbNil)))
    ('Cons 'P2Win ('Cons 'P2Win ('Cons 'P2Win 'Nil)))

*Spells> :kind! FinalScore1
FinalScore :: (Nat, Nat)
= '( 'Zero, 'Suc ('Suc ('Suc 'Zero)))
-}

-- | Another example play through.
type Example2Round1 = Play InitialState Xyzzy Xyzzy
type Example2Round2 = Play Example2Round1 (Plugh (Plover Xyzzy)) (Plugh Xyzzy)
type Example2Round3 = Play Example2Round2 (Plugh Xyzzy) (Plugh (Plugh Xyzzy))
type FinalScore2    = Scores Example2Round3



{-
-- Just to demonstrate that illegal moves are forbidden by the type-checker
-- (with an error message that reflects the consequences of dabbling with dark
-- magic beyond human comprehension):

*Spells> :kind! Play Example1Round1 (Plugh Xyzzy) (Plover Xyzzy)

<interactive>:1:36: error:
    • Expected kind ‘Spell (P2Spellbook Example1Round1)’,
        but ‘Plover Xyzzy’ has kind ‘Spell
                                       ('SbUncast ('SbUncast spellbook0))’
    • In the third argument of ‘Play’, namely ‘(Plover Xyzzy)’
      In the type ‘Play Example1Round1 (Plugh Xyzzy) (Plover Xyzzy)’
-}