[Haskell-cafe] Type-Level Programming

[Andrew Coppin]

Jason Dagit wrote:
>
> On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin 
> <andrewcoppin at btinternet.com <mailto:andrewcoppin at btinternet.com>> wrote:
>
>     Out of curiosity, what the hell does "dependently typed" mean anyway?
>
>
> The types can depend on values.  For example, have you ever notice we 
> have families of functions in Haskell like zip, zip3, zip4, ..., and 
> liftM, liftM2, ...?
>
> Each of them has a type that fits into a pattern, mainly the arity 
> increases.  Now imagine if you could pass a natural number to them and 
> have the type change based on that instead of making new versions and 
> incrementing the name.

Right. I see. (I think...)

> Then there are languages like Coq and Agda that support dependent 
> types directly.  There you can return a type from a function instead 
> of a value.

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. 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. But if you show me a few 
Prolog examples, I get the gist of what it does and why that's useful.)