<div dir="ltr"><div>I uploaded the Harper video series, here is a link to the first lecture: <a href="https://www.youtube.com/watch?v=ev7AYsLljxk&list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf&index=5">https://www.youtube.com/watch?v=ev7AYsLljxk&list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf&index=5</a><br>
</div>This is more of an introduction to dependent type theory, but it's worth a watch!<br></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>