On Functors Expressible in the Polymorphic Typed Lambda Calculus
Date
1991Author
Plotkin, Gordon
Reynolds, John
Metadata
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. These results are used to establish the impossibility
of certain models, including those in which types denote sets and S ! S0 denotes the
set of all functions from S to S0.