[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


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?

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 


we read

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


More information about the Haskell-Cafe mailing list