Why there is no an "Exist" keyword in Haskell for Existential Quantification?

Question

According to the GHC documentation, given the following declaration:

data Foo = forall a. MkFoo a (a -> Bool)
           | Nil

then

MkFoo :: forall a. a -> (a -> Bool) -> Foo

Is (nearly) isomorphic to the following pseudo-Haskell declaration

MkFoo :: (exists a . (a, a -> Bool)) -> Foo

Therefore, there is not need for a separated "Exist" keyword. Because:

Haskell programmers can safely think of the ordinary universally quantified type given above.

But I'm not sure what that means. Can someone please explain me why can we use the universal quantifier to express Existential quantification?

Answer 1

In logic (classical or intuitionistic), the formulas

(exists x. p x) -> q
forall x. (p x -> q)

are equivalent (note that q does not depend on x above). This can be used to express existential quantification in terms of universal quantification, provided the existential lies on the left side on an implication. (Here's a classical proof.)

In functional programming, you can achieve the same. Instead of writing

-- Pseudo-Haskell follows
f :: (exists a. (a, a->Int)) -> Int
f (x,h) = h x

we can use

-- Actual Haskell
f :: forall a. (a, a->Int) -> Int
f (x,h) = h x

so we can do without existential quantification, at least in cases such as the above.

Existential quantification is still needed when it occurs not on the left of an arrow. For instance,

g :: exists a. (a, a->Int)
g = (2 :: Int, \x -> x+3)

Alas, Haskell chose not to include these types. Likely, this choice was made to keep the already sophisticated type system from becoming too complex.

Still, Haskell got existential data types, which just require to wrap/unwrap one constructor around the existential. For example, using GADT syntax, we can write:

data Ex where
  E :: forall a. (a, a->Int) -> Ex
g :: Ex
g = E (2 :: Int, \x -> x+3)

Finally, let me add that existentials can also be simulated by rank-2 types and continuation-passing:

g :: forall r. (forall a. (a, a->Int) -> r) -> r
g k = k (2 :: Int, \x -> x+3)

Answer 2

The first thing to notice is that the forall quantifier appears on the right-hand side of the equal sign, so it is associated with a data constructor (not type): MkFoo. Thus, the type Foo says nothing about a.

We encounter a again when we try to pattern match on values of type Foo. At that point you'll know pretty much nothing about the components of MkFoo, except that they exist (there must exist a type used to call MkFoo) and that the first component can be used as an argument to the second component, which is a function:

f :: Foo -> Bool
f (MkFoo val fn) = fn val

Answer 3

If you look at the type of data constructors, you'll notice that we similarly use -> to somehow mean product. E.g.

(:) :: a -> [a] -> [a]

really means that we are using (:) to pack an a together with a list of type [a] and deliver a list of type [a].

In your example, the use of forall simply means that MkFoo, as a constructor, is willing to pack any type a. When you read (exists a . (a, a -> Bool)) -> Foo in the GHC documentation, you should think of it as an uncurried version of the original type of MkFoo. The corresponding uncurried version of (:) would be (a, [a]) -> [a].