Lambda the Ultimate

Do we Need Dependent Types?
started 8/21/2002; 2:54:10 AM - last post 8/22/2002; 4:06:25 AM

Ehud Lamm - Do we Need Dependent Types?

8/21/2002; 2:54:10 AM (reads: 1504, responses: 1)

Do we Need Dependent Types?

(via the Haskell mailing list)

Daniel Fridlender, Mia Indrika. Do we Need Dependent Types? Appears in Journal of Functional Programming, 10(4):409-415,2000.

Inspired by Danvy, we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in LC.

Simple yet cool solution.

Posted to theory by Ehud Lamm on 8/21/02; 2:54:52 AM

Ehud Lamm - Re: Do we Need Dependent Types?

8/22/2002; 4:06:25 AM (reads: 527, responses: 0)

This is another example of the law of unintended consequences in programming language design. Language features are more powerful and subtle than you think...