Type level Indexing, type classes or something else?


I am exploring the world of type level programming writing a Poker Texas hold’em simulator. I think it is a good problem to solve with the right amount of type shenanigans. I think I have a good and simple example (almost boring) and I just want to share so other people learning type level programming so we can have an example other than peano arithmetic. Also I’d like to have some feedback: would you choose a different approach?



Looks like you’re wrestling with a minor variation on the expression problem here. With a fixed and flat set of types and a fixed and homogeneous set of operators, neither the typeclass approach nor the GADT approach has an especially compelling case for or against, IMO. Of course if your ‘pots’ are something you want to treat as an open set, the typeclass approach recommends itself, and if your operators are something you want to treat as an open set, your GADT approach works nicely.

But even if both sets are closed, there are cases when you want one versus the other for non-aesthetic reasons. If your types are more complex then your pot example, you may want to express that one of your types is a Foo, and eligible for all Foo operations, and that same type is also a Bar, and eligible for all Bar operations. This is easy to represent with typeclasses—create IsFoo and IsBar classes, and have types implement one, the other, or both—and requires some fancy and not particularly ergonomic row-type-like footwork, or a proliferation of indices, to represent with GADTs. Conversely, if your operations are more complex than your example, you may have an operation that takes two pots as inputs, and those pots might be of different varieties. With GADTs, you simply write this like you would write any other n-squared pattern match, with one clause for each pair of constructors. Representing heterogeneous operators via typeclasses is much more unpleasant.

1 Like

Thanks for sharing this! I love the simplicity of your example, somehow it made me click how to apply GADTs in practice!

1 Like

Thanks @Lsmor, nice tight example!

One downside of GADTs is that datatype field names become awkward. I see you’re not using field names; but accessing fields by position becomes easily confusable when you’ve many fields of the same type.

For example for your GADT Pot, both constructors have a field :: Amount, and you could name that amount for both. What you can’t do is apply amount myPot as with usual field names, nor update myPot{amount = 20}. Instead you must laboriously pattern match on the constructor to be sure you’re safely using amount.

1 Like

In those cases I often make helper functions like

{-# LANGUAGE LambdaCase #-}
type data PotKind = Side | Playing
data Pot (k :: PotKind) where
  SidePot :: Set Player -> Amount -> Pot Side 
  PlayingPot :: Map Player Amount -> Amount -> Pot Playing

getAmount :: Pot k -> Amount
getAmount = \case
  SidePot _ amount -> amount
  PlayingPot _ amount -> amount

changeAmount :: (Amount -> Amount) -> Pot k -> Pot k
changeAmount f = \case
  SidePot s amount -> SidePot s $ f amount
  PlayingPot m amount -> PlayingPot m $ f amount

It’s a bit of boiler plate, but I find it worth it in certain situations.

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

Now hang on, hang on. Let me tease out what’s going on. (And you’ll have to bear with me: I know nothing about Poker.)

Can Pots appear only as part of Tables? Or does a Pot have independent existence before/after a particular Table? Just because within a business domain there’s two different things that practitioners call by the same name doesn’t make them the same data item – even if the two things are both piles of money (amongst other attributes).

Within a TableState, there’s a PlayingPot with a set of Player; and a bunch of SidePots each with a set of Players. What’s the connection between these Players? Can any rando join a SidePot even though they’ve not put a stake in the PlayingPot? Can there be two SidePots that just by chance consist of the same set of Players and the same Amount? Then we really need a way to identify each SidePot rather than a List that might include duplicates.

IIRC Poker tables have a dealer, with players sitting around in a specific sequence. And there’s something about a player being able to take over the bank? Does the relative sequence of Players need to be represented in TableState?

If members of a SidePot must first be a Player in the PlayingPot, your data structures are not expressing the business rules; and the blahblah with two varieties of Pot is modelling a false separation.

Perhaps a SidePot should be modelled as merely an identifier and Amount. PlayingPot as a Map Player (Amount, Set SidePotId). With a Foreign Key from SidePotId – that to represent properly needs a Relational Database.

Type class abstraction – the only instances that we want to use are those of SidePot and PlayingPot

I think this is they key point motivating the type level index. At this point I would have then taken a slightly different turn: introduce a singleton and make Pot a type family. One drawback of the GADT approach is that, with a larger collection of types, you are baking the “pot contructor” into every GADT you define. You may as well share them. That’s what the singleton is!

It’s not particularly compelling for this small example, but I’ve written it out below. We’re using this style very successfully at work.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Singletons.TH (genSingletons)
import Data.Singletons (SingI, sing)
import Data.Set (Set)
import Data.Map (Map)
import Data.Kind (Type)
import Data.Monoid (Sum (Sum, getSum))

type Player = String
type Amount = Int

data PotKind = Side | Playing

$(genSingletons [''PotKind])

data SidePot where
  MkSidePot :: Set Player -> Amount -> SidePot

data PlayingPot where
  MkPlayingPot :: Map Player Amount -> Amount -> PlayingPot

type Pot :: PotKind -> Type
type family Pot a where
  Pot Side = SidePot
  Pot Playing = PlayingPot

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

-- | Calculates the total value of a pot. It would throw a warning if
-- I miss one of the constructors
totalValue :: forall k. SingI k => Pot k -> Amount
totalValue = case sing @k of
  SSide -> \(MkSidePot _ amnt) -> amnt
  SPlaying -> \(MkPlayingPot tpot amnt) -> amnt + getSum (foldMap Sum tpot)

-- | 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 (MkPlayingPot bets sharedAmount) = undefined
-- No compiler warning "incomplete patterns" despite "missing"

Well, That’s a good question. Roughly speaking, everytime a player goes all-in a Side Pot Is created. After the creation of a Side Pot other players can still play, first by matching the all-in player’s bets (hence, joining the Side Pot) and then by betting above the all-in player capacity (hence joining the Playing Pot)

If you enter the betting round with all-in then you are never part of the Playing Pot but you are part of the Side Pot (the one created by your all-in)

No, actually. a Side Pot always include the “last bet” (unless they win) of someone. Instead of a list of Side Pot you could use a Map Player (Side Pot), but thats an implementation detail irrelevant for the thing in disccussion which are Type indexes hahaha

Don’t know exactly what you mean, but I think no

No. For every pot you look who is participating, and the one with the highest hand, wins that pot. Notice a hand can have multiple winner, one for each pot (either playing pot, or side pot). The order, desn’t matter at all

Usually yes, but it isn’t necessary. In general:

  • a Player can be in many pots (playing or side)
  • Given two pots (playing or side), the set of players in it must be not equal (That is hard to represent at type level I think)
  • there is no relation “Players in Side must be in Playing”, but It is true the other way: “Players in Playing must be in all Side pots”

Given the last condition the representation PlayingPot = Map Player (Amount, Set SidePotId) looks promising, but there is a catch. Players in all-in situation do not participate in the playing pot, so they should be filter out when deciding who wins that pot. You could always represent all-in players as players with a zero amount… but that’s quite artificial. This representation has the advantage that you can decide who wins a pot by simply comparing the hands of the participant of the pot… of course, other representations could be possible

Nice… but I am afraid of singletons and tamplate haskell hahahaha, so I am not prepare for that solution yet. Nevertheless, I agree my example works, precisely because it is small, I don’t think it scale well…