Article

Free access

Higher-order unCurrying

Authors:

John Hannan,

Patrick HicksAuthors Info & Claims

POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 1 - 11

https://doi.org/10.1145/268946.268947

Published: 21 January 1998 Publication History

PDF eReader

Abstract

We present a formal specification of unCurrying for a higherorder, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions which are passed as arguments or returned as values. The specification also supports partial unCurrying of any consecutive parameters of a function, rather than only unCurrying all of a function's parameters. We present the specification as a deductive system which axiomatizes a judgment relating a source term with an unCurried form of the term. We prove that this system relates only typable terms and that it is correct with respect to an operational semantics. We define a practical algorithm, based on algorithm W, which implements the unCurrying and prove this algorithm sound and complete with respect to the deductive system. This algorithm generates maximally unCurried forms of source terms. These results provide a declarative framework for reasoning about unCurrying and support a richer form of unCurrying than is currently found in compilers for functional languages.

References

[1]

Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

Digital Library

Google Scholar

[2]

Carsten K. Gomard and Peter Sestoft. Globalization and live variables, in Proceedings of ~he Symposium on Partial E~Jaluation and Semantics-Based Program Manipulation, pages 166-177~ 1991.

Digital Library

Google Scholar

[3]

John Ha~nan. Type systems for closure conversions. In Hanne Riis Nielson and Kirs~en Lackner Solberg, editors, Participants' Proceedings of the Workshop on Types for Program Analysis, pages 48-62. Aarhus University, DAIMt PB-493, May 1995.

Google Scholar

[4]

John Hannah. A type-based escape analysis for functional languages. Journal of Functional Programming, September .1997. To appear.

Digital Library

Google Scholar

[5]

