Polytypic values possess polykinded types

A polytypic value is one that is defined by induction on the structure of types. In Haskell types are assigned so-called kinds that distinguish between manifest types like the type of integers and functions on types like the list type constructor. Previous approaches to polytypic programming were restricted in that they only allowed to parameterize values by types of one fixed kind. In this paper, we show how to define values that are indexed by types of arbitrary kinds. It turns out that these polytypic values possess types that are indexed by kinds. We present several examples that demonstrate that the additional flexibility is useful in practice. One paradigmatic example is the mapping function, which describes the functorial action on arrows. A single polytypic definition yields mapping functions for data types of arbitrary kinds including first- and higher-order functors. Haskellʹs type system essentially corresponds to the simply typed lambda calculus with kinds playing the role of types. We show that the specialization of a polytypic value to concrete instances of data types can be phrased as an interpretation of the simply typed lambda calculus. This allows us to employ logical relations to prove properties of polytypic values. Among other things, we show that the polytypic mapping function satisfies suitable generalizations of the functorial laws.