<div dir="ltr"><div><div><div><div><div><div><div><div><div><div><div><div><div><div>> But below I do not understand your reasoning.<br><br></div>Given a datatype<br><br></div>data D = D Int<br></div><br>I call Int the type you're constructing D with, however the type of the constructor itself is Int -> D<br>
</div><br>In ghc haskell there is another way of defining the same type using GADTs alongside the above "haskell98" way:<br></div><br>data D where<br></div>  D :: Int -> D<br></div><br>Notice how here we are explicitly typing the constructor.<br>
<br></div><div>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.<br><br></div><div>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.<br>
I find this ugly because it breaks the isomorphism that the = sign indicates in a haskell98 definition.<br></div><br></div><div>The GADT way on the other hand is defining ways of construction, so a definition like:<br></div>
<div>data D2 where<br></div><div>  D2 :: a -> D2<br></div><div>makes perfect sense<br><br>> Is there around a good textbook for "beginners", with full proofs, but only the essential ones?<br><br></div><div>
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.<br>
</div><div><br><br></div></div></div></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On 3 December 2013 04:10, TP <span dir="ltr"><<a href="mailto:paratribulations@free.fr" target="_blank">paratribulations@free.fr</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">Andras Slemmer wrote:<br>
<br>
> Just expanding on Brandon's answer: DeMorgan's law he's referring to goes<br>
> like this:<br>
> ∀a.P(a) === ¬∃a.¬P(a) where 'a' is a sentence, so P is second order<br>
> A special case of this is this:<br>
> ∀a.(R(a) -> Q) === ¬∃a.¬(R(a) -> Q) === ¬∃a.(R(a)∧¬Q) === ¬((∃a.R(a))∧¬Q)<br>
> === (∃a.R(a)) -> Q   (i added extra parantheses for emphasis)<br>
> So what does this mean in terms of haskell? R(a) is your data definition's<br>
> "body", and Q is the type you are defining. On the lhs the universally<br>
> quantified version gives you the type of the constuctor you're defining,<br>
> and on the rhs the existential tells you what you're constructing the type<br>
> with.<br>
> Or in other words the universal version says: For any 'a' give me an R(a)<br>
> and i'll give you back a Q.<br>
> The existential version says: If you have some 'a' for which R(a) i'll<br>
> give you back a Q. (It's hard to phrase the difference without sounding<br>
> stupid, they are equivalent after all).<br>
><br>
> There are of course other considerations, for example introducing 'exists'<br>
> would mean another keyword in the syntax.<br>
<br>
</div>Thanks Andras, I have understood the developments up to that point. But<br>
below I do not understand your reasoning.<br>
<div class="im"><br>
><br>
> Having said that I think that the choice of 'forall' for<br>
> -XExistentialQuantification is wrong, as the data body defines the type<br>
> you're constructing with, not the type of the whole constructor. HOWEVER<br>
> for -XGADTs forall makes perfect sense. Compare the following:<br>
><br>
> data AnyType = forall a. AnyType a<br>
> data AnyType where<br>
>   AnyType :: forall a. a -> AnyType<br>
><br>
> These two definitions are operationally identical, but I think the GADT<br>
> way is the one that actually corresponds to the DeMorgan law.<br>
<br>
</div>And one more question: I had lectures on logic some years ago, but I never<br>
studied type theory at university (I'm some sort of "electrical engineer").<br>
Is there around a good textbook for "beginners", with full proofs, but only<br>
the essential ones? I would like a good "entry point" in the textbook<br>
literature. Not for experts.<br>
Are the books of Robert Harper suitable, for example<br>
<br>
<a href="http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570" target="_blank">http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570</a><br>
<div class="HOEnZb"><div class="h5"><br>
?<br>
<br>
TP<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>