[Haskell-cafe] existential quantification

[TP]

Hi everybody,


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

1/ I have just read the answer of yairchu at

http://stackoverflow.com/questions/3071136/what-does-the-forall-keyword-in-haskell-ghc-do

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"?

At the following address 

http://www.haskell.org/ghc/docs/6.12.1/html/users_guide/data-type-extensions.html#existential

we read

"""
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.

Thanks in advance,

TP