[Haskell-cafe] existential quantification

[Andras Slemmer]

I uploaded the Harper video series, here is a link to the first lecture:
https://www.youtube.com/watch?v=ev7AYsLljxk&list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf&index=5
This is more of an introduction to dependent type theory, but it's worth a
watch!


On 3 December 2013 04:10, TP <paratribulations at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131208/01388f6d/attachment.html>