John Hannau, Patrick Hicks, and David Libau-Nowell. A lifetime analysis for higher-order languages. Technica{ Report CSE-97-014, Penn State University, September 1997.

Google Scholar

[6]

Robert Harper, Furio Honsell, and Gordon Ploekin. A. framework for defining logics. Journal of the A CM, 40(1):143-184, 1993. A preliminary version appeared in Symposium on Logic in Computer Science, pages 194- 204, June 1987.

Digital Library

Google Scholar

[7]

Xavier Le~oy. The ZINC experiment: An economical implementation of ~he ML language. Technical Repor~ 11I, INRIA, 1990.

Google Scholar

[8]

S. Michaylov and F. Pfenning. Natural semantics and some of i~s meta-theory in Elf. In Lars Haling, editor, Extensions of Logic Programming~ pages 299-344. Springer-Verlag LNCS 596, 1992. A preliminary version is available as Technical Report MPI-I-91-211~ Max- Planck-Insti~ute for Computer Scienee~ Saarbriicken, Germany, Augus~ 1991.

Digital Library

Google Scholar

[9]

Robin Milner. A theory of type polymorphism in programming. Journal of Coml~u~er and System Sciences, 17(3):348-375, 1978.

Crossref

Google Scholar

[10]

Tobia Nipkow and Christian Prehofer. Type reconstruction for ~ype classes. Journal of Functional Pragramruing, 5(2):201-224, April 1995.

Crossref

Google Scholar

[11]

Frank Pfemaing. An implementation of the Elf core language in Standard ML. Available via ftp over ~he Internet, September 1991. Send mail to [email protected] for further information.

Google Scholar

[12]

Frank Pfenning. Logie programming in the LF logical fxamework, in G. Hue~ and G. :Plotkin, editors, Logi. cat Frameworks, pages 149-181. Cambridge University Press, 1991.

Digital Library

Google Scholar

[13]

David Tarditi. Design and Implementation of Code Op. timizations for a Type-Directed Compiler for Standard ML. PhD thesis, Carnegie Mellon University, 1996. Available as CMU CS Technical Repor~ 97-108,

Google Scholar

[14]

David Tarditi, Greg Morrisetti Perry Cheng, Chris Stone, Bob Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In Proceedings of the log6 A GM SIGPLAN Conference or, Programming Lan#uag~ Design and Implementation, pages 181-192, 1996.

Digital Library

Google Scholar

Cited By

View all

Downen PAriola ZPeyton Jones SEisenberg R(2020)Kinds are calling conventionsProceedings of the ACM on Programming Languages10.1145/34089864:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408986
Downen PSullivan ZAriola ZPeyton Jones SEisenberg R(2019)Making a faster Curry with extensional typesProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342594(58-70)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342594
Hannan J(2006)Program analysis in λprologPrinciples of Declarative Programming10.1007/BFb0056625(353-354)Online publication date: 2-Jun-2006
https://doi.org/10.1007/BFb0056625
Show More Cited By

Recommendations

Higher-Order UnCurrying

We present a formal specification of unCurrying for a higher-order, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions that are passed as arguments or returned as ...
A verified framework for higher-order uncurrying optimizations

Function uncurrying is an important optimization for the efficient execution of functional programming languages. This optimization replaces curried functions by uncurried, multiple-argument functions, while preserving the ability to evaluate partial ...
Higher-order abstract syntax in classical higher-order logic
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Higher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1998

403 pages

ISBN:0897919793

DOI:10.1145/268946

Chairmen:
David B. MacQueen
Bell Labs
,
Luca Cardelli
Digital Equipment Corp.

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL98

Sponsor:

POPL98: Symposium on Principles of Programming Languages

January 19 - 21, 1998

California, San Diego, USA

Acceptance Rates

POPL '98 Paper Acceptance Rate 32 of 175 submissions, 18%;

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

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
172
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)15

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Downen PAriola ZPeyton Jones SEisenberg R(2020)Kinds are calling conventionsProceedings of the ACM on Programming Languages10.1145/34089864:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408986
Downen PSullivan ZAriola ZPeyton Jones SEisenberg R(2019)Making a faster Curry with extensional typesProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342594(58-70)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342594
Hannan J(2006)Program analysis in λprologPrinciples of Declarative Programming10.1007/BFb0056625(353-354)Online publication date: 2-Jun-2006
https://doi.org/10.1007/BFb0056625
Choi KOhori A(2004)A Type Theory for Krivine-Style Evaluation and CompilationProgramming Languages and Systems10.1007/978-3-540-30477-7_15(213-228)Online publication date: 2004
https://doi.org/10.1007/978-3-540-30477-7_15
Dimock AWestmacott IMuller RTurbak FWells J(2001)Functioning without closureACM SIGPLAN Notices10.1145/507669.50764036:10(14-25)Online publication date: 1-Oct-2001
https://dl.acm.org/doi/10.1145/507669.507640
Dimock AWestmacott IMuller RTurbak FWells JPierce B(2001)Functioning without closureProceedings of the sixth ACM SIGPLAN international conference on Functional programming10.1145/507635.507640(14-25)Online publication date: 1-Oct-2001
https://dl.acm.org/doi/10.1145/507635.507640
Fischbach AHannan J(2001)Specification and Correctness of Lambda LiftingSemantics, Applications, and Implementation of Program Generation10.1007/3-540-45350-4_10(108-128)Online publication date: 1-Jun-2001
https://doi.org/10.1007/3-540-45350-4_10
Dimock AWestmacott IMuller RTurbak FWells JConsidine J(2001)Program Representation Size in an Intermediate Language with Intersection and Union TypesTypes in Compilation10.1007/3-540-45332-6_2(27-52)Online publication date: 13-Jun-2001
https://doi.org/10.1007/3-540-45332-6_2
Fischbach AHannan J(2001)Type Systems for Useless-Variable EliminationPrograms as Data Objects10.1007/3-540-44978-7_3(25-38)Online publication date: 25-Apr-2001
https://doi.org/10.1007/3-540-44978-7_3
Hannan JHicks P(2000)Higher-Order UnCurryingHigher-Order and Symbolic Computation10.1023/A:101000622954913:3(179-216)Online publication date: 1-Sep-2000
https://dl.acm.org/doi/10.1023/A%3A1010006229549
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

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

Cited By

Index Terms

Recommendations

Higher-Order UnCurrying

A verified framework for higher-order uncurrying optimizations

Higher-order abstract syntax in classical higher-order logic