typelevel stuff

Poker.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}


import GHC.TypeLits (Symbol)
import Data.Typeable
import Data.Proxy


data Nat = Z | Succ Nat deriving Show

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)

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 (a :: GameStage) where Stage :: Typeable a => Stage a

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


type family Game' (stage :: *) (board :: *) :: * where
    Game' (Stages 'PreDeal) (Vector Card Z) = Game (Stage 'PreDeal) (Vector Card 'Z)
    Game' (Stage 'PreFlop) (Vector Card (Succ Z)) = Game (Stage 'PreFlop) (Vector Card ('Succ 'Z))
 
 data Game (stage :: *) (board :: *) where 
     PreDealGame :: Stage 'PreDeal -> Vector Card 'Z -> Game (Stage 'PreDeal) (Vector Card 'Z)
     PreFlopGame :: Stage 'PreFlop -> Vector Card ('Succ 'Z) -> Game (Stage 'PreFlop) (Vector Card ('Succ 'Z))
     
 deriving instance (Show a, Show b) => Show (Game a b)