A types-as-sets semantics for milner-style polymorphism

ABSTRACT

In this paper we present a semantics for Milner-style polymorphism in which types are sets. The basic picture is that our programs are actually terms in a typed &lgr;-calculus, in which the type information can be safely deleted from the concrete syntax. In order to allow for common programming constructs, we allow reflexive or infinite types, and we also allow opaque types, which have private representations. An adaptation of Hindley's Principal Typing Theorem then asserts that the type information can be reconstructed. Thus expressions are polymorphic, since they may have more than one correct typing, but values are not. Expressions that are not well-typed are syntactically ill-formed, as they are in conventional mathematics, rather than having the meaning “wrong”. The resulting semantics is simpler than that for fully polymorphic models [Leivant 83], and generalizes the standard constructions, such as retracts and ideals.

REFERENCES

• 1: Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam, 1981.
• 2: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 3: Donahue, J. "On the Semantics of 'Data Type'," SIAM J. Comput. 8(1979), 546-560.
• 4: Fokkiuga, M.M. "On the Notion of Strong Typing," in Algorithmic Languages(deBakker and van Vliet, eds.), North-Holland, 1981, pp. 305-320.
• 5: M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512773]
• 6: Haynes, C. T. "A Theory of Data Type Representation Independence," *University of Iowa Computer Science Department Technical Report Numer 82-04, December, 1982.
• 7: Peter Henderson, Functional Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 8: Hindley, R. "The Principal Type-Scheme of an Object in Combinatory Logic," Trans. Am. Math. Soc. 146 (1969) 29-60.
• 9: Lehmann, D.J. and Smyth, M.B. "Algebraic Specification of Data Types: A Synthetic Approach," Math. Sys. Th. 14 (1981), 97-139.
• 10: Daniel Leivant, Structural semantics for polymorphic data types (preliminary report), Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.155-166, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567083]
• 11: Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
• 12: MacQueen, D.B., Plotkin, G., and Sethi, R. "An Ideal Model for Recursive Polymorphic Types," presentation at Workshop on Data Types, Carnegie-Mellon University, June 9-10, 1983.
• 13: Meyer, A.R. "What Is a Model of the Lambda Calculus," Information and Control 52 (1982), 87-122.
• 14: Milner, R. "A Theory of Type Polymorphism in Programming," J. Comp. @@@@ Sys. Sci. 17 (1978), 348-375.
• 15: Pottinger, G. "The Church-Rosser Theorem for the Typed &lgr;-Calculus with Subjective Pairing," Notre Dame Journal of Formal Logic 22 (1981) 264-268.
• 16: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 17: Reynolds, J.C. "User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction" Conf. on New Directions on Algorithmic Languages, IFIP WG 2.1, Munich, August, 1975.
• 18: Reynolds, J.C. "The Essence of Algol," in Algorithmic Languages, (J. W. deBakker and J.C. van Vliet, eds.) North-Holland, Amsterdam, 1981, pp. 345-372.
• 19: Reynolds, J.C. "Types, Abstractions, and Parametric Polymorphism," Proc. IFIP 83.
• 20: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 21: Scott, D. "Continuous Lattices" in Toposes, Algebraic Geometry, and Logic (F.W. Lawvere, ed.), Lecture Notes in Mathematics. vol. 274, Springer-Verlag, New York, pp. 97-136.
• 22: Scott, D. "Data Types as Lattices" SIAM J. Comput. 5 (1976), 522-587.
• 23: Scott, D. "Relating theories of the &lgr;-calculus," in To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism (Hindley and Seldin, eds.) Academic Press, New York and London, 1980, pp. 403-450.
• 24: Mitchell Wand, Semantics-directed machine architecture, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-241, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582179]
• 25: Mitchell Wand, Loops in combinator-based compilers, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.190-196, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567086]
• 26: Wand, M. "A Semantic Prototyping System," June, 1983.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

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

General Terms:
Languages