What does "exists" mean in Haskell type system?

Question

I'm struggling to understand the exists keyword in relation to Haskell type system. As far as I know, there is no such keyword in Haskell by default, but:

• There are extensions which add them, in declarations like these data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
• I've seen a paper about them, and (if I recall correctly) it stated that exists keyword is unnecessary for type system since it can be generalized by forall

But I can't even understand what exists means.

When I say, forall a . a -> Int, it means (in my understanding, the incorrect one, I guess) "for every (type) a, there is a function of a type a -> Int":

myF1 :: forall a . a -> Int myF1 _ = 123 -- okay, that function (`a -> Int`) does exist for any `a` -- because we have just defined it 

When I say exists a . a -> Int, what can it even mean? "There is at least one type a for which there is a function of a type a -> Int"? Why one would write a statement like that? What the purpose? Semantics? Compiler behavior?

myF2 :: exists a . a -> Int myF2 _ = 123 -- okay, there is at least one type `a` for which there is such function -- because, in fact, we have just defined it for any type -- and there is at least one type... -- so these two lines are equivalent to the two lines above 

Please note it's not intended to be a real code which can compile, just an example of what I'm imagining then I hear about these quantifiers.

---

P.S. I'm not exactly a total newbie in Haskell (maybe like a second grader), but my Math foundations of these things are lacking.

Answer 1

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 

Answer 2

When I say, forall a . a -> Int, it means (in my understanding, the incorrect one, I guess) "for every (type) a, there is a function of a type a -> Int":

Close, but not quite. It means "for every type a, this function can be considered to have type a -> Int". So a can be specialized to any type of the caller's choosing.

In the "exists" case, we have: "there is some (specific, but unknown) type a such that this function has the type a -> Int". So a must be a specific type, but the caller doesn't know what.

Note that this means that this particular type (exists a. a -> Int) isn't all that interesting - there's no useful way to call that function except to pass a "bottom" value such as undefined or let x = x in x. A more useful signature might be exists a. Foo a => Int -> a. It says that the function returns a specific type a, but you don't get to know what type. But you do know that it is an instance of Foo - so you can do something useful with it despite not knowing its "true" type.