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
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