## On Functors Expressible in the Polymorphic Typed Lambda
Calculus

**J.C. Reynolds and G.D. Plotkin**
*Abstract:* Given a model of the polymorphic typed lambda
calculus based upon a Cartesian closed category *K*, there
will be functors from *K* to *K* whose action on objects
can be expressed by type expressions and whose action on morphisms
can be expressed by ordinary expressions. We show that if *T*
is such a functor then there is a weak initial *T*-algebra and
if, in addition, *K* possesses equalizers of all subsets of
its morphism sets, then there is an initial *T*-algebra. It
follows that there is no model of the polymorphic typed lambda
calculus in which types denote sets and *S* -> *S'*
denotes the set of all functions from *S* to *S'*.

*LFCS report ECS-LFCS-88-53*

This report was published in *Information and Computation*,
**105**(1), pp.1-29, July 1993.

Previous |

Index |

Next