More Web Proxy on the site http://driver.im/

Article

Free access

On the runtime complexity of type-directed unboxing

Authors:

Yasuhiko Minamide,

Jacques GarrigueAuthors Info & Claims

ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

Pages 1 - 12

https://doi.org/10.1145/289423.289424

Published: 29 September 1998 Publication History

Abstract

Avoiding boxing when representing native objects is essential for the efficient compilation of any programming language For polymorphic languages this task is difficult, but several schemes have been proposed that remove boxing on the basis of type information. Leroy's type-directed unboxing transformation is one of them. One of its nicest properties is that it relies only on visible types, which makes it compatible with separate compilation. However it has been noticed that it is not safe both in terms of time and space complexity ---i.e. transforming a program may raise its complexity. We propose a refinement of this transformation, still relying only on visible types, and prove that it satisfies the safety condition for time complexity. The proof is an extension of the usual logical relation method, in which correctness and safety are proved simultaneously.

References

[1]

A. W. Appel. Compiling with Continuation. Cambridge University Press, 1992.

Digital Library

[2]

G. E. Blelloch ~md J. Greincr. A provably time and space etIicient implement~~tion of NESL. In Proc. A CM SIGPLAN International Conference on Functional Programming, pages 213--225, 1996.

Digital Library

[3]

D. Clement, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ML. In Proc. ACM Conference on Lisp and t;}znctional Programming, pages 13 --- 27, 1986.

Digital Library

[4]

