Dinaturality for free

Summary

The first aim of this paper is to attack a problem posed in [1] about uniform families of maps between realizable functors on PER's.

To put this into context, suppose that we are given a category C to serve as our category of types. The authors of [1] observe that the types representable in the second-order lambda; calculus and most extensions thereof can be regarded as being obtained from functors (C^op × C)ⁿ → C by diagonalisation of corresponding contra and covariant arguments. Terms in the calculus give rise to dinatural transformations. This suggests a general structure in which parametrised types are interpreted by arbitrary functors (C^op × C)ⁿ → C, and their elements by dinatural transformations. Unfortunately as the authors of the original paper point out, this interpretation can not be carried out in general since dinaturals do not necessarily compose.

However, suppose we are in the extraordinary position that all families of maps which are of the correct form to be a dinatural transformation between functors (C^op × C)ⁿ → C are in fact dinatural, a situation in which we have, so to speak, the dinaturality for free. In this situation dinaturals compose. The result is a structure for a system in which types can be parametrised by types (second-order lambda calculus without the polymorphic types). Suppose, in addition, the category in question is complete, then we can perform the necessary quantification (which is in fact a simple product), and obtain a model for the second-order lambda calculus.