skip to main content
10.1145/199448.199475acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article
Free access

Compiling polymorphism using intensional type analysis

Published: 25 January 1995 Publication History

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, 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.
[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}.
[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.
[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]
A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992.
[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.
[7]
V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172-22l, 1991.
[8]
L. Cardelli. Phase distinctions in type theory. Unpublished manuscript.
[9]
L. Cardelli. Typeful programming. Technical Report 45, DEC Systems Research Center, 1989.
[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.
[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.
[12]
R. L. Constable. Intensional analysis of functions and types. Technical Report CSR-t18-82, Computer Science Department, University of Edinburgh, June 1982.
[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.
[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]
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.
[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}.).
[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.
[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).
[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.
[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.
[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.
[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]
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].
[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.
[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.
[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]
R. Milner, M. Torte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.
[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.
[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.
[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, 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.
[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.
[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.
[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]
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.
[43]
Z. Shao. Compiling Standard ML for Efficient Execution on Modern Machines. PhD thesis, Princeton University, Princeton, NJ, November 1994.
[44]
B. C. Smith. Reflection and semantics in LISP. In Eleventh A CM Symposium on Principles of Programming Languages, pages 23-35, 1984.
[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]
S. R. Thatte. Quasi-static typing. In Seventeenth A CM Symposium on Principles of Programming Languages, pages 367-381, San Francisco, CA, Jan. 1990.
[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.
[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.
[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]
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.

Cited By

View all
  • (2024)Double-Ended Bit-Stealing for Algebraic Data TypesProceedings of the ACM on Programming Languages10.1145/36746288:ICFP(88-120)Online publication date: 15-Aug-2024
  • (2024)SoD2: Statically Optimizing Dynamic Deep Neural Network ExecutionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624869(386-400)Online publication date: 27-Apr-2024
  • (2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 1995
415 pages
ISBN:0897916921
DOI:10.1145/199448
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 1995

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

POPL95
POPL95: 22nd ACM Symposium on Principles of Programming Languages
January 23 - 25, 1995
California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)149
  • Downloads (Last 6 weeks)20
Reflects downloads up to 10 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Double-Ended Bit-Stealing for Algebraic Data TypesProceedings of the ACM on Programming Languages10.1145/36746288:ICFP(88-120)Online publication date: 15-Aug-2024
  • (2024)SoD2: Statically Optimizing Dynamic Deep Neural Network ExecutionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624869(386-400)Online publication date: 27-Apr-2024
  • (2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
  • (2022)Type-level programming with match typesProceedings of the ACM on Programming Languages10.1145/34986986:POPL(1-24)Online publication date: 12-Jan-2022
  • (2021)A Typed Slicing Compilation of the Polymorphic RPC calculusProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479406(1-15)Online publication date: 6-Sep-2021
  • (2020)MorphStoreProceedings of the VLDB Endowment10.14778/3407790.340783313:12(2396-2410)Online publication date: 14-Sep-2020
  • (2020)AriaProceedings of the VLDB Endowment10.14778/3407790.340780813:12(2047-2060)Online publication date: 14-Sep-2020
  • (2020)LeaperProceedings of the VLDB Endowment10.14778/3407790.340780313:12(1976-1989)Online publication date: 1-Jul-2020
  • (2020)A polymorphic RPC calculusScience of Computer Programming10.1016/j.scico.2020.102499197(102499)Online publication date: Oct-2020
  • (2019)A role for dependent types in HaskellProceedings of the ACM on Programming Languages10.1145/33417053:ICFP(1-29)Online publication date: 26-Jul-2019
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media