[Haskell-cafe] existential quantification
0slemi0 at gmail.com
Tue Dec 3 00:47:25 UTC 2013
> 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
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
> > "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
> > 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
> > 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
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe