wren ng thornton wrote:
Andrew Coppin wrote:
I think I looked at Coq (or was it Epigram?) and found it utterly
incomprehensible. Whoever wrote the document I was reading was
obviously very comfortable with advanced mathematical abstractions
which I've never even heard of.
One of the things I've found when dealing with--- er, reading the
documentation for languages like Coq, is that the class of problems
which motivate the need to move to such powerful formalisms are often
so abstract that it is hard to come up with simple practical examples
of why anyone should care. There are examples everywhere, but complex
machinery is only motivated by complex problems, so it's hard to find
nice simple examples.
Yeah. I think a similar problem is probably why most of the existing GHC
extensions don't have comprehendable documentation. It's like "if you
don't understand why this is useful, you probably don't even need it
anyway". Except that that still doesn't explain the opaque language.
(Other than that saying "this lets you put a thingy on the wotsit
holder" would be even *more* opaque...)
It's a bit like trying to learn Prolog from somebody who thinks that
the difference between first-order and second-order logic is somehow
"common knowledge". (FWIW, I have absolutely no clue what that
difference is.
First-order means you can only quantify over simple things.
Second-order means you can also quantify over quantification, as it were.
Sure. I get the idea that "second-order" means "like first-order, but
you can apply it to itself" (in most contexts, anyway). But what the
heck does "quantification" mean?
Sadly, I suspect that it would be like asking where Maidenhead is.
("Hey, where *is* Maidenhead anyway?" "Oh, it's near Slough." "Uh,
where's Slough?" "It's in Berkshire." "...and where's Berkshire?" "It's
near Surrey." "OK, forget I asked.")
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
