[Haskell-cafe] existential quantification

[TP]

Andras Slemmer wrote:

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

Thanks Andras, I have understood the developments up to that point. But 
below I do not understand your reasoning.

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

And one more question: I had lectures on logic some years ago, but I never 
studied type theory at university (I'm some sort of "electrical engineer"). 
Is there around a good textbook for "beginners", with full proofs, but only 
the essential ones? I would like a good "entry point" in the textbook 
literature. Not for experts.
Are the books of Robert Harper suitable, for example

http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

?

TP