Relating models of polymorphism

ABSTRACT

A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and initiality theorems, and can be used to unify and relate many different notions of model that have been proposed in the literature, including those that extend the basic calculus with additional features such as fixpoints or a type of all types. Moreover, the polymorphic lambda calculus and Martin-Löf type theory are related by a map of logics. A categorical and initial model semantics is given for the basic calculus and for richer calculi that extend the basic one with fixpoints or with a type of all types.

REFERENCES

• 1: R. Amadio, K.B. Bruce, and G. Longo. The finitary projection model for se, cond order lambda calculus and solutions to higher order domain equations. In Proc. L{CS'86, pages 122-130, IEEE, 1986.
• 2: A. Asperti and G. Longo. Categories for denotational semantics. To appear.
• 3: E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J Scott. Functorial polymorphism. In G. Huet, editor, Logical Foundations of Functional Programming, Addison- Wesley, 1988. To appear.
• 4: Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
• 5: K. Bruce, A. Meyer, and J. Mitchell. The Semantics of Second-Order Lambda Calculus. Technical Report to appear, Lab. Computer Sci., MIT, 1985.
• 6: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• 7: Rod M. Burstall , Joseph A. Goguen, The Semantics of CLEAR, A Specification Language, Proceedings of the Abstract Software Specifications, 1979 Copenhagen Winter School, p.292-332, January 22-February 02, 1979
• 8: L. Cardelli. A polymorphic X-caluculu,~: with Type:Type. Technical Report, SEC System Research Center, PMo Alto, Ca, 1985.
• 9: J. Cartmell. Genera/ised algebraic theories and contextual categories. Annals Pure Appl. Logic, 32:209- 243, 1986.
• 10: T. Coquand, C. Gunter, and G. Winskel. Di-Domains as a Model of Polymorphism. Technical Report 107, Computer Laboratory, Univ. of Cambridge, 1987.
• 11: T. Coquand, C. Gunter, and G. Winskel. Domain Theoretic Models of Polymorphism. Technical Report 116, Computer Laboratory, Univ. of Cambridge, 1987.
• 12: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 13: P. Freyd. Aspects of topoi. Bull. Austral. Math. Soc., 7:1-76, 1972.
• 14: P.J. Freyd, J.-Y. Girard, A. Scedrov, and P.J. Scott. Semantic parametric:try in polymorphic lambdi~, calculus. In Proc. L1CS'8;?, pages 274-279, IEEE, 1988.
• 15: Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318610]
• 16: J.Y. Girard. Interprgtation Fonetionelle et Elimirtation des Coupures dons l'Arithmdtique d'ordre Sup~rieure. PhD thesis, Univ. Paris VII, 1972.
• 17: Jean-Yves Girard, The system F of variable types, fifteen years later, Theoretical Computer Science, v.45 n.2, p.159-192, Sept. 1986
• 18: Joseph Goguen. Higher-order functions considered unnecessary for higher-order programming. In David Turner, editor, Proc., University of Texas Year of Programming, institute on Declarative Programming, Addison-Wesley~ 1988. To appear; preliminary version as SRI Tech. Rep. SRI-CSL-88-1, January 1988.
• 19: Joseph Goguen and Rod Burstall. Institutions: Abstract Model Theory/or Computer Science. Technical Report CSLI-85-30, Center for the Study of Language and Information, Stanford University, 1985. Also submitted for publication.
• 20: Joseph Goguen and Jos6 Meseguer. Eqlog: equality, types, and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295-363, Prentice-Hall, 1986. An earlier version appears in Journal of Logic Programming, Volume 1, Number 2, pages 179-210, September 1984.
• 21: J. A. Goguen , J. Meseguer, Models and equality for logical programming, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.1-22, March 1987, Pisa, Italy
• 22: A. Grotheadieck and J.L. Verdier. Pr~fascieaux. In J.L. Verdier M. Artin, A Grothendieck, editor, Th~orie de Topos et Cohomologie Etale des Schdmas, SGA$, Springer Lecture Notes in Mathematics No. 269, 1972.
• 23: L. Henkin. Completeness in the theory of types. J. Symbolic Logic, 15:81-91, 1950.
• 24: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• 25: H. Huwig and A. Poign4. A note on inconsistencies caused by fixpoints in a cartesian closed category. Manuscript, C.S. Dept., Univ. of Dortmund.
• 26: J.M.E. Hyland. The effective topos, in A.S. Toelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165-216, North-Hollartd, 1982.
• 27: J.M.E. Hyland. A small complete category. In Proc. Conf. or~ Church's Thesis: Fi.ity Years Later, 1987.
• 28: J.M.E. Hyland and A. Pitts. The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models. American Mathematical Society, 1987.
• 29: Peter Johnstone. Topos Theory. Academic Press, 1977.
• 30: A. Kock. Bitinearity and cartesian closed monads. Math. Seand., 29:161-174, 1971.
• 31: Francis William Lawvere. Quantifiets and sheaves. In Acres Congr~s Intl. Math. (Nice 1970), vol. 1, pages 329-334, Gauthier-Villars, 1971.
• 32: F.W. Lawvere. Skolem categories. Unpublished Seminar Lectures at University of Buffalo. Fall of 1974.
• 33: G. Longo and E. Moggi. Constructive natural deduction and its "modest" interpretation. In M. Gawron, D. Israel, J. Meseguer, and S. Peters, editors, Semantics of Natural and Computer Languages, MIT Press, 1988. To appear.
• 34: Saunders MacLane. Categories for the working mathematieian. Springer, 1971.
• 35: P. Martin-LSf. An Intuitionistic Theory of Types" Predicative Part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloq. '73, Noth-Holland, 1973.
• 36: P. Martin-LSf. Intuitionistic Type Theory. Bibliopolis, 1984.
• 37: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 38: J. Meseguer. Order completion monads. Algebra Universalis, 16:63-82, 1983.
• 39: J. Meseguer. Universe models and initial model semantics for the second order polymorphic lambda calculus. Abstracts of the AMS, August:338, 1988. Also appeared as a communication in the Types electronic forum ([e-mail]), April 13 1988.
• 40: J. Meseguer. What is logic programming? what is a logic? In M. Garrido, editor, Proc. Logic Colloquium'87, North-Holland, 1988. To appear.
• 41: J Meseguer , J A Goguen, Initiality, induction, and computability, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 42: A. R. Meyer , J. C. Mitchell , E. Moggi , R. Statman, Empty types in polymorphic lambda calculus, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.253-262, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41648]
• 43: Andrew M. Pitts, Polymorphism is Set Theoretic, Constructively, Category Theory and Computer Science, p.12-39, September 07-09, 1987
• 44: A.M. Pitts. An extension of reynolds' result on the non-existence of set-models of polymorphism. Communication in the Types electronic forum ([e-mail]), May 29, 1988.
• 45: A.M. Pitts and P. Taylor. A note on rusel's paradox in locally cartesian closed categories. 1987. University of Sussex.
• 46: John C. Reynolds , Gordon D. Plotkin, On functors expressible in the polymorphic lambda calculus, Logical foundations of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 47: J.C. Reynolds. Polymorphism is not set-theoretic. In G. Kahn, D.B. MacQueen, and G.D. Plotkin, editors, Semantics of Data Types, pages 145-156, Springer Lecture Notes in Computer Science 173, 1984.
• 48: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 49: J.C. Reynolds. Types, Abstraction, and Parametric Polymorphism. In R.E.A. Mason, editor, Information Processing '83, pages 513-523, North-Holland, 1983,
• 50: Edmund Robinson. How complete is PER? Technical Report 88-229, Queen's University, Department of Computing and Information Science, 1988.
• 51: Edmund Robinson. Personal communication. July 1988.
• 52: D.S. Scott. Data Types as Lattices. SIAM Journal of Computing, 5:522-587, 1976.
• 53: R. A. G. Seely. Categorical semantics for higher order polymorphic laznbda calculus. J. Symbol. Logic, 52(4):969-9s9, 19s7.
• 54: R. A. G. Seely. Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soe., 95:33--48, 1984.
• 55: P. Taylor. Reeursive Domains, indexed Category Theory and Polymorphism. PhD thesis, Mathematics Department, University of Cambridge, 1987.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Design, Languages, Theory