A semantic model of types for applicative languages

ABSTRACT

If integer constants are added to the syntax of the pure lambda calculus, then primitive integer values have to be added to the underlying domain V of values. Unlike functions, primitive values should not be applied; we want a run-time error to occur if an attempt is made to apply them as functions. Expressions that might lead to run-time errors are separated out by imposing a “type” structure on expressions. A systematic model of types is developed, in which types are formalized as “ideals” (sets with a certain structure). Polymorphic functions are handled by introducing a quantifier for taking conjunctions of types. Operations for constructing new types from old lead to the consideration of higher-order or meta types, which are called “kinds” to avoid confusion with types. Finally, the semantic model of types is applied to show the soundness of a proof system for inferring the types of expressions.

REFERENCES

• 1: Mario Coppo, An Extended Polymorphic Type System for Applicative Languages, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.194-204, September 01-05, 1980
• 2: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 3: 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]
• 4: M. J. C. Gordon, "A note on the semantics of explicitly quantified polymorphic types," manuscript (1979).
• 5: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 6: A. R. Meyer, Personal communication, January 1982.
• 7: R. Milner, "A theory of type polymorphism in programming," JCSS17(3), pp. 348-375 (December 1978).
• 8: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 9: D. S. Scott, "The lattice of flow diagrams," pp. 311-372 in Symposium on Semantics of Algorithmic Languages, ed. E. Engeler, Lecture Notes in Mathematics 188, Springer-Verlag, Berlin (1971).
• 10: D. S. Scott, "Data types as lattices," SIAM J. Computing5(3), pp. 522-587 (September 1976).
• 11: D. S. Scott, Personal communication, January 1982.
• 12: Adi Shamir , William W. Wadge, Data Types as Objects, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.465-479, July 18-22, 1977
• 13: W. W. Wadge, Personal communication to R. Milner, March 1978.
• 14: M. Wand, Personal communication, January 1982.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

  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