Just expanding on Brandon's answer: DeMorgan's law he's referring to goes like this: ∀a.P(a) === ¬∃a.¬P(a) where 'a' is a sentence, so P is second order A special case of this is this: ∀a.(R(a) -> Q) === ¬∃a.¬(R(a) -> Q) === ¬∃a.(R(a)∧¬Q) === ¬((∃a.R(a))∧¬Q) === (∃a.R(a)) -> Q (i added extra parantheses for emphasis) So what does this mean in terms of haskell? R(a) is your data definition's "body", and Q is the type you are defining. On the lhs the universally quantified version gives you the type of the constuctor you're defining, and on the rhs the existential tells you what you're constructing the type with. Or in other words the universal version says: For any 'a' give me an R(a) and i'll give you back a Q. The existential version says: If you have some 'a' for which R(a) i'll give you back a Q. (It's hard to phrase the difference without sounding stupid, they are equivalent after all). There are of course other considerations, for example introducing 'exists' would mean another keyword in the syntax. Having said that I think that the choice of 'forall' for -XExistentialQuantification is wrong, as the data body defines the type you're constructing with, not the type of the whole constructor. HOWEVER for -XGADTs forall makes perfect sense. Compare the following: data AnyType = forall a. AnyType a data AnyType where AnyType :: forall a. a -> AnyType These two definitions are operationally identical, but I think the GADT way is the one that actually corresponds to the DeMorgan law. On 2 December 2013 22:07, TP 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-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

On 12/02/2013 11:07 PM, TP wrote:

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

This still says that 'test' is a value of type 's' for all 's' with a 'Show' instance. Basically, 'test' gets a type 's', an instance 'Show s' and we get a value of type 's'.

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.

Generally speaking, a typing judgement x :: A can be interpreted as a proof that type 'A' is inhabited, or in other words, there exists a value of type 'A'. (Of course in Haskell this fact alone is trivial due to 'undefined', but additional reasoning could render it meaningful. For the remainder I'll just ignore the issue of lifting.) This is somewhat related to classical existential quantification, but it is stronger in a sense, since it says that we know how to construct such a value. (The classical version in general just says that the assumption that there is no such value leads to a contradiction.) Pattern matching allows one to get back the original constructor and the arguments used to construct a value of some ADT type. A universal quantifier over a type states that we can provide any type and obtain a value of the type provided in the body where all instances of the bound variable are replaced by our type. I.e. you can interpret forall a. (...) as stating that a value of that type takes an additional implicit argument 'a' at type level. Now MkFoo is declared as follows: data Foo = forall a. MkFoo a (a -> Bool) | Nil Which gives it the type: MkFoo :: forall a. a -> (a -> Bool) -> Foo I.e. it gets a type 'a' a value of that type and a decidable predicate ranging over that type and constructs a value of type 'Foo'. Pattern matching (roughly speaking) does the opposite: It gets you back a type, a value of that type and the predicate. The type is called nearly isomorphic to the explicit existential type, because using some rounds of pattern matching one would also recover the same kinds of objects. I.e. existential quantification can be thought of as being left implicit in the typing judgement, but 'forall' is needed in order to make explicit the scope of the type variable, which otherwise would range over the entire data declaration instead of just a single constructor. -XExistentialQuantification enables uses of 'forall' necessary for using existential quantification.