Intensional polymorphism in type-erasure semantics

ABSTRACT

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion.We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.

REFERENCES

• 1: Shail Aditya , Alejandro Caro, Compiler-directed type reconstruction for polymorphic languages, Proceedings of the conference on Functional programming languages and computer architecture, p.74-82, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165192]
• 2: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• 3: R. L. Constable. Intensional analysis of functions and types. Technical Report CSR-118-82, Department of Computer Science, University of Edinburgh, June 1982.
• 4: Robert L. Constable , Daniel R. Zlatin, The Type Theory of PL/CV3, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.94-117, Jan. 1984 [doi>10.1145/357233.357238]
• 5: Joëlle Despeyroux , Frank Pfenning , Carsten Schürmann, Primitive Recursion for Higher-Order Abstract Syntax, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.147-163, April 02-04, 1997
• 6: Catherine Dubois , François Rouaix , Pierre Weis, Extensional polymorphism, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.118-129, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199473]
• 7: Dominic Duggan, A Type-Based Semantics for User-Defined Marshalling in Polymorphic Languages, Proceedings of the Second International Workshop on Types in Compilation, p.273-297, March 25-27, 1998
• 8: J.-Y. Girard. Une extension de l'interprdtation de GSdel ~ l'analyse, et son application ~ l'~limination de coupures dans l'analyse et la th~orie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium,, pages 63-92. North-Holland Publishing Co., 1971.
• 9: J.-Y. Girard. Interprdtation fonctionelle et dlimination des coupures de l'arithmdtique d'ordre sup&'ieur. PhD thesis, Universit6 Paris VII, 1972.
• 10: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 11: 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]
• 12: Mark P. Jones, A theory of qualified types, Symposium proceedings on 4th European symposium on programming, p.287-306, January 1992, Rennes, France
• 13: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• 14: Y. Minamide. Full lifting of type parameters. Submitted for publication. Earlier version published as "Compilation Based on a Calculus for Explicit Type-Passing" in the Second Fuji International Workshop on Functional and Logic Programming, 1996.
• 15: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 16: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 17: G. Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, Dec. 1995.
• 18: 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]
• 19: G. Morrisett , R. Harper, Semantics of memory management for polymorphic languages, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 20: G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software, Tucson, Feb. 1996.
• 21: 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]
• 22: J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing '83, pages 513-523. North-Holland, 1983. Proceedings of the IFIP 9th World Computer Congress.
• 23: Erik Ruf, Partitioning dataflow analyses using types, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 15-17, 1997, Paris, France [doi>10.1145/263699.263705]
• 24: Bratin Saha , Zhong Shao, Optimal Type Lifting, Proceedings of the Second International Workshop on Types in Compilation, p.156-177, March 25-27, 1998
• 25: Zhong Shao, Flexible representation analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.85-98, June 09-11, 1997, Amsterdam, The Netherlands
• 26: Z. Shao. An overview of the FLINT/ML compiler. In I997 Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Department Technical Report BCCS-97-03.
• 27: 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
• 28: Andrew Tolmach, Tag-free garbage collection using explicit type parameters, Proceedings of the 1994 ACM conference on LISP and functional programming, p.1-11, June 27-29, 1994, Orlando, Florida, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Design, Languages, Performance, Theory