[Haskell-cafe] Type-Level Programming
andrewcoppin at btinternet.com
Sat Jun 26 07:33:14 EDT 2010
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.)
More information about the Haskell-Cafe