[Haskell-cafe] existential quantification

MigMit miguelimo38 at yandex.ru
Mon Dec 2 17:47:12 UTC 2013


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



More information about the Haskell-Cafe mailing list