• People
• Events
• Research

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. 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.