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.

Angelika

I'm looking forward to a great answer. Thanks for asking. – Aphasia

This link: haskell.org/haskellwiki/Existential_type may be of some help. – Aphasia

Ctrl-F exists - one occurrence, and not in the main text... But I'm reading it, thank you very much – Angelika

@valya: yes. The Essential Haskell phd thesis linked there is perhaps worth reading too. – Aphasia

answers to this question may help: #3071636 – Patentee

Thank you for your awesome answers. I like mokus' and rampion's most, but I don't know which to choose. I'll use the answer with the most score tomorrow – Angelika

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

Residue

This is the functional way to do OOP's polymorphism. – Aphasia

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.

Eyelid

Since exists doesn't exist in Haskell, what would be the equivalent forall notation for your second example? exists a. Foo a => Int -> a – Sophistry

Answer 3

It means precisely "there exists a type a for which I can provide values of the following types in my constructor." Note that this is different from saying "the value of a is Int in my constructor"; in the latter case, I know what the type is, and I could use my own function that takes Ints as arguments to do something else to the values in the data type.

Thus, from the pragmatic perspective, existential types allow you to hide the underlying type in a data structure, forcing the programmer to only use the operations you have defined on it. It represents encapsulation.

It is for this reason that the following type isn't very useful:

data Useless = exists s. Useless s

Because there is nothing I can do to the value (not quite true; I could seq it); I know nothing about its type.

Regina

maybe you could elaborate a bit with not useless example? thank you very much. (your blog is awesome, by the way, teaches me a lot) – Angelika

Answer 4

UHC implements the exists keyword. Here's an example from its documentation

x2 :: exists a . (a, a -> Int)
x2 = (3 :: Int, id)

xapp :: (exists b . (b,b -> a)) -> a
xapp (v,f) = f v

x2app = xapp x2

And another:

mkx :: Bool -> exists a . (a, a -> Int)
mkx b = if b then x2 else ('a',ord)

y1 = mkx True -- y1 :: (C_3_225_0_0,C_3_225_0_0 -> Int)
y2 = mkx False -- y2 :: (C_3_245_0_0,C_3_245_0_0 -> Int)

mixy = let (v1,f1) = y1
            (v2,f2) = y2
       in f1 v2

"mixy causes a type error. However, we can use y1 and y2 perfectly well:"

main :: IO ()
main = do putStrLn (show (xapp y1))
          putStrLn (show (xapp y2))

ezyang also blogged well about this: http://blog.ezyang.com/2010/10/existential-type-curry/

Patentee