×

Categorical models of polymorphism. (English) Zbl 0772.18007

Category theory has already been in the past one of the deepest instruments for the study of semantics of functional programming; and it seems to become more and more so in the future. It all started with the well-known correspondence between Cartesian-closed categories and lambda- calculus but it has gone much beyond that. This is particularly true of the second-order polymorphic lambda-calculus \(\lambda_ 2\), first defined in Y. Girard’s Thèse d’Etat (1976). This language has been modeled via two distinct categorical notions: that (external models) given by Seely (1987) based on CCC’s indexed over another CCC on the one hand and that (internal models) given by Moggi (1987) based on topos theory. The present paper is devoted to an “equational” approach along Moggi’s ideas.
The paper presents and discusses the relations between two classes of categorical models of the second-order (or polymorphic) lambda-calculus, namely those based on internal categories (internal models) and those based on indexed categories (external models).
Part I gives a detailed introduction to internal categories and their relations to indexed categories, via equations between arrows in an ambient category with finite limits. Part II introduces the above- mentioned two notions of a model and presents the “externalization process” that, given an internal model, yields an external one. It then shows how to go the other way round — obtaining thus equivalent models. Part III discusses three major examples of models: provable retractions inside a PER model (Berardi, 1991), PER inside \(\omega\)-Set following Longo and Moggi (1991), and PL-categories inside their Grothendieck completion (Pitts, 1987). The appendix is an involved study of the notions of internal adjunction and internal CCC.

MSC:

18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amadio, R., Recursion over realizability structures, Inform. Comput., 91, 55-85 (1991), (1991) · Zbl 0760.03012
[2] Asperti, A., (The Internal Model of Polymorphic Lambda Calculus (1988), Carnegie-Mellon University), Report CMU-CS-88-155
[3] Asperti, A.; Longo, G., (Categories, Types and Structures. An Introduction to Category Theory for the Working Computer Scientist (1991), MIT Press: MIT Press Cambridge, MA) · Zbl 0783.18001
[4] Berardi, S., Retractions on dI Domains as a Model for Type: Type, Inform. Comput., 94, 204 (1991) · Zbl 0728.68036
[5] Bruce, K.; Meyer, A.; Mitchell, J., The semantics of second order lambda calculus, Inform. Comput., 85, 76 (1989)
[6] Cardone, F., Relational semantics for recursive types and bounded quantification, (Dezani, M.; Ronchi, S., Proceedings, ICALP. Proceedings, ICALP, Lecture Notes in Computer Science, Vol. 372 (1989), Springer-Verlag: Springer-Verlag Berlin/New York), 164-178
[7] Coquand, T.; Ehrhard, T., An equational presentation of higher order logic, (Pitt; etal., Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Edinburgh. Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Edinburgh, Lecture Notes in Computer Science, Vol. 283 (1987), Springer-Verlag: Springer-Verlag Berlin/New York), 40-56
[8] Girard, J.-Y., Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieur, (Thèse de Doctorat d’Etat (1972), Université de Paris)
[9] Girard, J.-Y., The system \(F\) of variable types, fifteen years later, Theoret. Comput. Sci., 45, 159 (1986) · Zbl 0623.03013
[10] Hyland, J. M.E., A small complete category, Ann. Pure Appl. Logic, 40, 135 (1988) · Zbl 0659.18007
[11] Jacobs, B., On the semantics of second order lambda-calculus: From Bruce-Meyer-Mitchell models to hyperdoctrine models and vice-versa, (Pitt; etal., Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Manchester. Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Manchester, Lecture Notes in Computer Science, Vol. 389 (1989), Springer-Verlag: Springer-Verlag Berlin/New York), 198-212 · Zbl 1496.03061
[12] Johnstone, P. T., (Topos Theory (1977), Academic Press: Academic Press London), London Mathematical Society Monographs, No. 10 · Zbl 0368.18001
[13] Lambek, J.; Scott, P. J., (Introduction to Higher Order Categorical Logical (1986), Cambridge Univ. Press: Cambridge Univ. Press London/New York), Cambridge Studies in Advanced Mathematics, No. 7 · Zbl 0596.03002
[14] Lawvere, F. W., Equality in hyperdoctrines and comprehension schema as an adjoint functor, (Heller, A., Proceedings, New York Symposium on Application of Categorical Algebra (1970), Amer. Math. Soc: Amer. Math. Soc Providence, RI), 1-14 · Zbl 0234.18002
[15] Longo, G.; Moggi, E., Constructive natural deduction and its modest interpretation, Math. Structures Comput. Sci., 1, 215 (1991) · Zbl 0756.03028
[16] Martini, S., An interval model for second order lambda-calculus, (Pitt; etal., Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Edinburgh. Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Edinburgh, Lecture Notes in Computer Science, Vol. 283 (1987), Springer-Verlag: Springer-Verlag Berlin/New York), 219-237
[17] Meseguer, J., (Relating Models of Polymorphism (1989)), Report SRI-CSL 88-13
[18] Preliminary version in; Preliminary version in
[19] MacLane, S., (Categories for the Working Mathematician (1971), Springer-Verlag: Springer-Verlag Berlin)
[20] Moggi, E., Interpretation of second order lambda-calculus in categories (1987), unpublished manuscript
[21] Pitts, A. M., Polymorphism is set theoretic, constructively, (Pitt; etal., Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Edinburgh. Proceedings, Conference on Category Theory and Computer Science. Proceedings, Conference on Category Theory and Computer Science, Edinburgh, Lecture Notes in Computer Science, Vol. 283 (1987), Springer-Verlag: Springer-Verlag Berlin/New York), 12-39 · Zbl 0644.18003
[22] Paré, R.; Schumacher, D., Abstract families and the adjoint functor theorem, (Johnstone; Paré, Indexed Categories and Their Applications. Indexed Categories and Their Applications, Lecture Notes in Mathematics, Vol. 661 (1978), Springer-Verlag: Springer-Verlag Berlin/New York), 1-125
[23] Reynolds, J. C., Towards a theory of type structure, (Robinet, Colloque sur la programmation. Colloque sur la programmation, Lecture Notes in Computer Science, Vol. 19 (1974), Springer-Verlag: Springer-Verlag Berlin/New York), 408-425
[24] Reynolds, J. C., Polymorphism is not set theoretic, (Kahn; etal., Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1984), Springer-Verlag: Springer-Verlag Berlin/New York), 145-156 · Zbl 0554.03012
[25] Seely, R. A.G., Categorical semantics for higher order polymorphic lambda calculus, J. Symbolic Logic, 52, 969 (1987) · Zbl 0642.03007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.