Semantic types: a fresh look at the ideal model for types

ABSTRACT

We present a generalization of the ideal model for recursive polymorphic types. Types are defined as sets of terms instead of sets of elements of a semantic domain. Our proof of the existence of types (computed by fixpoint of a typing operator) does not rely on metric properties, but on the fact that the identity is the limit of a sequence of projection terms. This establishes a connection with the work of Pitts on relational properties of domains. This also suggests that ideals are better understood as closed sets of terms defined by orthogonality with respect to a set of contexts.

REFERENCES

• 1: M. Abadi , B. Pierce , G. Plotkin, Faithful ideal models for recursive polymorphic types, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.216-225, June 1989, Pacific Grove, California, United States
• 2: M. Abadi and G. Plotkin. A per model of polymorphism and recursive types. In J. Mitchell, editor, 5th Annual IEEE Symposium on Logic in Computer Science, pages 355--365. IEEE Computer Society Press, 1990.
• 3: Samson Abramsky , Achim Jung, Domain theory, Handbook of logic in computer science (vol. 3): semantic structures, Oxford University Press, Oxford, 1995
• 4: 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]
• 5: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 6: Lars Birkedal , Robert Harper, Relational interpretations of recursive types in an operational setting, Information and Computation, v.155 n.1-2, p.3-63, Nov./Dec. 1999 [doi>10.1006/inco.1999.2828 ]
• 7: G. Birkhoff. Lattice theory, volume 25 of Colloquium Publications. American Mathematical Society, 1940.
• 8: Michael Brandt , Fritz Henglein, Coinductive Axiomatization of Recursive Type Equality and Subtyping, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.63-81, April 02-04, 1997
• 9: Kim Bruce , John C. Mitchell, PER models of subtyping, recursive types and higher-order polymorphism, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-327, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143230]
• 10: Felice Cardone, Relational Semantics for Recursive Types and Bounded Quantification, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.164-178, July 11-15, 1989
• 11: Robert Cartwright, Types as intervals, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.22-36, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318604]
• 12: J. Chroboczek. Subtyping recursive games. In Proceedings of the Fifth International Conference on Typed Lambda Calculi and Applications (TLCA'01)., Kraków, Poland, May 2001.
• 13: Laurent Dami, Labelled Reductions, Runtime Errors and Operational Subsumption, Proceedings of the 24th International Colloquium on Automata, Languages and Programming, p.782-793, July 07-11, 1997
• 14: L. Dami. Operational subsumption, an ideal model of subtyping. In A. D. Gordon, A. M. Pitts, and C. Talcott, editors, HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics, volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2000.
• 15: F. Damm. Subtyping with union types, intersection types and recursive types II. Research Report 2259, INRIA Rennes, May 1994.
• 16: Vincent Danos , Jean-Louis Krivine, Disjunctive Tautologies as Synchronisation Schemes, Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, p.292-301, August 21-26, 2000
• 17: Rowan Davies , Frank Pfenning, Intersection types and computational effects, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.198-208, September 2000
• 18: M. Erné, J. Koslowski, A. Melton, and G. E. Strecker. A primer on Galois connections. In A. R. Todd, editor, Papers on general topology and applications (Madison, WI, 1991), volume 704 of Annals of the New York Academy of Sciences, pages 103--125, New York, 1993. New York Acad. Sci.
• 19: M. P. Fiore. A coinduction principle for recursive data types based on bisimulation. Information and Computation, 127(2):186--198, 1996.
• 20: P. J. Freyd. Algebraically complete categories. In A. Carboni, M. C. Pedicchio, and G. Rosolini, editors, Proceedings of the 1990 Como Category Theory Conference, volume 1488 of Lecture Notes in Mathematics, pages 95--104. Springer--Verlag, 1991.
• 21: Alain Frisch , Giuseppe Castagna , Véronique Benzaken, Semantic Subtyping, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.137-146, July 22-25, 2002
• 22: Vladimir Gapeyev , Michael Y. Levin , Benjamin C. Pierce, Recursive subtyping revealed, Journal of Functional Programming, v.12 n.6, p.511-548, November 2002 [doi>10.1017/S0956796802004318]
• 23: Jean-Yves Girard, Locus Solum: From the rules of logic to the logic of rules, Mathematical Structures in Computer Science, v.11 n.3, p.301-506, June 2001 [doi>10.1017/S096012950100336X]
• 24: Andrew D. Gordon , Andrew M. Pitts, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 25: Jean Goubault-Larrecq , Slawomir Lasota , David Nowak, Logical Relations for Monadic Types, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.553-568, September 22-25, 2002
• 26: Haruo Hosoya , Benjamin C. Pierce, XDuce: A statically typed XML processing language, ACM Transactions on Internet Technology (TOIT), v.3 n.2, p.117-148, May 2003 [doi>10.1145/767193.767195]
• 27: Haruo Hosoya , Jérôme Vouillon , Benjamin C. Pierce, Regular expression types for XML, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.11-22, September 2000
• 28: J. M. E. Hyland. A syntactic characterization of the equality in some models of the λ-calculus. Journal of the London Mathematical Society, 12(2):361--370, 1976.
• 29: Proceedings of the the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montréal, Canada, Sept. 2000. ACM Press.
• 30: J.-J. Lévy. An algebraic interpretation of the lambda beta K-calculus; and an application of a labelled lambda-calculus. Theoretical Computer Science, 2(1):97--114, June 1976.
• 31: 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]
• 32: Ian A. Mason , Scott F. Smith , Carolyn L. Talcott, From operational semantics to domain theory, Information and Computation, v.128 n.1, p.26-47, July 10, 1996 [doi>10.1006/inco.1996.0061 ]
• 33: B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.
• 34: A. M. Pitts. Relational properties of domains. Information and Computation, 127:66--90, 1996.
• 35: Andrew M. Pitts, Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, v.10 n.3, p.321-359, June 2000 [doi>10.1017/S0960129500003066]
• 36: A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In Gordon and Pitts {24}, pages 227--273.
• 37: S. F. Smith. The coverage of operational semantics. In Gordon and Pitts {39}, pages 307--346.
• 38: B. M. R. Stadler and P. F. Stadler. Basic properties of closure spaces, 2002. Supplemental material for {39}.
• 39: B. M. R. Stadler and P. F. Stadler. Generalized topological spaces in evolutionary theory and combinatorial chemistry. J. Chem. Inf. Comput. Sci., 42:577--585, 2002. Proceedings MCC 2001, Dubrovnik.
• 40: Ian Stark, Names, equations, relations: practical ways to reason about new, Fundamenta Informaticae, v.33 n.4, p.369-396, April 1998
• 41: C. Talcott, Reasoning about functions with effects, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 42: C. P. Wadsworth. The relation between computational and denotational properties for Scott's D∞-models of the lambda-calculus. SIAM Journal on Computing, 5(3):488--521, Sept. 1976.

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.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Languages, Theory

Keywords:
ideal model, inductive/coinductive principle, polymorphism, realizability, recursive types, subtyping