(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