[Haskell-cafe] existential quantification
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.
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
More information about the Haskell-Cafe
mailing list