[Haskell-cafe] Type-Level Programming
andrewcoppin at btinternet.com
Mon Jun 28 15:18:28 EDT 2010
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.")
More information about the Haskell-Cafe