On Functors Expressible in the Polymorphic Typed Lambda Calculus
dc.contributor.author
Plotkin, Gordon
en
dc.contributor.author
Reynolds, John
en
dc.date.accessioned
2003-11-05T12:59:58Z
dc.date.available
2003-11-05T12:59:58Z
dc.date.issued
1991
dc.description.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.
en
dc.format.extent
244789 bytes
en
dc.format.mimetype
application/pdf
en
dc.identifier.uri
http://hdl.handle.net/1842/200
dc.language.iso
en
dc.publisher
Information and Computation
en
dc.subject
Laboratory for Foundations of Computer Science
en
dc.title
On Functors Expressible in the Polymorphic Typed Lambda Calculus
en
dc.type
Preprint
en
Files
Original bundle
1 - 1 of 1
- Name:
- Functors_Expressible_Polymorphic.pdf
- Size:
- 239.05 KB
- Format:
- Adobe Portable Document Format
This item appears in the following Collection(s)