[Haskell-cafe] existential quantification

[Andras Slemmer]

> 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 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/20131203/d615acfc/attachment.html>