Skip to content

Instantly share code, notes, and snippets.

@therewillbecode
Last active May 13, 2019
Embed
What would you like to do?
typelevel stuff
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment