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
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/...
?
TP
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe