Polytypic Programming With Ease

This article proposes a new framework for a polytypic extension of functional programming languages. A polytypic functional program is one that is parameterised by datatype. Since polytypic functions are defined by induction on types rather than by induction on values, they typically operate on a higher level of abstraction than their monotypic counterparts. However, polytypic programming is not necessarily more complicated than conventional programming. In fact, a polytypic function is uniquely defined by its action on projection functors and on primitive functors such as sums and products. This information is sufficient to specialize a polytypic function to arbitrary datatypes, including mutually recursive datatypes and nested datatypes. The key idea is to use infinite trees as index sets for polytypic functions and to interpret datatypes as algebraic trees. This approach is simpler, more general, and more efficient than previous ones that are based on the initial algebra semantics of datatypes. Polytypic functions enjoy polytypic properties. We show among other things that well-known properties of various functions are obtained as direct consequences of two polytypic fusion laws