J. Goubault. Generalized unboxing, congruences and partial inlining, in Proc. Static Analysis Symposium, pages 147-16{, 1994.

[5]

J. Greiner and G. E. Blelloch. A provably time-efficient parallel implementation of full speculation. In Proc. A CM Symposium on Principles of Programming Languages, pages 309 - 321, 1996.

Digital Library

[6]

R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proc. ACM Symposium on Principles of Programming Languages, pages t30-141, 1995.

Digital Library

[7]

F. Henglein and J. Jorgensen. Formally optimal boxing. In Proc. A CM Symposium on Principles of Programming Languages, pages 213- 226, 1994.

Digital Library

[8]

X. Leroy. Unboxed objects and polymorphic typing. In Proc. A CM Symposium on Principles of Programming Languages, pages 177 .. 188, 1992.

Digital Library

[9]

X. Leroy. The effectiveness of type-based unboxing. In Proc. International Workshop on Types in Compilation, pages 1-8, 1997.

Digital Library

[10]

R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, {7:348-375, 1978.

[11]

Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proc. A CM Symposium on Principles of Programming Languages, pages 271 - 283, 1996.

Digital Library

[12]

CI. Morrisett. Compiling with Types. PhD thesis, School ~)f Computer Science Carnegie Mellon University, 1995.

[13]

G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In Proc. A CM Symposium on l~nctional Programming Languages and Cornputer Architecture, pages 66-77, 1995.

Digital Library

[14]

A. Ohori. A polymorphic record calculus and its compilation. A CM Transaction on Programming Languages and Systems, 17(6):844-895, 1995.

Digital Library

[15]

A. Ohori and T. Takamizawa. An unboxed operational semantics for ML polymorphisln. Journal of Lisp and Symbolic Computation, 10(1):61 -- 91, 1997.

Digital Library

[16]

S. L. Peyton Jones and J. Launchbury. Unboxed values as first class citizens in a non-strict functional language. In Proc. A CM Symposium on Functional Programming Languages and Computer' Architecture, pages 636--666, 1991.

Digital Library

[17]

P. Roe. Parallel Programming using Functional Languages. PhD thesis, Department of Computing Science, University of Glasgow, 1991.

[18]

A. L. Santos. Compilation by Transformation in Nonstrsct Functional Languages. PhD thesis, Department of Computing Science, University of Glasgow, 1995.

[19]

Z. Shao. Flexible representation analysis. In Proc. A CM $IGPLAN International Conference on Functional Programming, pages 85 - 98, 1997.

Digital Library

[20]

Z. Shao and A. W. Appel. A type-based compiler for Standard ML. In Proc. A CM SIGPLAN Conference on Programming Language Design and Implementation, pages 116 - 129, 1995.

Digital Library

[21]

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In Proc. A CM SlGPLAN Conference on Programming Language Design and Implementation, pages 181-192, 1996.

Digital Library

[22]

P. Thiemann. Polymorphic typing and unboxed values revisited. In Proc. A CM Symposium on Functional Programming Languages and Computer Architecture, pages 24- 35, 1995.

Digital Library

Cited By

Monnier SShao Z(2019)Inlining as staged computationJournal of Functional Programming10.1017/S095679680200461613:3(647-676)Online publication date: 19-Nov-2019
https://dl.acm.org/doi/10.1017/S0956796802004616
Ziarek LWeeks SJagannathan S(2018)Flattening tuples in an SSA intermediate representationHigher-Order and Symbolic Computation10.1007/s10990-008-9035-321:3(333-358)Online publication date: 15-Dec-2018
https://dl.acm.org/doi/10.1007/s10990-008-9035-3
Ureche VBurmako EOdersky M(2014)Late data layoutACM SIGPLAN Notices10.1145/2714064.266019749:10(397-416)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2714064.2660197
Show More Cited By

Index Terms

On the runtime complexity of type-directed unboxing
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
2. Theory of computation
  1. Computational complexity and cryptography
    1. Complexity classes

Recommendations

On the runtime complexity of type-directed unboxing

Avoiding boxing when representing native objects is essential for the efficient compilation of any programming language For polymorphic languages this task is difficult, but several schemes have been proposed that remove boxing on the basis of type ...
Type inference with rank 1 polymorphism for type-directed compilation of ML

This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different frdm the conventional ML type discipline, the proposed type system allows full rank 1 ...
Type inference with rank 1 polymorphism for type-directed compilation of ML
ICFP '99: Proceedings of the fourth ACM SIGPLAN international conference on Functional programming

This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different frdm the conventional ML type discipline, the proposed type system allows full rank 1 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

September 1998

351 pages

ISBN:1581130244

DOI:10.1145/289423

Chairmen:
Matthias Felleisen
Rice Univ., Houston, TX
,
Paul Hudak
Yale Univ., New Haven, CT
,
Christian Queinnec
Univ. Paris 6; and INRIA

ACM SIGPLAN Notices Volume 34, Issue 1
Jan. 1999
357 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/291251
Chairmen:
Matthias Felleisen
Rice Univ.
,
Paul Hudak
Yale Univ.
,
Editor:
A. Michael Berman
Issue’s Table of Contents

Copyright © 1998 ACM.

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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 September 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICFP98

Sponsor:

SIGPLAN

ICFP98: 1998 International Conference on Functional Programming

September 26 - 29, 1998

Maryland, Baltimore, USA

Acceptance Rates

ICFP '98 Paper Acceptance Rate 30 of 77 submissions, 39%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
465
Total Downloads

Downloads (Last 12 months)71
Downloads (Last 6 weeks)18

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Monnier SShao Z(2019)Inlining as staged computationJournal of Functional Programming10.1017/S095679680200461613:3(647-676)Online publication date: 19-Nov-2019
https://dl.acm.org/doi/10.1017/S0956796802004616
Ziarek LWeeks SJagannathan S(2018)Flattening tuples in an SSA intermediate representationHigher-Order and Symbolic Computation10.1007/s10990-008-9035-321:3(333-358)Online publication date: 15-Dec-2018
https://dl.acm.org/doi/10.1007/s10990-008-9035-3
Ureche VBurmako EOdersky M(2014)Late data layoutACM SIGPLAN Notices10.1145/2714064.266019749:10(397-416)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2714064.2660197
Ureche VBurmako EOdersky MBlack AMillstein T(2014)Late data layoutProceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications10.1145/2660193.2660197(397-416)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2660193.2660197
Tatsubori MTozawa ASuzumura TTrent SOnodera T(2010)Evaluation of a just-in-time compiler retrofitted for PHPACM SIGPLAN Notices10.1145/1837854.173601545:7(121-132)Online publication date: 17-Mar-2010
https://dl.acm.org/doi/10.1145/1837854.1736015
Tatsubori MTozawa ASuzumura TTrent SOnodera TFiuczynski MBerger EWarfield A(2010)Evaluation of a just-in-time compiler retrofitted for PHPProceedings of the 6th ACM SIGPLAN/SIGOPS international conference on Virtual execution environments10.1145/1735997.1736015(121-132)Online publication date: 17-Mar-2010
https://dl.acm.org/doi/10.1145/1735997.1736015
Minamide Y(2003)Selective tail call eliminationProceedings of the 10th international conference on Static analysis10.5555/1760267.1760280(153-170)Online publication date: 11-Jun-2003
https://dl.acm.org/doi/10.5555/1760267.1760280
Nishimura S(2003)Correctness of a Higher-Order Removal Transformation through a Relational ReasoningProgramming Languages and Systems10.1007/978-3-540-40018-9_24(358-375)Online publication date: 2003
https://doi.org/10.1007/978-3-540-40018-9_24
Minamide Y(2003)Selective Tail Call EliminationStatic Analysis10.1007/3-540-44898-5_9(153-170)Online publication date: 13-May-2003
https://doi.org/10.1007/3-540-44898-5_9
Hasegawa M(2002)Logical Predicates for Intuitionistic Linear Type TheoriesTyped Lambda Calculi and Applications10.1007/3-540-48959-2_15(198-213)Online publication date: 27-May-2002
https://doi.org/10.1007/3-540-48959-2_15
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents