Type dispatch for named hierarchical types

ABSTRACT

Type dispatch constructs are an important feature of many programming languages. Scheme has predicates for testing the runtime type of a value. Java has a class cast expression and a try statement for switching on an exception's class. Crucial to these mechanisms, in typed languages, is type refinement: The static type system will use type dispatch to refine types in successful branches. Considerable previous work has addressed type case constructs for structural type systems without subtyping, but these do not extend to named type systems with subtyping, as is common in object oriented languages. Previous work on type dispatch in named type systems with subtyping has not addressed its implementation formally.This paper describes a number of type dispatch constructs that share a common theme: class cast and class case constructs in object oriented languages, ML style exceptions, hierarchical extensible sums, and multimethods. I describe a unifying mechanism, tagging, that abstracts the operation of these constructs, and I formalise a small tagging language. After discussing how to implement the tagging language, I present a typed language without type dispatch primitives, and a give a formal translation from the tagging language.

REFERENCES

• AC96: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• ACPP91: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• CGL95: 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]
• Cha97: Craig Chambers. The Cecil language, specification and rationale. Technical report, Department of Computer Science and Engineering, University of Washington, Box '352350, Seattle, Washington 98195-2350, USA, March 1997.
• CW99: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• CWM98: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
• FR99: Kathleen Fisher , John Reppy, The design of a class mechanism for Moby, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.37-49, May 01-04, 1999, Atlanta, Georgia, United States
• GJS96: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• Gle99: Neal Glew, Type Dispatch for Named Hierarhical Types, Cornell University, Ithaca, NY, 1999
• HM95: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• HS97: Robert Harper and Christopher Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, Carnegie Mellon University, Pittsburgh, PA 15213, June 1997.
• KCR98: N. I. Adams, IV , D. H. Bartley , G. Brooks , R. K. Dybvig , D. P. Friedman , R. Halstead , C. Hanson , C. T. Haynes , E. Kohlbecker , D. Oxley , K. M. Pitman , G. J. Rozas , G. L. Steele, Jr. , G. J. Sussman , M. Wand , H. Abelson, Revised5 report on the algorithmic language scheme, ACM SIGPLAN Notices, v.33 n.9, p.26-76, Sept. 1, 1998 [doi>10.1145/290229.290234]
• MCG+99: Greg Morrisett, Karl Crary, Neal Clew, Dan Grossman, Richard Samuels, Frederick Smith, Daivd Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In A CM SIGPLAN Workshop on Compiler Support for System Software, volume 0228 of INRIA Research Reports, Atlanta, CA, USA, May 1999.
• MFH95: Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
• Mor95: Greg Morrisett. Compiling with ~lpes. PhD thesis, Carnegie Mellon University, December 1995. Published as CMU Technical Report CMU-CS-95-226.
• MWCG98: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• RR96: John Reppy , Jon Riecke, Simple objects for Standard ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.171-180, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• TMC+96: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional 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