Inspired by Functional Unparsing (Danvy 1998), we describe a technique for dening, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general denition of zipWith for which the Haskell library provides a family of functions, each member of the family having a dierent type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in λ-calculus.
Lire maintenant ?