Hugo Simões
Kevin Hammond
ABSTRACT
This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this paper, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of lazy potential. We present our analysis as a proof system for predicting heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury's natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis.
- E. Albert, J. Silva, and G. Vidal. Time Equations for Lazy Functional (Logic) Languages. In Proc. AGP-2003: 2003 Joint Conf. on Declarative Prog., Reggio Calabria, Italy, Sept. 3-5, 2003, pages 13--24, 2003.Google Scholar
- E. Albert, S. Genaim, and M. Gómez-Zamalloa. Live Heap Space Analysis for Languages with Garbage Collection. In Proc. ISMM 2009: Intl. Symp. on Memory Management, pages 129--138, Dublin, Ireland, June 2009. ACM. ISBN 978-1-60558-347-1. Google ScholarDigital Library
- E. Albert, S. Genaim, and M. Gómez-Zamalloa. Parametric Inference of Memory Requirements for Garbage Collected Languages. In Proc. 2010 International Symposium on Memory Management, ISMM '10, pages 121--130, New York, NY, USA, 2010. ACM. Google ScholarDigital Library
- Z. M. Ariola and M. Felleisen. The Call-by-Need Lambda Calculus. J. Funct. Program., 7:265--301, May 1997. Google ScholarDigital Library
- A. Bakewell and C. Runciman. A Model for Comparing the Space Usage of Lazy Evaluators. In Proc. PPDP 2000: Intl. Conf. on Principles and Practice of Declarative Prog., Quebec, Canada, pages 151--162, 2000. Google ScholarDigital Library
- A. Bakewell and C. Runciman. A Space Semantics for Core Haskell. Electr. Notes Theor. Comput. Sci., 41(1), 2000.Google Scholar
- B. Bjerner and S. Holmström. A Compositional Approach to Time Analysis of First Order Lazy Functional Programs. In Proc. FPCA '89: Conf. on Functional Prog. Langs. and Comp. Arch., pages 157--165, 1989. Google ScholarDigital Library
- V. Braberman, F. Fernández, D. Garbervetsky, and S. Yovine. Parametric Prediction of Heap Memory Requirements. In Proc. ISMM 2008: Intl. Symp. on Memory Management, pages 141--150, New York, NY, USA, June 2008. Google ScholarDigital Library
- B. Campbell. Amortised Memory Analysis Using the Depth of Data Structures. In G. Castagna, editor, Proc. ESOP 2009: 18th European Symposium on Programming, York, UK, pages 190--204. Springer LNCS 5502, 2009. Google ScholarDigital Library
- W.-N. Chin, H. Nguyen, C. Popeea, and S. Qin. Analysing Memory Resource Bounds for Low-Level Programs. In Proc. ISMM'08: Intl. Symp. on Memory Management, pages 151--160, Tucson, USA, June 2008. ACM. ISBN 978-1-60558-134-7. Google ScholarDigital Library
- K. Crary and S. Weirich. Resource Bound Certification. In Proc. POPL 2000: ACM Symp. on Principles of Prog. Langs., pages 184--198, Jan. 2000. Google ScholarDigital Library
- N. A. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proc. POPL 2008: Symp. on Principles of Prog. Langs., San Francisco, USA, January 7-12, 2008, pages 133--144. ACM, 2008. Google ScholarDigital Library
- A. de la Encina and R. Peña-Marí. Proving the Correctness of the STG Machine. In Proc. IFL '01: Impl. of Functional Langs., Stockholm, Sweden, Sept. 24-26, 2001, pages 88--104. Springer LNCS 2312, 2002. Google ScholarDigital Library
- A. de la Encina and R. Peña-Marí. Formally Deriving an STG Machine. In Proc. 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 102--112. ACM, 2003. Google ScholarDigital Library
- A. de la Encina and R. Peña-Marí. From Natural Semantics to C: a Formal Derivation of two STG Machines. J. Funct. Program., 19(1): 47--94, 2009. Google ScholarDigital Library
- P. Fradet and D. L. Métayer. Compilation of functional languages by program transformation. ACM Transactions on Programming Languages and Systems, 13(1):21--51, January 1991. Google ScholarDigital Library
- J. Gustavsson and D. Sands. A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science, 26, 1999.Google Scholar
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. In 38th Symp. on Principles of Prog. Langs. (POPL'11), pages 357--370, 2011. Google ScholarDigital Library
- M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Proc. POPL 2003: ACM Symp. on Principles of Prog. Langs., pages 185--197, Jan. 2003. Google ScholarDigital Library
- M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis (for an Object-Oriented Language). In Proc. ESOP '06: European Symposium on Prog., pages 22--37, Mar. 2006. Google ScholarDigital Library
- M. Hofmann and D. Rodriguez. Efficient type-checking for amortised heap-space analysis. In Proc. CSL '09: 18th EACSL Annual Conf. on Computer Science Logic, pages 317--331, 2009. Google ScholarDigital Library
- C. Hope. A Functional Semantics for Space and Time. PhD thesis, 2008. University of Nottingham.Google Scholar
- R. Hughes. Why Functional Programming Matters. The Computer Journal, 32(2):98--107, 1989. Google ScholarDigital Library
- S. L. P. Jones. Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine. J. Funct. Program., 2 (2):127--202, 1992.Google ScholarCross Ref
- M. B. Josephs. The semantics of lazy functional languages. Theor. Comput. Sci., 68(1):105--111, 1989. Google ScholarDigital Library
- S. Jost. Static Prediction of Dynamic Space Usage of Linear Functional Programs, Dipl. Thesis, Darmstadt Univ. of Tech., 2002.Google Scholar
- S. Jost. Automated Amortised Analysis. PhD thesis, LMU Munich.Google Scholar
- S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. 'Carbon Credits' for Resource-Bounded Computations Using Amortised Analysis. In Proc. FM 2009: Intl. Conf. on Formal Methods, pages 354--369. Springer LNCS 5850, 2009. Google ScholarDigital Library
- S. Jost, H.-W. Loidl, K. Hammond, and M. Hofmann. Static determination of quantitative resource usage for higher-order programs. In Proc. POPL 2010: ACM Symp. on Principles of Prog. Langs.,Madrid, Spain, pages 223--236, Jan. 2010. Google ScholarDigital Library
- J. Launchbury. A Natural Semantics for Lazy Evaluation. In Proc. POPL '93: Symp. on Princ. of Prog. Langs., pages 144--154, 1993. Google ScholarDigital Library
- J. Maraist, M. Odersky, and P. Wadler. The Call-by-Need Lambda Calculus. J. Funct. Program., 8:275--317, May 1998. Google ScholarDigital Library
- R. Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Induction Types. PhD thesis, LMU Munich, 1998.Google Scholar
- A. Moran and D. Sands. Improvement in a Lazy Context: An Operational Theory for Call-by-Need. In POPL, pages 43--56, 1999. Google ScholarDigital Library
- J. Mountjoy. The Spineless Tagless G-machine, naturally. In Proc. ICFP '98: Intl. Conf. on Functional Prog., pages 163--173, 1998. Google ScholarDigital Library
- C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google ScholarCross Ref
- S. Peyton Jones (ed.), L. Augustsson, B. Boutel, F. Burton, J. Fasel, A. Gordon, K. Hammond, R. Hughes, P. Hudak, T. Johnsson, M. Jones, J. Peterson, A. Reid, and P. Wadler. Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report, Yale University, 1999.Google Scholar
- D. Sands. Complexity Analysis for a Lazy Higher-Order Language. In Proc. ESOP '90: European Symposium on Programming, Copenhagen, Denmark, Springer LNCS 432, pages 361--376, 1990. Google ScholarDigital Library
- D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, University of London, September 1990.Google Scholar
- D. Sands. Computing with Contexts: A Simple Approach. In Proc. HOOTS II: Higher-Order Operational Techniques in Semantics, Electr. Notes in Theoretical Comp. Sci. 1998.Google ScholarDigital Library
- P. Sestoft. Deriving a Lazy Abstract Machine. J. Functional Programming, 7(3):231--264, 1997. Google ScholarDigital Library
- O. Shkaravska, R. van Kesteren, and M. van Eekelen. Polynomial Size Analysis of First-Order Functions. In Proc. TLCA 2007: Typed Lambda Calculi and Applications (TLCA 2007), pages 351--365, Paris, France, June 26-28, June 2007. Springer LNCS 4583. Google ScholarDigital Library
- R. E. Tarjan. Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306--318, April 1985.Google ScholarDigital Library
- P. B. Vasconcelos. Space Cost Analysis Using Sized Types. PhD thesis, University of St Andrews, 2008.Google Scholar
- P. B. Vasconcelos and K. Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In Proc. IFL '03: Impl. of Functional Languages, pages 86--101, Edinburgh, UK, 2004. Springer LNCS 3145. Google ScholarDigital Library
- P.Wadler. Strictness Analysis aids Time Analysis. In Proc. POPL '88: ACM Symp. on Princ. of Prog. Langs., pages 119--132, 1988. Google ScholarDigital Library
- P. Wadler. The Essence of Functional Programming. In Proc. POPL '92: ACM Symp. on Principles of Prog. Langs., pages 1--14, Jan. 1992. Google ScholarDigital Library
- P. Wadler and J. Hughes. Projections for Strictness Analysis. In Proc. FPCA'87: Intl. Conf. on Functional Prog. Langs. and Comp. Arch., Springer LNCS 274, pages 385--407, Sept. 1987. Google ScholarDigital Library
Index Terms
- Automatic amortised analysis of dynamic memory allocation for lazy functional programs
Recommendations
Automatic amortised analysis of dynamic memory allocation for lazy functional programs
ICFP '12This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and ...
Resource Analysis for Lazy Evaluation with Polynomial Potential
IFL '20: Proceedings of the 32nd Symposium on Implementation and Application of Functional LanguagesSpace and time requirements of lazy functional programs are hard to predict for both programmers and compilers. Previous work in compile-time amortised analyses for lazy functional languages by Simões, Jost et.al. was limited to bounds that are linear ...
A Lazy Language Needs a Lazy Type System: Introducing Polymorphic Contexts
IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming LanguagesMost type systems that support polymorphic functions are based on a version of System-F. We argue that this limits useful programming paradigms for languages with lazy evaluation. We motivate an extension of System-F alleviating this limitation.
First, ...
Comments