[Haskell-cafe] existential quantification

[Brandon Allbery]

On Mon, Dec 2, 2013 at 5:07 PM, TP <paratribulations at free.fr> wrote:

> ---------------
> 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.
>
 (...)

> So I thought that by using existential quantification, the first example
> could work:
>
> ---------------
> {-# LANGUAGE ExistentialQuantification #-}
>
> test :: forall s . Show s => s
> test = "asd"
> ---------------
>

This is actually the same as the first one; top level type variables (that
is, outside of parentheses) are always `forall`.

And just tossing a `forall` in there does not mean you can claim to be any
type and then force a `String` down the caller's throat.

Which brings us to what is *really* going on. When you write

    test :: Show s => s

you are saying exactly and only this:

    Any function that calls me can request *any* type that has an instance
of Show, and I will give them *that type*.

It still means that if you add an explicit `forall`.

It does not, nor can it be forced to mean, that you will only ever give
them a String. Likewise, it does not, nor can it be forced to mean, that
you can pick a different type based on (the value of a function parameter,
the value of an environment variable, the phase of the moon).

Haskell does not use an OO type system; there is no java.lang.Object that
can be every possible type, and `forall` does not create one. You cannot
represent in Haskell the kind of type that you are trying to write. (There
is something you can do that is almost the same, but requires a constraint
and can only represent monomorphic types. And *still* does not give you
java.lang.Object; it gives you a thing which has a specific type and
"contains" a thing with another specific type, but can be queried about
what that type is and can be extracted *only* in a context that requires
that type.)

When `forall` is useful is inside parentheses in a type. I am not sure that
I can provide a useful example that I can explain meaningfully until you
understand the above. (But others here probably can....)


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

Because "there exists" and "for all" are related by DeMorgan's rule (think
about it), and "for all" is easier to represent in GHC's type machinery. I
believe UHC provides an "exists" type quantifier as well as "forall".

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

"You don't have to keep two different kinds of quantification in mind, or
figure out how they interact with each other and non-quantified types,
since you can write one in terms of the other."

-- 
brandon s allbery kf8nh                               sine nomine associates
allbery.b at gmail.com                                  ballbery at sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131202/bf914ee1/attachment.html>