Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types

ABSTRACT

Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. This work shows how to define a subtyping relation semantically in the presence of Boolean connectives, functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• 2: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 3: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 4: Roberto M. Amadio , Pierre-Louis Curien, Domains and lambda-calculi, Cambridge University Press, New York, NY, 1998
• 5: Andrea Asperti , Giuseppe Longo, Categories, types, and structures: an introduction to category theory for the working computer scientist, MIT Press, Cambridge, MA, 1991
• 6: Franco Barbanera , Mariangiola Dezani-Ciancaglini , Ugo De'Liguoro, Intersection and union types: syntax and semantics, Information and Computation, v.119 n.2, p.202-230, June 1995 [doi>10.1006/inco.1995.1086]
• 7: Barendregt, H., Coppo, M., and Dezani-Ciancaglini, M. 1983. A filter lambda model and the completeness of type assignment. J. Symb. Logic 48, 4, 931--940.
• 8: Véronique Benzaken , Giuseppe Castagna , Alain Frisch, CDuce: an XML-centric general-purpose language, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.51-63, August 25-29, 2003, Uppsala, Sweden
• 9: Castagna, G. 2005. Semantic subtyping: Challenges, perspectives, and open problems. In ICTCS 2005, Proceedings of the Italian Conference on Theoretical Computer Science. Lecture Notes in Computer Science, vol. 3701. Springer-Verlag, New York, 1--20.
• 10: Giuseppe Castagna , Daniele Varacca, Semantic Subtyping for the p-Calculus, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.92-101, June 26-29, 2005 [doi>10.1109/LICS.2005.46]
• 11: Castagna, G., De Nicola, R., and Varacca, D. 2007. Semantic subtyping for the π-calculus. Theoretical Computer Science. Special issue in honor of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca. To appear.
• 12: Castagna, G., Dezani-Ciancaglini, M., and Varacca, D. 2006. Encoding Cduce into the π-calculus. In CONCUR 2006, Proceedings of the 17th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 4137. Springer-Verlag, New York, 310--326.
• 13: Giuseppe Castagna , Alain Frisch, A gentle introduction to semantic subtyping, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.198-199, July 11-13, 2005, Lisbon, Portugal [doi>10.1145/1069774.1069793]
• 14: Giuseppe Castagna , Giorgio Ghelli , Giuseppe Longo, A Semantics for Lambda&-early: A Calculus with Overloading and Early Binding, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.107-123, March 16-18, 1993
• 15: Giuseppe Castagna , Giorgio Ghelli , Giuseppe Longo, A calculus for overloaded functions with subtyping, Information and Computation, v.117 n.1, p.115-135, Feb. 15, 1995 [doi>10.1006/inco.1995.1033]
• 16: CDUCE. The Cduce programming language. http://www.cduce.org.
• 17: Coppo, M., and Dezani-Ciancaglini, M. 1980. An extension of the basic functionality theory for the λ-calculus. Notre-Dame J. Formal Logic 21, 4 (Oct.), 685--693.
• 18: Damm, F. 1994a. Subtyping with union types, intersection types and recursive types II. Research Report 816, IRISA.
• 19: Flemming M. Damm, Subtyping with Union Types, Intersection Types and Recursive Types, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.687-706, April 19-22, 1994
• 20: 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
• 21: Dezani-Ciancaglini, M., Frisch, A., Giovannetti, E., and Motohama, Y. 2002. The relevance of semantic subtyping. In Intersection Types and Related Systems. Electronic Notes in Theoretical Computer Science 70, 1.
• 22: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 23: Frisch, A. 2004. Théorie, conception et réalisation d'un langage de programmation fonctionnel adapté à XML. Ph.D. dissertation. Université Paris 7.
• 24: Alain Frisch, OCaml + XDuce, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 25: 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
• 26: Gapayev, V., and Pierce, B. 2003. Regular object types. In Proceedings of the ECOOP '03. Lecture Notes in Computer Science, Springer-Verlag, New York.
• 27: Hindley, R., and Longo, G. 1980. Lambda-calculus models and extensionality. Zeit. Math. Logik Grund. Math. 26, 2, 289--319.
• 28: Hosoya, H. 2001. Regular expression types for XML. Ph.D. dissertation, The University of Tokyo, Tokyo, Japan.
• 29: Haruo Hosoya , Alain Frisch , Giuseppe Castagna, Parametric polymorphism for XML, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.50-62, January 12-14, 2005, Long Beach, California, USA
• 30: Haruo Hosoya , Benjamin Pierce, Regular expression pattern matching for XML, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.67-80, January 2001, London, United Kingdom
• 31: 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]
• 32: 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
• 33: 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]
• 34: Paul-Andre Mellies , Jerome Vouillon, Recursive Polymorphic Types and Parametricity in an Operational Framework, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.82-91, June 26-29, 2005 [doi>10.1109/LICS.2005.42]
• 35: Pfenning, F. 1993. Refinement types for logical frameworks. In Informal Proceedings of the Workshop on Types for Proofs and Programs, H. Geuvers, Ed. Nijmegen, The Netherlands, 285--299.
• 36: Pierce, B. 1991. Programming with intersection types, union types, and polymorphism. Tech. Rep. CMU-CS-91-106, School of Computer Sciente, Carnegie Mellon University.
• 37: Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In Information Processing, R. E. A. Mason, Ed. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, The Netherlands, 513--523.
• 38: John C. Reynolds, The Coherence of Languages with Intersection Types, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.675-700, September 24-27, 1991
• 39: Reynolds, J. C. 1996. Design of the programming language Forsythe. Tech. Rep. CMU-CS96-146, Carnegie Mellon University, Pittsburgh, PA, June.
• 40: Studer, T. 2001. A semantics for λ-{}: A calculus with overloading and late-binding. J. Logic Computation 11, 4, 527--544.
• 41: Hideki Tsuiki, A Normalizing Calculus with Overloading and Subtyping, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.273-295, April 19-22, 1994
• 42: Jérôme Vouillon, Polymorphic regular tree types and patterns, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.103-114, January 11-13, 2006, Charleston, South Carolina, USA
• 43: Jerome Vouillon , Paul-André Melliès, Semantic types: a fresh look at the ideal model for types, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.52-63, January 14-16, 2004, Venice, Italy

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

General Terms:
Languages, Theory

Keywords:
Subtyping, higher-order functions, intersection types, negation types, union types