Compiling polymorphism using intensional type analysis

ABSTRACT

Traditional techniques for implementing polymorphism use a universal representation for objects of unknown type. Often, this forces a compiler to use universal representations even if the types of objects are known. We examine an alternative approach for compiling polymorphism where types are passed as arguments to polymorphic routines in order to determine the representation of an object. This approach allows monomorphic code to use natural, efficient representations, supports separate compilation of polymorphic definitions and, unlike coercion-based implementations of polymorphism, natural representations can be used for mutable objects such as refs and arrays.We are particularly interested in the typing properties of an intermediate language that allows run-time type analysis to be coded within the language. This allows us to compile many representation transformations and many language features without adding new primitive operations to the language. In this paper, we provide a core target language where type-analysis operators can be coded within the language and the types of such operators can be accurately tracked. The target language is powerful enough to code a variety of useful features, yet type checking remains decidable. We show how to translate an ML-like language into the target language so that primitive operators can analyze types to produce efficient representations. We demonstrate the power of the “user-level” operators by coding flattened tuples, marshalling, type classes, and a form of type dynamic within the language.

REFERENCES

• 1: M. Abadi , L. Cardelli , B. Pierce , G. Plotkin, Dynamic typing in a statically-typed language, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-227, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75296]
• 2: 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]
• 3: 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]
• 4: S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken. The semantics of reflected proof. In Fifth Symposium on Logic in Computer Science, pages 95-106, Philadelphia, PA, June 1990. IEEE.
• 5: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 6: Guy E. Blelloch , Jonathan C. Hardwick , Siddhartha Chatterjee , Jay Sipelstein , Marco Zagha, Implementation of a portable nested data-parallel language, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.102-111, May 19-22, 1993, San Diego, California, United States
• 7: 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]
• 8: L. Cardelli. Phase distinctions in type theory. Unpublished manuscript.
• 9: L. Cardelli. Typeful programming. Technical Report 45, DEC Systems Research Center, 1989.
• 10: Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
• 11: Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
• 12: R. L. Constable. Intensional analysis of functions and types. Technical Report CSR-t18-82, Computer Science Department, University of Edinburgh, June 1982.
• 13: 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]
• 14: D. Duggan and J. Ophel. Kinded parametric overloading. Technical Report CS-94-35, University of Waterloo, Department of Computer Science, September 1994. Supersedes CS-94-15 and CS-94-16, March 1994, and CS-93-32, August 1993.
• 15: H. Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloquium '75, Studies in Logic and the Foundations of Mathematics, pages 22-37. North-Holland, 1975.
• 16: J.-Y. Girard. Une extension de l'interpr#tation de Ghdel t# l'analyse, et son application k l'dlimination des coupures dans l'analyse et la th#orie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics, pages 63-92. North-Holland, 1971.
• 17: J.-Y. Girard. Interprdtation Fonctionnelle et t#limination des Coupures dans I'Arithmdtique d'Ordre Supdrieure. PhD thesis, Universit6 Paris VII, 1972.
• 18: K. Ghdel. Uber eine bisher noch nicht benfitzte Erweiterung des finiten Standpunktes. Dialectica, 12:280-287, 1958.
• 19: Carl A. Gunter , Elsa L. Gunter , David B. MacQueen, Computing ML equality kinds using abstract interpretation, Information and Computation, v.107 n.2, p.303-323, Dec. 1993 [doi>10.1006/inco.1993.1070]
• 20: Robert Harper , John C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.211-252, April 1993 [doi>10.1145/169701.169696]
• 21: Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
• 22: Robert Harper , Greg Morrisett, Compiling Polymorphism Using Intensional Type Analysis, Carnegie Mellon University, Pittsburgh, PA, 1994
• 23: Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
• 24: Fritz Henglein , Jesper Jørgensen, Formally optimal boxing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-226, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177874]
• 25: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 26: M. Jones. Coherence for qualified types. Research Report YALEU/DCS/RR-989, Yale University, New Haven, Connecticut, USA, September 1993.
• 27: M. Jones. Partial evaluation for dictionary-free overloading. In A CM Conference on Partial Evaluation and Semantics- Based Program Manipulation, 1994.
• 28: Mark Philip Jones, Qualified types: theory and practice (ordering relation), 1992
• 29: Simon L. Peyton Jones , John Launchbury, Unboxed values as first class citizens in a non-strict functional language, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.636-666, June 1991, Cambridge, Massachusetts, United States
• 30: 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]
• 31: P. Martin-LSf. About models for intuitionistic type theories and the notion of definitional equality. In S. Kanger, editor, Proceedings of the Third Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics, pages 81-109. North-Holland, 1975.
• 32: R. Milner. A theory of type polymorphism in programming languages. Journal of Computer and System Sciences, 17:348-375, 1978.
• 33: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 34: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• 35: 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]
• 36: G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In preparation, Oct. 1994.
• 37: R. Morrison , A. Dearle , R. C. H. Connor , A. L. Brown, An ad hoc approach to the implementation of polymorphism, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.3, p.342-371, July 1991 [doi>10.1145/117009.117017]
• 38: Atsushi Ohori, A compilation method for ML-style polymorphic record calculi, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-165, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143200]
• 39: Atsushi Ohori , Kazuhiko Kato, Semantics for communication primitives in a polymorphic language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.99-112, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158529]
• 40: G. Plotkin. Lambda-definabiIity in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 363-373. Academic Press, 1980.
• 41: E. R. Poulsen. Representation analysis for efficient implementation of polymorphism. Technical report, Department of Computer Science (DIKU), University of Copenhagen, Apr. 1993. Master Dissertation.
• 42: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 43: Zhong Shao, Compiling standard ML for efficient execution on modern machines, Princeton University, Princeton, NJ, 1994
• 44: Brian Cantwell Smith, Reflection and semantics in LISP, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-35, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800513]
• 45: R. Statman. Completeness, invariance, and lambdadefinability. Journal o/ Symbolic Logic, 47:17-26, 1982.
• 46: R. Statman. Logical relations and the typed .k-calculus. In. formation and Control, 65:85-97, 1985.
• 47: S. Stenlund. Combinators, )#-terms and Proof Theory. D. Reidel, 1972.
• 48: W.W. Tait. Intensional interpretation of functionals of finite type. Journal o/Symbolic Logic, 32(2):187-199, June 1967.
• 49: Satish Thatte, Quasi-static typing, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-381, December 1989, San Francisco, California, United States [doi>10.1145/96709.96747]
• 50: Satish R. Thatté, Semantics of type classes revisited, Proceedings of the 1994 ACM conference on LISP and functional programming, p.208-219, June 27-29, 1994, Orlando, Florida, United States
• 51: 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
• 52: A. K. Wright. Polymorphism for imperative languages without imperative types. Technical Report TR93-200, Department of Computer Science, Rice University, Houston, TX, Feb. 1993. To appear, Lisp and Symbolic Computation.
• 53: Andrew K. Wright , Robert Cartwright, A practical soft type system for Scheme, Proceedings of the 1994 ACM conference on LISP and functional programming, p.250-262, June 27-29, 1994, Orlando, Florida, United States

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.2 Language Classifications

          Nouns: ML
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Languages