This pearl is about some functions whose definitions seem to require a language with dependent types. We describe a technique for defining them in Haskell or ML, which are languages without dependent types.

Consider, for example, the scheme defining zipWith in figure 1. When this scheme is instantiated with n equal to 1 we obtain the standard function map. In practice, other instances of the scheme are often useful as well.

Figure 1 cannot be used as a definition of a function in Haskell because of the ellipses ‘...’. More importantly, the type of zipWith is parameterized by n, which seems to indicate the need for dependent types. However, as mentioned above, Haskell does not allow dependent types.