Why there is no an "Exist" keyword in Haskell for Existential Quantification?
haskell
Solution
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)
Problem
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?