What does “exists” mean in Haskell type system?

A use of existential types that I’ve run into is with my code for mediating a game of Clue.

My mediation code sort of acts like a dealer. It doesn’t care what the types of the players are – all it cares about is that all the players implement the hooks given in the Player typeclass.

class Player p m where
  -- deal them in to a particular game
  dealIn :: TotalPlayers -> PlayerPosition -> [Card] -> StateT p m ()

  -- let them know what another player does
  notify :: Event -> StateT p m ()

  -- ask them to make a suggestion
  suggest :: StateT p m (Maybe Scenario)

  -- ask them to make an accusation
  accuse :: StateT p m (Maybe Scenario)

  -- ask them to reveal a card to invalidate a suggestion
  reveal :: (PlayerPosition, Scenario) -> StateT p m Card

Now, the dealer could keep a list of players of type Player p m => [p], but that would constrict
all the players to be of the same type.

That’s overly constrictive. What if I want to have different kinds of players, each implemented
differently, and run them against each other?

So I use ExistentialTypes to create a wrapper for players:

-- wrapper for storing a player within a given monad
data WpPlayer m = forall p. Player p m => WpPlayer p

Now I can easily keep a heterogenous list of players. The dealer can still easily interact with the
players using the interface specified by the Player typeclass.

Consider the type of the constructor WpPlayer.

    WpPlayer :: forall p. Player p m  => p -> WpPlayer m

Other than the forall at the front, this is pretty standard haskell. For all types
p that satisfy the contract Player p m, the constructor WpPlayer maps a value of type p
to a value of type WpPlayer m.

The interesting bit comes with a deconstructor:

    unWpPlayer (WpPlayer p) = p

What’s the type of unWpPlayer? Does this work?

    unWpPlayer :: forall p. Player p m => WpPlayer m -> p

No, not really. A bunch of different types p could satisfy the Player p m contract
with a particular type m. And we gave the WpPlayer constructor a particular
type p, so it should return that same type. So we can’t use forall.

All we can really say is that there exists some type p, which satisfies the Player p m contract
with the type m.

    unWpPlayer :: exists p. Player p m => WpPlayer m -> p

Leave a Comment

Hata!: SQLSTATE[HY000] [1045] Access denied for user 'divattrend_liink'@'localhost' (using password: YES)