TP paratribulations at free.fr
Mon Dec 2 22:07:28 UTC 2013

```Hi everybody,

I try to understand existential quantification. I have two questions.

He writes:

"""
So with Existential-Quantification, foralls in data definitions mean that,
the value contained *can* be of *any* suitable type, not that it *must* be
of *all* suitable types.
"""

This made me think to an error I obtained with the code:
---------------
test :: Show s => s
test = "foobar"
---------------

The error is:

Could not deduce (s ~ [Char])
from the context (Show s)
bound by the type signature for test :: Show s => s
[...]
`s' is a rigid type variable bound by
the type signature for test :: Show s => s

Indeed, `test :: Show s => s` means "for any type s which is an instance of
Show, test is a value of that type s". But for example "foobar" can't be an
Int that is an instance of Show, so it yields an error.
By comparison,

---------------
test :: Num a => a
test = 42
---------------

works because 42 can be a value of type Int or Integer or Float or anything
else that is an instance of Num.
So I thought that by using existential quantification, the first example
could work:

---------------
{-# LANGUAGE ExistentialQuantification #-}

test :: forall s . Show s => s
test = "asd"
---------------

But I obtain the same error, why?

2/
Is the notion of existential type related in some way to the classical
mathematical quantifier "∃" (Unicode symbol U+2203: "There exists")?
If yes, then why using "forall" for an "existential type"?

"""
7.4.4.1. Why existential?

What has this to do with existential quantification? Simply that MkFoo has
the (nearly) isomorphic type

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

But Haskell programmers can safely think of the ordinary universally
quantified type given above, thereby avoiding adding a new existential
quantification construct.
"""

But I don't understand the explanation.