research-article

Sharing-aware improvements in a call-by-need functional core language

Authors:

Manfred Schmidt-Schauß,

David SabelAuthors Info & Claims

IFL '15: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages

Article No.: 6, Pages 1 - 12

https://doi.org/10.1145/2897336.2897343

Published: 14 September 2015 Publication History

Abstract

Based on recent work on program improvements in call-by-need lambda calculi, this paper investigates improvements in a call-by-need polymorphically typed lambda-calculus with letrec, case, constructors, and seq. The goal is to contribute to the foundations and practice of safe optimizations in lazy functional programming languages. We introduce a novel notion of work-decorations which are sensitive for shared work between several subexpressions. Based on this notion computation rules for decorations are developed. Inductive and co-inductive proof tools are introduced for improvement transformations and are illustrated by several examples including fold-variants.

References

[1]

R. Bird. Thinking functionally with Haskell. Cambridge University Press, 2014.

[2]

R. Bird and P. Wadler. Introduction to functional programming. Prentice Hall International series in computer science. Prentice Hall, 1988.

Digital Library

[3]

J. Gibbons and G. Hutton. Proof methods for corecursive programs. Fundam. Inform., 66(4):353--366, 2005.

Digital Library

[4]

J. Hackett and G. Hutton. Worker/wrapper/makes it/faster. In ICFP 2014, pp. 95--107. ACM, 2014.

Digital Library

[5]

J. Hughes. Why functional programming matters. Comput. J., 32(2):98--107, 1989.

Digital Library

[6]

P. Johann and J. Voigtländer. The impact of seq on free theorems-based program transformations. Fundamenta Informaticae, 69(1-2):63--102, 2006.

Digital Library

[7]

A. Kutzner and M. Schmidt-Schauß. A nondeterministic call-by-need lambda calculus. In ICFP 1998, pp. 324--335. ACM, 1998.

Digital Library

[8]

S. Marlow, editor. Haskell 2010 -- Language Report. 2010.

[9]

A. Moran and D. Sands. Improvement in a lazy context: An operational theory for call-by-need. In POPL 1999, pp. 43--56. ACM, 1999.

Digital Library

[10]

S. Peyton Jones and S. Marlow. Secrets of the Glasgow Haskell Compiler inliner. Journal of Functional Programming, 12(4+5):393--434, 2002.

Digital Library

[11]

B. C. Pierce. Types and Programming Languages. The MIT Press, 2002.

Digital Library

[12]

A. M. Pitts. Parametric polymorphism and operational equivalence. Math. Structures Comput. Sci., 10:321--359, 2000.

Digital Library

[13]

D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501--553, 2008.

Digital Library

[14]

M. Schmidt-Schauß. Correctness of copy in calculi with letrec. In RTA 2007, LNCS 4533, pp. 329--343. Springer, 2007.

Digital Library

[15]

M. Schmidt-Schauß, E. Machkasova, and D. Sabel. Extending Abramsky's lazy lambda calculus: (non)-conservativity of embeddings. In RTA 2013, LIPIcs 21, pp. 239--254. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2013.

[16]

M. Schmidt-Schauß and D. Sabel. On generic context lemmas for higher-order calculi with sharing. Theoret. Comput. Sci., 411(11-13):1521--1541, 2010.

Digital Library

[17]

M. Schmidt-Schauß and D. Sabel. Contextual equivalences in call-by-need and call-by-name polymorphically typed calculi (preliminary report). In WPTE 2014, OASICS 40, pp. 63--74. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.

[18]

M. Schmidt-Schauß and D. Sabel. Improvements in a functional core language with call-by-need operational semantics. In PPDP 2015, pp. 220--231. ACM, 2015.

Digital Library

[19]

M. Schmidt-Schauß and D. Sabel. Improvements in a functional core language with call-by-need operational semantics. Frank report 55, Institut für Informatik, Goethe-Universität Frankfurt am Main, 2015. http://www.ki.cs.uni-frankfurt.de/papers/frank.

[20]

M. Schmidt-Schauß and D. Sabel. Shared work decorations for reasoning on improvements in an extended call-by-need lambda calculus. Frank report 56, Institut für Informatik, Goethe-Universität Frankfurt am Main, 2016. http://www.ki.cs.uni-frankfurt.de/papers/frank.

[21]

M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Log. Methods Comput. Sci., 11(1), 2015.

[22]

M. Schmidt-Schauß, Marko Schütz, and D. Sabel. Safety of Nöcker's strictness analysis. J. Funct. Programming, 18(04):503--551, 2008.

Digital Library

[23]

N. Sculthorpe, A. Farmer, and A. Gill. The HERMIT in the tree - mechanizing program transformations in the GHC core language. In IFL 2012, LNCS 8241, pp. 86--103. Springer, Heidelberg, 2012.

[24]

P. Sestoft. Deriving a lazy abstract machine. J. Funct. Programming, 7(3):231--264, 1997.

Digital Library

[25]

D. Vytiniotis and S. Peyton Jones. Evidence Normalization in System FC (Invited Talk). In RTA 2013, LIPIcs 21, pp. 20--38. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2013.

Cited By

Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Schmidt-Schauß MSabel DDallmeyer NSabel DThiemann P(2018)Sequential and Parallel Improvements in a Concurrent Functional Programming LanguageProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236952(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236952
Dallmeyer NSchmidt-Schauss M(2017)An Environment for Analyzing Space Optimizations in Call-by-Need Functional LanguagesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.235.6235(78-92)Online publication date: 1-Jan-2017
https://doi.org/10.4204/EPTCS.235.6

Index Terms

Sharing-aware improvements in a call-by-need functional core language
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Improvements in a functional core language with call-by-need operational semantics
PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming

An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is not increased in any context. This paper investigates improvements an untyped call-by-...
The call-by-need lambda calculus, revisited
ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

The existing call-by-need λ describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the ...
Classical call-by-need and duality
TLCA'11: Proceedings of the 10th international conference on Typed lambda calculi and applications

We study call-by-need from the point of view of the duality between call-by-name and call-by-value. We develop sequent-calculus style versions of call-by-need both in the minimal and classical case. As a result, we obtain a natural extension of call-by-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

IFL '15: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages

September 2015

140 pages

ISBN:9781450342735

DOI:10.1145/2897336

Program Chair:
Ralf Lämmel
University of Koblenz-Landau, Germany

Copyright © 2015 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 September 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

IFL '15

IFL '15: Symposium on the implementation and application of functional programming languages

September 14 - 16, 2015

Koblenz, Germany

Acceptance Rates

Overall Acceptance Rate 19 of 36 submissions, 53%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
59
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Schmidt-Schauß MSabel DDallmeyer NSabel DThiemann P(2018)Sequential and Parallel Improvements in a Concurrent Functional Programming LanguageProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236952(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236952
Dallmeyer NSchmidt-Schauss M(2017)An Environment for Analyzing Space Optimizations in Call-by-Need Functional LanguagesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.235.6235(78-92)Online publication date: 1-Jan-2017
https://doi.org/10.4204/EPTCS.235.6

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents