Abstract
The polymorphic, or second-order, typed lambda calculus is an extension of the typed lambda calculus in which polymorphic functions can be defined. In this paper, we will prove that the standard set-theoretic model of the ordinary typed lambda calculus cannot be extended to model this language extension.
Work supported by National Science Foundation Grant MCS-8017577.
Preview
Unable to display preview. Download preview PDF.
References
Reynolds, J. C., Towards a Theory of Type Structure, Proc. Colloque sur la Programmation, Lecture Notes in Computer Science 19, Springer-Verlag, New York, 1974, pp. 408–425.
Girard, J.-Y., Interprétation Fonctionelle et Elimination des Coupures dans l'Arithmétique d'Ordre Supérieur, Thèse de Doctorat d'Etat, Paris, 1972.
Reynolds, J. C., Types, Abstraction and Parametric Polymorphism, Information Processing 83, R. E. A. Mason (ed.), Elsevier Science Publishers B.V. (North-Holland) 1983, pp. 513–523.
Strachey, C., Fundamental Concepts in Programming Languages, Lecture Notes, International Summer School in Computer Programming, Copenhagen, August 1967.
Lehmann, D., and Smyth, M. B., Algebraic Specification of Data Types: A Synthetic Approach, Math. Systems Theory 14 (1981), pp. 97–139.
Smyth, M. B., and Plotkin, G. D., The Category-Theoretic Solution of Recursive Domain Equations, SIAM Journal on Computing 11, 4 (November 1982), pp. 761–783.
Arbib, M. A., and Manes, E. G., Arrows, Structures, and Functors: The Categorical Imperative, Academic Press, New York, 1975, p. 95.
McCracken, N. J., An Investigation of a Programming Language with a Polymorphic Type Structure, Ph. D. dissertation, Syracuse University, June 1979.
McCracken, N. J., A Finitary Retract Model for the Polymorphic Lambda-Calculus, to appear in Information and Control.
Fortune, S., Leivant, D., and O'Donnell, M., The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM 30, 1 (January 1983), pp. 151–185.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reynolds, J.C. (1984). Polymorphism is not set-theoretic. In: Kahn, G., MacQueen, D.B., Plotkin, G. (eds) Semantics of Data Types. SDT 1984. Lecture Notes in Computer Science, vol 173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-13346-1_7
Download citation
DOI: https://doi.org/10.1007/3-540-13346-1_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-13346-9
Online ISBN: 978-3-540-38891-3
eBook Packages: Springer Book Archive