Types as intervals

ABSTRACT

To accommodate polymorphic data types and operations, several computer scientists--most notably MacQueen, Plotkin, and Sethi--have proposed formalizing types as ideals. Although this approach is intuitively appealing, the resulting type system is both complex and restrictive because the type constructor that creates function types is not monotonic, and hence not computable. As a result, types cannot be treated as data values, precluding the formalization of type constructors and polymorphic program modules (where types are values) as higher order computable functions. Moreover, recursive definitions of new types do not necessarily have solutions. This paper proposes a new formulation of types--called intervals--that subsumes the theory of types as ideals, yet avoids the pathologies caused by non-monotonic type constructors. In particular, the set of interval types contains the set of ideal types as a proper subset and all of the primitive type operations on intervals are extensions of the corresponding operations on ideals. Nevertheless, all of the primitive interval type constructors including the function type constructor and type quantifiers are computable operations. Consequently, types are higher order data values that can be freely manipulated within programs. The key idea underlying the formalization of types as intervals is that negative information should be included in the description of a type. Negative information identifies the finite elements that do not belong to a type, just as conventional, positive information identifies the elements that do. Unless the negative information in a type description is the exact complement of the positive information, the description is partial in the sense that it approximates many different types--an interval of ideals between the positive information and the complement of the negative information. Although programmers typically deal with total (maximal) types, partial types appear to be an essential feature of a comprehensive polymorphic type system that accommodates types as data, just as partial functions are essential in any universal programming language.

REFERENCES

• 1: J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977 [doi>10.1145/321992.321997]
• 2: [Bana22] Banach, S. "Sur les operations dans les ensembles abstraits et leurs applications aux equations integrales," Fund. Math. 3 (1922) pp. 7-33.
• 3: [Burs84] Burstall, R. and B. Lampson, The Cedar Kernel Language, unpublished draft, Xerox Palo Alto Research Center, 1984.
• 4: Robert Cartwright, A constructive alternative to axiomatic data type definitions, Proceedings of the 1980 ACM conference on LISP and functional programming, p.46-55, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802789]
• 5: Robert Cartwright , James Donahue, The semantics of lazy (and industrious) evaluation, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.253-264, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802157]
• 6: [Ende72] Enderton, H. B. A Mathematical Introduction to Logic. Academic Press, New York, 1972.
• 7: [Gier80] Gierz, G. et. al. A Compendium of Continuous Lottices. Springer-Verlag, Berlin, 1980.
• 8: [Gord77] Gordon, M., R. Milner and C. Wadsworth. Edinburgh LCF. CSR-11-77. Computer Science Department, Edinburgh University.
• 9: [Gutt78] Guttag, J. V. and J. J. Horning. The Algebraic Specification of Data Structures, Comm. ACM 20, 395- 404.
• 10: [Hind69] Hindley, R. The Principal Type Scheme of an Object of Combinatory Logic. Trans. AMS 146, pp. 29-60, (December 1969).
• 11: D. B. MacQueen , Ravi Sethi, A semantic model of types for applicative languages, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.243-252, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802156]
• 12: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.165-174, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800528]
• 13: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• 14: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., Syracuse University, Syracuse, NY, 1979
• 15: [Miln78] Milner, R. A Theory or Type Polymorphism for Programming, JCSS 17(3), pp. 348-375.
• 16: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 17: [plot78] Plotkin, G. T^¿ as a Universal Domain. Journal of Computer and System Sciences 17 (1978), pp. 209-236.
• 18: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 19: [Scot76] Scott, D. Data Types as Lattices. SIAM J. Computing 5(1976), pp. 522-587.
• 20: [Scot81] Scott, D. Lectures on a Mathematical Theory of Computation. Technical Monograph PRG-19, Oxford University Computing Laboratory, Oxford.
• 21: [Scot83] Scott, D. Domains for Denotational Semantics. Technical Report, Computer Science Department, Carnegie-Mellon University, 1983.
• 22: 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
• 23: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Design, Languages, Performance, Theory, Verification