Robert Harper
Greg Morrisett
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.
- 1.M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In Proceedings of the Sixteenth Annual A CM Symposium on Principles of Programmmg Languages, Austin. ACM, January 1989. Google Scholar
Digital Library
- 2.M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. A CM Transactions on Progamming Languages and Systems, 13(2):237-268, Apr. 1991. Revised version of {1}. Google ScholarDigital Library
- 3.A. Aiken, E. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Twenty-First A CM Symposium on Principles of Programming Languages, pages 163-173, Portland, OR, Jan. 1994. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 5.A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992. Google ScholarDigital Library
- 6.G. Blelloch, S. Chatterjee, J. C. Hardwick, J. Sipelstein, and M. Zagha. Implementation of a portable nested data-parallel language. In Proceedings of the Fourth A CM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 102-111, May 1993. Google ScholarDigital Library
- 7.V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172-22l, 1991. Google ScholarDigital Library
- 8.L. Cardelli. Phase distinctions in type theory. Unpublished manuscript.Google Scholar
- 9.L. Cardelli. Typeful programming. Technical Report 45, DEC Systems Research Center, 1989.Google Scholar
- 10.R. Cartwright and M. Fagan. Soft typing. In Proc. SIG- PLAN '91 Conference on Programmzng Language Design and implementation, pages 278-292. ACM, June 1991. Google ScholarDigital Library
- 11.D. C16ment, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ML. In 1986 A CM Conf. on LISP and Functional Prog., 1986. Google ScholarDigital Library
- 12.R. L. Constable. Intensional analysis of functions and types. Technical Report CSR-t18-82, Computer Science Department, University of Edinburgh, June 1982.Google Scholar
- 13.R. L. Constable and D. R. Zlatin. The type theory of PL/CV3. A CM Transactions on Progamming Languages and Systems, 7(1):72-93, Jan. 1984. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 17.J.-Y. Girard. Interprdtation Fonctionnelle et t#limination des Coupures dans I'Arithmdtique d'Ordre Supdrieure. PhD thesis, Universit6 Paris VII, 1972.Google Scholar
- 18.K. Ghdel. Uber eine bisher noch nicht benfitzte Erweiterung des finiten Standpunktes. Dialectica, 12:280-287, 1958.Google ScholarCross Ref
- 19.C. A. Gunter, E. L. Gunter, and D. B. MacQueen. Computing ML equality kinds using abstract interpretation. Information and Computation, 107(2):303-323, Dec. 1993. Google ScholarDigital Library
- 20.R. Harper and J. C. Mitchell. On the type structure of Standard ML. A CM Transactions on Progamming Languages and Systems, 15(2):211-252, April 1993. (See aIso {34}.). Google ScholarDigital Library
- 21.R. Harper, j. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In Seventeenth A CM Symposium on Principles o/ Programming Languages, San Francisco, CA, January 1990. Google ScholarDigital Library
- 22.R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. Technical Report CMU-CS-94- 185, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, September 1994. (Also published as Fox Memorandum CMU-CS-FOX-94-07). Google ScholarDigital Library
- 23.N. Heintze. Set-based analysis of ML programs. In Proc. 1994 A CM Conf. on LISP and Functional Programming, pages 306-317, Orlando, FL, June 1994. ACM. Google ScholarDigital Library
- 24.F. Henglein and J. Jcrgensen. Formally optimal boxing, in Twenty-First A CM Symposium on Principles of Programming Languages, pages 213-226, Portland, OR, Jan. 1994. ACM. Google ScholarDigital Library
- 25.P. Hudak, S. L. P. Jones, and P. Wadler. Report on the programming language Haskell, version 1.2. SIGPLAN Notices, 27(5), May 1992. Google ScholarDigital Library
- 26.M. Jones. Coherence for qualified types. Research Report YALEU/DCS/RR-989, Yale University, New Haven, Connecticut, USA, September 1993.Google Scholar
- 27.M. Jones. Partial evaluation for dictionary-free overloading. In A CM Conference on Partial Evaluation and Semantics- Based Program Manipulation, 1994.Google Scholar
- 28.M.P. Jones. Qualified Types: Theory and Practice. PhD thesis, Programming Research Group, Oxford University Computing Laboratory, July 1992. Currently available as Technical Monograph PRG-106, Oxford University Computing Laboratory, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, U.K. email: [email protected]. Google ScholarDigital Library
- 29.S. P. Jones and J. Launchbury. Unboxed values as firstclass citizens. In Proc. Conf. on Functional Programming and Computer Architecture, volume 523 of Lecture Notes in Computer Science, pages 636-666. ACM, Springer-Verlag, 1991. Google ScholarDigital Library
- 30.X. Leroy. Unboxed objects and polymorphic typing. In Conference Record of the Nineteenth Annual A CM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, Albuquerque, pages 177-188. ACM Press, January 1992. Google ScholarDigital Library
- 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.Google Scholar
- 32.R. Milner. A theory of type polymorphism in programming languages. Journal of Computer and System Sciences, 17:348-375, 1978.Google ScholarCross Ref
- 33.R. Milner, M. Torte, and R. Harper. The Definition of Standard ML. MIT Press, 1990. Google ScholarDigital Library
- 34.J. Mitchell and R. Harper. The essence of ML. In Fifteenth A CM Symposium on Principles of Programming Languages, San Diego, California, Jan. 1988. Google ScholarDigital Library
- 35.J. C. Mitchell and G. Plotkin. Abstract types have existential type. A CM Transactions on Progamming Languages and Systems, 10(3):470-502, 1988. Google ScholarDigital Library
- 36.G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In preparation, Oct. 1994.Google Scholar
- 37.R. Morrison, A. Dearle, R. C. H. Connor, and A. L. Brown. An ad hoc approach to the implementation of polymorphism. A CM Transactions on Progamming Languages and Systems, 13(3):342-371, July 1991. Google ScholarDigital Library
- 38.A. Ohori. A compilation method for ML-style polymorphic record calculi. In Nineteenth A CM Symposium on Principles of Programming Languages, pages 154-165, Albuquerque, NM, Jan. 1992. Association for Computing Machinery. Google ScholarDigital Library
- 39.A. Ohori and K. Kato. Semantics for communication primitives in a polymorphic language. In Twentieth A CM Symposium on Principles of Programming Languages, pages 99- 112, Charleston, SC, Jan. 1993. Association for Computing Machinery. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 42.J. C. Reynolds. Towards a theory of type structure. In Colloq. sur la Programmation, volume 19 of Lecture Notes in Computer Science, pages 408-423. Springer-Verlag, 1974. Google ScholarDigital Library
- 43.Z. Shao. Compiling Standard ML for Efficient Execution on Modern Machines. PhD thesis, Princeton University, Princeton, NJ, November 1994. Google ScholarDigital Library
- 44.B. C. Smith. Reflection and semantics in LISP. In Eleventh A CM Symposium on Principles of Programming Languages, pages 23-35, 1984. Google ScholarDigital Library
- 45.R. Statman. Completeness, invariance, and lambdadefinability. Journal o/ Symbolic Logic, 47:17-26, 1982.Google Scholar
- 46.R. Statman. Logical relations and the typed .k-calculus. In. formation and Control, 65:85-97, 1985.Google Scholar
- 47.S. Stenlund. Combinators, )#-terms and Proof Theory. D. Reidel, 1972.Google Scholar
- 48.W.W. Tait. Intensional interpretation of functionals of finite type. Journal o/Symbolic Logic, 32(2):187-199, June 1967.Google Scholar
- 49.S. R. Thatte. Quasi-static typing. In Seventeenth A CM Symposium on Principles of Programming Languages, pages 367-381, San Francisco, CA, Jan. 1990. Google ScholarDigital Library
- 50.S. R. Thatte. Semantics of type classes revisited. In Proc. 1994 A CM Conference on LISP and Functional Programming, pages 208-219, Orlando, June 1994. ACM. Google ScholarDigital Library
- 51.A. Tolmach. Tag-free garbage collection using explicit type parameters. In Proc. 1994 A CM Conference on LISP and Functional Programming, pages 1-11, Orlando, FL, June 1994. ACM. Google ScholarDigital Library
- 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.Google Scholar
- 53.A.K. Wright and R. Cartwright. A practical soft type system for Scheme. In Proc 1994 A CM Conference on LISP and Functional Programming, pages 250-262, Orlando, FL, June 1994. ACM. Google ScholarDigital Library
Index Terms
- Compiling polymorphism using intensional type analysis
Recommendations
Intensional polymorphism in type-erasure semantics
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, ...
Intensional polymorphism in type-erasure semantics
ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programmingIntensional 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, ...
Comments