There is just one place where "forall" means "any suitable type", and that's in "data" (or "newtype") declaration, BEFORE the data constructor. Like this:
newtype T = forall s. Show s => T s
Then you can have
test :: T
test = T "foobar".
If "forall" is AFTER the data constructor, it means that the value should have ALL suitable types simultaniously. Like this:
data T = T (forall s. Show s => s).
Then you CAN'T have
test = T "foobar"
because "foobar" has only one type, String; it's not polymorphic. On the other hand, if you happen to have a value of type T, you can treat the value inside it as a value of any suitable type, like this:
baz :: T -> String
baz (T s) = s
Same thing happens if you use "forall" without defining a new type, like
test :: forall s => Show s => s
It differs from the previous example just by one level of indirection, that's all.
On 03 Dec 2013, at 02:07, 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-h...
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...
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe