×

Functorial polymorphism. (English) Zbl 0717.18005

The authors study two semantic approximations to Strachey’s parametric polymorphism. The first one insists on certain naturality conditions on indexed families of functions and therefore interprets universal type abstraction as only a part of the product over all types. Types are approximated by functors and terms by natural transformations between types, all defined over some cartesian closed category of “ground” types. The second approximation is based on a version of Reynold’s invariance condition.
Reviewer: V.Kurkova-Pohlova

MSC:

18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Forsythe; Nuprl; Miranda
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bainbridge, E. S.; Freyd, P. J.; Scedrov, A.; Scott, P. J., Functorial polymorphism, (Huet, G., Logical Foundations of Functional Programming, Proceedings (1987), University of Texas Programming Institute: University of Texas Programming Institute Austin, TX), (Preliminary Report) · Zbl 0717.18005
[2] Barendregt, H. P., The Lambda Calculus, (Studies in Logic and the Foundations of Mathematics (1984), North-Holland: North-Holland Amsterdam) · Zbl 0467.03010
[3] Barnes, J. G.P., Programming in Ada (1981), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0485.68008
[4] Böhm, C.; Berarducci, A., Automatic synthesis of typed \(A\)-programs on term algebras, Theoret. Comput. Sci., 39, 135-154 (1985) · Zbl 0597.68017
[5] Breazu-Tannen, V.; Coquand, T., Extensional models for polymorphism, Theoret. Comput. Sci., 59, 1, 2, 85-114 (1988) · Zbl 0713.03005
[6] Bruce, K. B.; Longo, G., A modest model of records, inheritance, and bounded quantification, (Proc. 3rd IEEE Symp. on Logic in Computer Science. Proc. 3rd IEEE Symp. on Logic in Computer Science, Edinburgh, Scotland (1988)), 38-50
[7] K.B. Bruce, A.R. Meyer and J.C. Mitchell, The semantics of second-order lambda calculus, Inform. and Comput.; K.B. Bruce, A.R. Meyer and J.C. Mitchell, The semantics of second-order lambda calculus, Inform. and Comput. · Zbl 0714.68052
[8] Carboni, A.; Freyd, P.; Scedrov, A., A categorical approach to realizability and polymorphic types, (Main, M., Proc. 3rd ACM Workshop on the Mathematical Foundations of the Programming Semantics, New Orleans, April, 1987. Proc. 3rd ACM Workshop on the Mathematical Foundations of the Programming Semantics, New Orleans, April, 1987, Lectures Notes in Computer Science, 298 (1988), Springer: Springer Berlin), 23-42
[9] Cardelli, L., Time for a new language (April 1988), Preprint
[10] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, Comput. Surveys, 17, 471-522 (1985)
[11] Constable, R., Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice Hall: Prentice Hall Englewood Cliffs, NJ
[12] Coquand, T.; Huet, G., Constructions: a higher-order proof system for mechanizing mathematics, (Proc: EUROCAL ’85. Proc: EUROCAL ’85, Lecture Notes in Computer Science, 203 (1985), Speinger: Speinger Berlin), 151-184 · Zbl 0581.03007
[13] Coquand, T.; Gunter, C. A.; Winskel, G., Di-domains as a model of polymorphism, (Main, M., Proc. 3rd ACM Workshop on the Mathematical Foundations of the Programming Language Semantics, New Orleans, April 1987. Proc. 3rd ACM Workshop on the Mathematical Foundations of the Programming Language Semantics, New Orleans, April 1987, Lecture Notes in Computer Science, 298 (1988), Springer: Springer Berlin), 344-363
[14] T. Coquand, C.A. Gunter and G. Winskel, Domain theoretical models for polymorphism, Inform. and Comput.; T. Coquand, C.A. Gunter and G. Winskel, Domain theoretical models for polymorphism, Inform. and Comput. · Zbl 0683.03007
[15] Cousineau, G., CAML, Lectures at the University of Texas Programming Institute on the Logical Foundations of Functional Programming (June 1987), Austin, TX
[16] Dubuc, E. J.; Street, R., Dinatural transformations, (Reports of the Midwest Category Seminar IV. Reports of the Midwest Category Seminar IV, Lecture Notes in Mathematics, 137 (1970), Springer: Springer Berlin), 126-128 · Zbl 0222.18004
[17] Eilenberg, S.; Kelly, G. M., A generalization of the functorial calculus, J. Algebra, 3, 366-375 (1966) · Zbl 0146.02501
[18] Freyd, P. J., Structural polymorphism I, II, III (January 1989), University of Pennsylvannia, (Preliminary Report)
[19] Freyd, P. J.; Girard, J. Y.; Scedrov, A.; Scott, P. J., Semantic parametricity in polymorphic lambda calculus, (Proc.v 3rd IEEE Symp. on Logic in Computer Science (1988), Scotland: Scotland Edinbergh)
[20] Girard, J. Y., Une extension de l’interprétation de Gödel, (Fenstad, J. E., Second Scandinavian Logic Symposium, 1970 (1971), North-Holland: North-Holland Amsterdam), 63-92
[21] Girard, J. Y., Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, (Thèse de Doctorat d’Etat (1972), Université de Paris VIII)
[22] Girard, J. Y., The system \(F\) of variables types, fifteen years later, Theoret. Comput. Sci., 45, 159-192 (1986) · Zbl 0623.03013
[23] Gordon, M. J.C.; Milner, R.; Wadsworth, C., Edinburgh LCF, (Lecture Notes in Computer Science, 78 (1979), Springer: Springer Berlin) · Zbl 0421.68039
[24] Huet, G., Deduction and computation, (Bibel, W.; Jorrand, P., Lecture Notes in Computer Science (1986), Springer: Springer Berlin), Fundamentals of Artificial Intelligence · Zbl 0634.68018
[25] Huet, G., A uniform approach to type theory, Logical Foundations of Functional Programming, Proceedings University of Texas Programming Institute (1987), Austin, TX
[26] Huet, G., Logical Foundations of Functional Programming, Proceedings University of Texas Programming Institute (1987), Austin, TX
[27] Hyland, J. M.E., The effective topos, (Troelstra, A. S.; van Dalen, D., The L.E.J. Brouwer Centenary (1982), North-Holland: North-Holland Amsterdam) · Zbl 0522.03055
[28] Hyland, J. M.E., A small complete category, Ann. Pure Appl. Logic, 40, 135-165 (1988) · Zbl 0659.18007
[29] Hyland, J. M.E.; Robinson, E. P.; Rosolini, G., The discrete objects in the effective topos (1987), Preprint. · Zbl 0703.18002
[30] Hyland, J. M.E.; Robinson, E. P.; Rosolini, G., Algebraic types in PER models, (Technical Report 88-234 (1988), Queen’s University Dept. of Computing: Queen’s University Dept. of Computing Kingston, Ont) · Zbl 0703.18002
[31] Kelly, M., Many-variable function calculus I, (MacLane, S., Coherence in Categories. Coherence in Categories, Lecture Notes in Mathematics, 281 (1977), Springer: Springer Berlin), 66-105
[32] Kleene, S. C., Introduction to Metamathematics (1952), Van Nostrand: Van Nostrand New York · Zbl 0047.00703
[33] Lambek, J.; Scott, P. J., Introduction to Higher-Order Categorical Logic, (Studies in Advanced Mathematics, 7 (1986), Cambridge University Press: Cambridge University Press Cambridge) · Zbl 0596.03002
[34] Landin, P. J., The next 700 programming languages, Comm. ACM, 9, 157-166 (1964) · Zbl 0149.12505
[35] Liskov, B., Clu Reference Manual, (Lecture Notes in Computer Science, 114 (1981), Springer: Springer Berlin) · Zbl 0463.68009
[36] Longo, G.; Moggi, E., Constructive natural deduction and its “modest” interpretation, (Meseguer, J., Workshop on Semantics of Natural and Computer Languages (March 1987), MIT Press: MIT Press Cambridge, MA), to appear. · Zbl 0756.03028
[37] MacLane, S., Categories for the Working Mathematician, (Graduate Texts in Mathematics, 5 (1971), Springer: Springer Berlin) · Zbl 0705.18001
[38] Martin-Löf, P., Constructive mathematics and computer programming, (Sixth Internat. Congress of Logic, Methodology and Philosophy of Science (1982), North-Holland: North-Holland Amsterdam), 153-175 · Zbl 0552.03040
[39] Meseguer, J., Relating models of polymorphism (1988), SRI International: SRI International Menlo Park, CA, U.S.A, Preprint
[40] Milner, R., A proposal for standard ML, Proc. ACM Symp. on LISP and Functional Programming, 184-197 (1984)
[41] Mitchell, J. C., A type-inference approach to reduction properties and semantics of polymorphic expressions, Proc. 1986 ACM Symp. on Lisp and Functional Programming, 308-319 (1986)
[42] Mitchell, J. C.; Harper, R., The essence of ML, Proc. 15th ACM Symp. on Principles of Programming Languages, 28-46 (1988)
[43] Mitchell, J. C.; Meyer, A. R., Second-order logical relations, (Parikh, R., Lecture Notes in Computer Science, 193 (1985), Springer: Springer Berlin), 225-236
[44] Pitts, A., Polymorphism is set-theoretic, constructively, (Proc. Symp. on Category Theory and Computer Science. Proc. Symp. on Category Theory and Computer Science, Lecture Notes in Computer Science, 283 (1987), Springer: Springer Berlin) · Zbl 0644.18003
[45] Plotkin, G. D., LCF considered as a programming language, Theoret. Comput. Sci., 5, 223-256 (1977) · Zbl 0369.68006
[46] Reynolds, J. C., Towards a theory of type structure, (Lecture Notes in Computer Science, 19 (1974), Springer: Springer Berlin), 408-425
[47] Reynolds, J. C., The essence of Algol., (de Bakker, J.; van Vliet, J. C., Algorithmic Languages (1981), North-Holland: North-Holland Amsterdam), 345-372, IFIP
[48] Reynolds, J. C., Types, abstraction, and parametric polymorphism, (Mason, R. E.A., Information Processing ’83 (1983), North-Holland: North-Holland Amsterdam), 513-523
[49] Reynolds, J. C., Polymorphism is not set-theoretic, (Kahn, Symp. on Semantics of Data Types. Symp. on Semantics of Data Types, Lecture Notes in Computer Science, 173 (1984), Springer: Springer Berlin) · Zbl 0554.03012
[50] Reynolds, J. C., Preliminary design of the programming language Forsythe, (Research Report (June, 1988), Carnegie-Mellon University)
[51] J.C. Reynolds and G.D. Plotkin, On functors expressible in the polymorphic typed lambda calculus, Inform. and Comput.; J.C. Reynolds and G.D. Plotkin, On functors expressible in the polymorphic typed lambda calculus, Inform. and Comput. · Zbl 0785.03004
[52] Robinson, E. P., How complete is PER?, (Technical Report 88-229 (1988), Dept. of Computing & Information Science, Queen’s University: Dept. of Computing & Information Science, Queen’s University Kingston, Ont., Canada) · Zbl 0717.03028
[53] A. Scedrov, A guide to polymorphic types, in: P. Odifreddi, ed., Logic and Computer Science, Proc. C.I.M.E. Summer School, Montecatini Terme (June 1988); A. Scedrov, A guide to polymorphic types, in: P. Odifreddi, ed., Logic and Computer Science, Proc. C.I.M.E. Summer School, Montecatini Terme (June 1988) · Zbl 0706.03015
[54] Scott, D. S., Continuous lattices, (Lawvere, F. W., Toposes, Algebraic Geometry and Logic. Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, 274 (1972), Springer: Springer Berlin), 97-136
[55] Scott, D. S., Data types as lattices, SIAM J. Comput., 5, 522-587 (1976) · Zbl 0337.02018
[56] Scott, D. S., Domains for denotational semantics, (Proc. ICALP ’82. Proc. ICALP ’82, Lecture Notes in Computer Science, 140 (1982), Springer: Springer Berlin) · Zbl 0495.68025
[57] Scott, D. S., Lecture at the Amer. Math. Soc. Research Conference on Categories in Computer Science and Logic, Boulder, Colorado. Lecture at the Amer. Math. Soc. Research Conference on Categories in Computer Science and Logic, Boulder, Colorado, Realizability and domain theory (June 1987)
[58] Seely, R. A.G., Categorical semantics for higher-order polymorphic lambda calculus, J. Symbolic Logic, 52, 969-989 (1987) · Zbl 0642.03007
[59] Smyth, M. B.; Plotkin, G. D., The category-theoretic solution of recursive domain equations, SIAM J. Comput., 11, 761-783 (1982) · Zbl 0493.68022
[60] Strachey, C., Fundamental concepts in programming languages, (Lecture Notes (August 1967), International Summer School in Computer Programming: International Summer School in Computer Programming Copenhagen) · Zbl 0949.68510
[61] (Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, 344 (1973), Springer: Springer Berlin) · Zbl 0275.02025
[62] Turner, D. A., Miranda: a non-strict functional language with polymorphic types, (Jovannaud, J. P., Functional Programming Languages and Computer Architecture. Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, 201 (1985), Springer: Springer Berlin) · Zbl 0592.68014
[63] Yoneda, N., On Ext and exact sequences, J. Fac. Sci. Tokyo Sec 1, 8, 507-526 (1960) · Zbl 0163.26902
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.