Subtyping recursive types

ABSTRACT

We investigate the interactions of subtyping and recursive types, in a simply typed &lgr;-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, we relate various definitions of type equivalence and subtyping that are induced by a model, an ordering on infinite trees, an algorithm, and a set of type rules. We show soundness and completeness among the rules, the algorithm, and the tree semantics. We also prove soundness and a restricted form of completeness for the model. To address the second question, we show that to every pair of types in the subtype relation we can associate a term whose denotation is the uniquely determined coercion map between the two types. Moreover, we derive an algorithm that, when given a term with implicit coercions, can infer its least type whenever possible.

REFERENCES

• 1: AMADiO, R. Formal theones of inheritance for typed funct~onal languages. Tech. Rep. TR 28/89, Dip. dl Informatica, Univ. dl Fisa, Pisa, Italy, 1989.
• 2: Roberto M. Amadio, Typed Equivalence, Type Assignment, and Type Containment, Proceedings of the 2nd International CTRS Workshop on Conditional and Typed Rewriting Systems, p.372-382, June 11-14, 1990
• 3: Roberto M. Amadio, Recursion over realizability structures, Information and Computation, v.91 n.1, p.55-85, March 1991 [doi>10.1016/0890-5401(91)90074-C]
• 4: ARNOLD, A., AND NIVAT, M. The metric space of infinite trees. Algebraic and topological properties. Fundamenta Inf. III. (1980), 445 476.
• 5: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 6: REAZU-TANNEN, V., GUNTER, C., AND SCEDROV, A. Denotational semantics for subtyping between recursive types. Rep. MS-CIS 89 63, Logic of Computation 12, Dept. of Computer and Information Science, Univ. of Pennsylvania, Philadelphia, 1989.
• 7: Kim B. Bruce , Giuseppe Longo, A modest model of records, inheritance, and unbounded quantification, Information and Computation, v.87 n.1-2, p.196-240, July/August 1990 [doi>10.1016/0890-5401(90)90062-M]
• 8: Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
• 9: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• 10: Luca Cardelli, Amber, Proceedings of the Thirteenth Spring School of the LITP on Combinators and Functional Programming Languages, p.21-47, May 06-10, 1985
• 11: CARDELLI, L. Typeful programming. In Formal Descrtption of Programming Concepts, E. J. Neuhold and M. Paul, Eds. Springer-Verlag, New York, 1991, 431 507.
• 12: CARDELLI, L., AND LONaO, G. A semantic basis for Quest. J. Functional Program. 1, 4 (Oct. 1991), 417-458.
• 13: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 14: Felice Cardone , Mario Coppo, Type inference with recursive types: syntax and semantics, Information and Computation, v.92 n.1, p.48-80, May 1991 [doi>10.1016/0890-5401(91)90020-3]
• 15: William R. Cook, A denotational semantics of inheritance, 1989
• 16: COURCELLE, B. Fundamental properties of infinite trees. Theor. Comput. Sci. 25, (1983), 95-169.
• 17: COURCELLE, B. Equivalence and transformation of regular systems--Applications to recursive program schemes and gTammars. Theor. Comput. Sci. 42, (1986), I 122.
• 18: CURIEN, P.-L., AND GHELLI, G. Coherence of subsumption, minimum typing and type checking in F<. Math. Struc. Comput. Sci. 2, (1992), 55 91.
• 19: H~ANo, M. A small complete category. Ann. Pure Appl. Logic 40, 2, (1989), 135 165.
• 20: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 21: MmNER, R. A complete inference system for a class of regular behaviors. J. Comput. Syst. Sci. 28 (1984), 439-466.
• 22: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 23: David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
• 24: Benjamin C. Pierce, Bounded quantification is undecidable, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.305-315, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143228]
• 25: Arto Salomaa, Two Complete Axiom Systems for the Algebra of Regular Events, Journal of the ACM (JACM), v.13 n.1, p.158-169, Jan. 1966 [doi>10.1145/321312.321326]
• 26: SCOTT, D. Continuous lattices. In Toposes, Algebraic Geometry and Logic. Lecture Notes in Mathematics 274. Springer-Verlag, New York, 1972, 97 136.
• 27: SCOTT, D. Data types as lattices. SIAM J. Comput. 5, (1976), 522-587.
• 28: A. van Wijngaarden, Report on the algorithmic language ALGOL 68, Printing by the Mathematisch Centrum, 1969
• 29: W,OSWORTH, C. The relation between computational and denotational properties for Scott's D~ models ofthe lambda-calculus. SIAM J. Comput. 5, (1976), 488-521.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Program and recursion schemes

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.3 Language Constructs and Features
          Subjects: Recursion; Abstract data types

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Algorithms, Languages, Theory

Keywords:
coercions, lambda-calculus, partial-equivalence relations, recursive types, regular trees, subtyping, tree orderings, type equivalence, typechecking algorithm