Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Playing around
{-# 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"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment