> But below I do not understand your reasoning.

Given a datatype

data D = D Int

I call Int the type you're constructing D with, however the type of the constructor itself is Int -> D

In ghc haskell there is another way of defining the same type using GADTs alongside the above "haskell98" way:

data D where
  D :: Int -> D

Notice how here we are explicitly typing the constructor.

The haskell98 way defines what your datatype D is isomorphic to - here it is Int, whereas the GADT way defines how to construct a D.

The problem haskell developers faced was that in order to use the haskell98 way for existentials they would've had to introduce an 'exists' quantifier, which would mess up a boatload of things in the type theory. Instead they introduced this forall hack that doesn't define an isomorphic type, rather it indicates that we are defining a way of constructing an existential.
I find this ugly because it breaks the isomorphism that the = sign indicates in a haskell98 definition.

The GADT way on the other hand is defining ways of construction, so a definition like:
data D2 where
  D2 :: a -> D2
makes perfect sense

> Is there around a good textbook for "beginners", with full proofs, but only the essential ones?

Types and Programming Languages from Benjamin Pierce is a good one. I also plan to upload a short video lecture series from Harper on type theory (it assumes minimal knowledge of logic), i'll send you a link when it's up.




On 3 December 2013 04:10, TP <paratribulations@free.fr> wrote:
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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe