Typed compilation of inclusive subtyping

ABSTRACT

I present a type-preserving translation that eliminates subtyping and bounded quantification without introducing any run-time costs. This translation is based on Mitchell and Pierce's encoding of bounded quantification using intersection types. I show that, previous negative observations notwithstanding, the encoding is adequate given a sufficiently rich target type theory. The necessary target type theory is made easily typecheckable by including a collection of explicit coercion combinators, which are already desired for eliminating subtyping. However, no form of coercion abstraction is necessary (even to support bounded quantification), leading to a simple target language.

REFERENCES

• 1: 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]
• 2: Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An extension of system F with subtyping, Information and Computation, v.109 n.1-2, p.4-56, Feb. 15/March 1994 [doi>10.1006/inco.1994.1013]
• 3: 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]
• 4: 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
• 5: Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in F. Mathematical Structures in Computer Science, 2(1):55-91, 1992.
• 6: Allyn Dimock , Robert Muller , Franklyn Turbak , J. B. Wells, Strongly typed flow-directed representation transformations (extended abstract), Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.11-24, June 09-11, 1997, Amsterdam, The Netherlands
• 7: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support for System Software, Atlanta, May 1999.
• 8: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 9: Benjamin Crawford Pierce, Programming with intersection types and bounded polymorphism, Carnegie Mellon University, Pittsburgh, PA, 1992
• 10: Benjamin C. Pierce, Intersection types and bounded polymorphism, Mathematical Structures in Computer Science, v.7 n.2, p.129-193, April 1997 [doi>10.1017/S096012959600223X]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Performance, Theory