On functors expressible in the polymorphic typed lambda calculus

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 ↔ S’ denotes the set of all functions from S to S’. © 1993 Academic Press, Inc.