[Haskell-cafe] Type-Level Programming

[Andrew Coppin]

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.")