Jason Dagit wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
<andrewcop...@btinternet.com <mailto:andrewcop...@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.)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
