### Re: existential quantification

MigMit <miguelimo38 <at> yandex.ru>

2013-12-02 17:47:12 GMT

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 <paratribulations <at> free.fr> wrote:
> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe