Type Level Poker.md

Representing Poker Pots Safely

This is a personal exploration of type-level programming. I am sharing this as an example of how a little bit of type-level programming can lead to better and safer APIs. Also, it uses an example other than Peano arithmetic.

For context:

• A 'side pot' is one in which some players participate, all of them with the same amount of money.
• A 'playing pot' is one in which some players participate, each with potentially different amounts and with some shared money (blinds and folds).

In any given round, there might be many side pots (or zero) but one and only one playing pot.

Let's explore different ways of representing the pot and how they lead to different APIs.

Pot as Records

The first (naive) idea is to express the pot as a simple record:

data Pot = MkPot { playersBets :: (Map Player Amount), shared :: Amount }

createSidePot :: [Player]  -- The list of players in the pot
              -> Amount     -- The (equal) amount each player participates with
              -> Pot 
createSidePot = ... --- creates a pot with zero amount for each player and a shared amount for all of them

createPlayingPot :: [(Player, Amount)] -- The map of players and the amount each participates with
                 -> Amount             -- The shared amount.
createPlayingPot = ... --- do the obvious thing.                

There are many things wrong with this representation. First, nothing guarantees that a side pot has the property: "All players must participate with the same amount." Of course, the createSidePot function can guarantee that, but afterwards, every time you use a side pot, you must check such a property; otherwise, you risk creating money out of thin air or removing money from the game.

Another (yet hidden) problem is that you can't differentiate between a playing pot and a side pot, neither at the type level nor at the term level, unless you add a third field like isSidePot :: Bool, which just introduces yet another thing to check constantly throughout the code.

Pot as an ADT

The second approach is to use an old (but gold) ADT so we can differentiate at the term level.

data Pot 
  = SidePot (Set Player) Amount          -- Who participates and the total value.
  | PlayingPot (Map Player Amount) Amount -- Who participates with how much money, and the shared amount.

We have solved some problems that the record representation had:

• We can guarantee a side pot has the same amount for every player.
• We can differentiate at the term level (via pattern matching) between a side pot and a playing pot (throwing compiler warnings if we forget).

But one problem remains unsolved: we can't differentiate them at the type level. Think about it: how do we represent the state of the table? AFAIK, with this representation, we jump straight into unsafety.

data TableState = MkTableState {playingPot :: Pot, sidePots :: [Pot], ...}

Do you spot the problem? The playingPot field isn't just any kind of pot: it must be the PlayingPot constructor. The same applies to sidePots. We can't express this fact in the types, so there is a chance we mess up and build a TableState with a SidePot in the place of the playingPot.

There is a second problem with this approach: partial functions. You may want to write a function that folds a player (that is, moves its bets to the shared amount), but players can fold only if the pot is a playing pot. Also, you can create a side pot out of a playing pot, but not the other way around, etc.

Pots as a Type Class

data SidePot = MkSidePot (Set Player) Amount             -- Who participates and the total value.
data PlayingPot = MkPlayingPot (Map Player Amount) Amount -- Who participates with how much money, and the shared amount.

data TableState = MkTableState {playingPot :: PlayingPot, sidePots :: [SidePot], ...}

Okay, so now we've solved all the problems:

• We can guarantee the invariants of a SidePot.
• We can differentiate them at the term level.
• We can differentiate them at the type level.
• We can get rid of partial functions.

Yet... it feels like it shouldn't be two types. At the end of the day, they are both pots, so they will share a lot of functionality. For example, if you had one single type, you could write:

potTotalValue :: Pot -> Amount
potTotalValue = ...

queryAmount :: Player -> Pot -> Amount
queryAmount = ...

doesPlayerParticipate :: Player -> Pot -> Bool
doesPlayerParticipate = ...

But now you can't; Pot is not a single type anymore, so you have to either create a duplicate interface or abstract away with type classes or records.

data SidePot = MkSidePot (Set Player) Amount             -- Who participates and the total value.
data PlayingPot = MkPlayingPot (Map Player Amount) Amount -- Who participates with how much money, and the shared amount.

data TableState = MkTableState {playingPot :: PlayingPot, sidePots :: [SidePot], ...}

{-
API duplication.

This feels just wrong... It is bearable if the pot API is small enough, but it doesn't scale.
-}
sidepotTotalValue :: SidePot -> Amount
sidepotTotalValue = ...


playingpotTotalValue :: PlayingPot -> Amount
playingpotTotalValue = ...

{-
Type class abstraction

Probably, many would go this way, but it feels just artificial. IsPot is completely ad hoc and has no real meaning.
It is just a bunch of functions we push there for convenience. Also, the only instances that we want to use
are those of SidePot and PlayingPot. This is probably fine if we are building a binary, but we have to admit
the type class mechanism is intended for extensible interfaces, not for an interface with just two possibilities.

Also, there is the argument of "type classes must have laws," but I am not going this deep.
-}

class IsPot p where
   totalValue :: p -> Amount
   queryAmount :: Player -> p -> Amount
   ...

instance IsPot SidePot where
  ... 

instance IsPot PlayingPot where
  ... 

{-
Records abstraction

Not terrible, but it suffers the same issues as the type class solution (afaik, the compiler desugars type classes into this). 
PotCalculator doesn't represent something real (some element of poker), whereas a Pot type does.

To me, PotCalculator is like those OOP patterns in which classes become a mechanism instead of a representation of 
the business problem (e.g., factory pattern, singleton pattern, etc.). We would like our types/classes 
to represent something in the space of the problem we want to solve, not hacks for us to abstract our code.
-}

newtype PotCalculator p = PotCalculator {totalValue :: p -> Amount, ...}

spCalculator :: PotCalculator SidePot
spCalculator = PotCalculator {...}

ppCalculator :: PotCalculator PlayingPot
ppCalculator = PotCalculator {...}

As a conclusion, none of the solutions in this section are terrible, but they feel far from optimal.

GADTs and Kind Indexing

After experimenting with type-level programming, I reached this solution which looks very nice. Nevertheless, something in my gut tells me that I can push the type system a little bit more. Let's go straight to the code and we'll comment on it later.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeData #-} 
-- You could use DataKind instead, but TypeData looks a little bit easier

type data PotKind = Side | Playing
data Pot (k :: PotKind) where
  -- Notice the return type of each constructor. 
  SidePot :: Set Player -> Amount -> Pot Side 
  PlayingPot :: Map Player Amount -> Amount -> Pot Playing

data TableState = MkTableState {playingPot :: Pot Playing, sidePots :: [Pot Side], ...}

Objectively, there is some duplication: we have Side and Playing repeated in the constructors and in the types. But we solve all the problems we have:

• We can guarantee the invariants of SidePot.
• We can differentiate them at the term level (via pattern matching).
• We can differentiate them at the type level (via kind index).
• We can get rid of partial functions.
• We can have a shared interface without resorting to ad-hoc abstractions.

The beautiful thing about this solution is that we can choose between leaving the kind free (hence writing a function for both constructors), or making the kind explicit (hence writing the function for one constructor). Let me show:

-- | Calculates the total value of a pot. It would throw a warning if I miss one of the constructors
totalValue :: Pot k -> Amount
totalValue (SidePot _ amnt) = amnt
totalValue (PlayingPot tpot amnt) = amnt + getSum (foldMap Sum tpot)
-- No need for a type class. totalValue is defined normally, pattern matching on the constructors

-- | Moves player's bet to the shared amount. It only makes sense to define this function for playing pots...
foldPlayer :: Player -> Pot Playing -> Pot Playing
foldPlayer ply (PlayingPot bets sharedAmount) = ... 
-- No compiler warning "incomplete patterns" despite "missing"

Conclusion

This is just the surface of type level programming, but I think it does help a lot to see an easy (rather boring) example and compare it with alternatives.