Playing around

typePoker.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits (Symbol)

import Data.Typeable
import Data.Proxy
import Data.Kind
import Data.Singletons
import Data.Singletons.TH

data Nat = Z | Succ Nat deriving Show

-- type level list which has a Nat type to represent length
data Vector a n where
    Nil  :: Vector a Z
    (:-) :: a -> Vector a n -> Vector a (Succ n)

type family   Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z  m = m
type instance Plus (Succ n)  m = Succ (Plus n m)

-- adds the index of two vectors so new type is a vector with the combined lengths
type family VCons (v1 :: * ) (v2 :: *) :: *
type instance VCons (Vector a n1) (Vector a n2) = Vector a (Plus n1 n2)

deriving instance Eq a => Eq (Vector a n)
deriving instance Show a => Show (Vector a n)

append :: Vector a n -> Vector a m -> Vector a (Plus n m)
append (x :- xs) ys = x :- append xs ys
append Nil       ys = ys

--data Stage = PreDeal | PreFlop | Flop | Turn | River deriving Show

data Card = A | K | Q | J | Ten deriving Show

data GameStage = PreDeal | PreFlop | Flop | Turn | River deriving Show 

-- proxy
data Stage (s :: GameStage) where Stage :: Typeable s => Stage s

instance Typeable a => Show (Stage a) where
    showsPrec p x = showParen (p > 0) $ showString "" . shows (typeOf x)

type family Board' (board :: *) :: * where
    Board' (Vector Card Z) = Board 'PreDeal
    Board' (Vector Card (Succ (Succ Z))) = Board 'Flop

--type family Players (board :: *) :: Players where
--    Players (Vector String Z) = NoPlayers
--    Players (Vector String (Succ Z)) = OnePlayer
--    Players (Vector String (Succ (Succ Z))) = TwoPlayers

data Board (a :: GameStage) where Board :: Typeable a => Board a

deriving instance Typeable a => Show (Board a)

showsPrec p x = showParen (p > 0) $ showString "" . shows (typeOf x)

newtype PocketCards = PocketCards (Vector Card ('Succ ('Succ 'Z))) deriving Show
--
--data Player a = Player {
--    name :: String,
--    chips :: Int
--} deriving (Show, Eq)

$(singletons [d|
   data PlayerState = Folded | InHand | AllIn | SatOut
     deriving (Show, Eq)
  |])

data PlayerMaterial = PlayerMaterial {
  name :: String,  
  chips :: Int
} deriving (Show, Eq)

-- Player is an indexed data type (indexed by a type of kind PlayerState) in that picking a different type variable gives a different “type” of Player:
data Player :: PlayerState -> * where
    UnsafeMkPlayer :: { player :: PlayerMaterial } -> Player s

instance Typeable a => Show (Player a) where
  showsPrec p x = showParen (p > 0) $ showString " :: " . shows (typeOf x)
  
-- existential data type
-- useful for when we just want to use a value of type Player and we don't care about the PlayerState singleton type
-- Cases where we don't care about the player state mostly include serialisation and parsing so we want to bypass the singleton type PlayerState.
data SomePlayer :: * where
  MkSomePlayer :: Sing s -> Player s -> SomePlayer

mkPlayer :: Sing s -> PlayerMaterial -> Player s
mkPlayer _ = UnsafeMkPlayer

fromPlayer :: Sing s -> Player s -> SomePlayer
fromPlayer = MkSomePlayer

fromPlayer_ :: SingI s => Player s -> SomePlayer
fromPlayer_ = fromPlayer sing

playerStatus_ :: SingI s => Player s -> PlayerState
playerStatus_ = playerStatus sing

-- Reifies a PlayerState as an existentially quantified data type; lifting player state values to types
-- withPlayer takes a function which operates on a player embedded in a singleton and then reifies the playerState value back to the type level
withPlayer :: PlayerState -> PlayerMaterial -> (forall s. Sing s -> Player s -> p) -> p
withPlayer pState pMaterial f = withSomeSing pState $ \s -> f s (mkPlayer s pMaterial)

sitOut :: Player s -> Player 'SatOut
sitOut (UnsafeMkPlayer plyr) = UnsafeMkPlayer plyr

playerStatus :: Sing s -> Player s -> PlayerState
playerStatus SInHand _ = InHand
playerStatus SAllIn _ = AllIn
playerStatus SFolded _ = Folded
playerStatus SSatOut _ = SatOut

allInPlayer :: Player 'InHand -> Player 'AllIn
allInPlayer (UnsafeMkPlayer p) = UnsafeMkPlayer p

foldPlayer :: Player 'InHand -> Player 'Folded
foldPlayer (UnsafeMkPlayer p) = UnsafeMkPlayer p

sitPlayerIn :: Player 'SatOut -> Player 'InHand
sitPlayerIn (UnsafeMkPlayer p) = UnsafeMkPlayer p

sitPlayerOut :: Player 'Folded -> Player 'SatOut
sitPlayerOut (UnsafeMkPlayer p) = UnsafeMkPlayer p

type GameErr = String


type family CanAct (s :: PlayerState) :: Bool where
    CanAct 'InHand = 'True
    CanAct 'AllIn = 'False
    CanAct 'Folded = 'False
    CanAct 'SatOut = 'False

-- apply our singleton type PlayerState to our CanAct typefamilily which returns a singleton Bool
-- interleaving equality at the type and value level
playerCanAct :: Sing s -> Sing (CanAct s)
playerCanAct = \case 
    SInHand -> STrue
    SAllIn -> SFalse
    SFolded -> SFalse
    SSatOut -> SFalse

canRaise :: (CanAct s ~ 'True) => Player s -> Bool
canRaise _ = True

data Game (stage :: *) (board :: *) (players :: *) where
    PreDealGame :: Players n -> Game (Stage 'PreDeal) (Vector Card 'Z) players
    PreFlopGame :: Players n -> Game (Stage 'PreFlop) (Vector Card 'Z) players
    FlopGame :: Players n -> Vector Card ('Succ ('Succ ('Succ 'Z))) -> Game (Stage 'Flop) (Vector Card ('Succ ('Succ ('Succ 'Z)))) players
    TurnGame :: Players n -> Vector Card ('Succ 'Z) -> Game (Stage 'Turn) (Vector Card ('Succ ('Succ ('Succ ('Succ 'Z))))) players
    RiverGame :: Players n -> Vector Card ('Succ 'Z) -> Game (Stage 'River) (Vector Card ('Succ ('Succ ('Succ ('Succ ('Succ 'Z)))))) players

-- can't get this to work :/
--deriving instance (Show c, Show s, Show p) => Show (Game c s p)

newtype Players (n :: Nat) = Players (Vector SomePlayer n) 

instance Typeable n => Show (Players n) where
    showsPrec p x = showParen (p > 0) $ showString "" . shows x

someFunc = UnsafeMkPlayer @ 'SatOut PlayerMaterial { chips = 2000, name = "Zincy" }

-- We are using the type synonym variety of type families as we do not need injectivite instances - or in other words no two types ever map to the same type 
-- this reflects the fact that each type representing a game stage is unique
class Progress game where
    type NextPhase game
    progressGame :: game -> NextPhase game

instance Progress (Game (Stage 'PreDeal) (Vector Card 'Z) (Players n)) where
   type NextPhase (Game (Stage 'PreDeal) (Vector Card 'Z) (Players n)) = Game (Stage 'PreFlop) (Vector Card 'Z) (Players n)
   progressGame (PreDealGame ps) = PreFlopGame ps

instance Progress (Game (Stage 'PreFlop) (Vector Card 'Z) (Players n)) where
   type NextPhase (Game (Stage 'PreFlop) (Vector Card 'Z) (Players n)) = Game (Stage 'Flop) (Vector Card ('Succ ('Succ ('Succ 'Z)))) (Players n)
   progressGame (PreFlopGame ps) = FlopGame ps (dealCard (dealCard (dealCard Nil A) Q) K)


dealCard :: Vector Card n -> Card -> Vector Card (Succ n) 
dealCard board card = card :- board


allInSomePlayer :: SomePlayer -> Either GameErr (Player 'AllIn )
allInSomePlayer (MkSomePlayer s p) = case s of
    SInHand -> Right $ allInPlayer p
    SAllIn -> Left "cannot go allin when already all in" 
    SFolded -> Left "cannot go allin when folded"
    SSatOut -> Left "cannot go allin when satout"

sitSomePlayerOut :: SomePlayer -> Either GameErr (Player 'SatOut )
sitSomePlayerOut (MkSomePlayer s p) = case s of
    SInHand -> Left "cannot sit out when in hand" 
    SAllIn -> Left "cannot sit out when all in" 
    SFolded -> Right $ sitPlayerOut p
    SSatOut -> Left "cannot sit out when already satout"

sitSomePlayerIn :: SomePlayer -> Either GameErr (Player 'InHand)
sitSomePlayerIn (MkSomePlayer s p) = case s of
    SInHand -> Left "cannot sit in when already sat in" 
    SAllIn -> Left "cannot sit in when all in" 
    SFolded -> Left "cannot sit in when folded" 
    SSatOut -> Right $ sitPlayerIn p

foldSomePlayer :: SomePlayer -> Either GameErr (Player 'Folded)
foldSomePlayer (MkSomePlayer s p) = case s of
    SInHand -> Right $ foldPlayer p
    SAllIn -> Left "cannot fold when all in"
    SFolded -> Left "cannot fold when already folded" 
    SSatOut -> Left "cannot fold when sat out"