Do we need dependent types?

Abstract

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.