Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs

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 au-tomatic 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 un-evaluated 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 ap-proach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementa-tion of our analysis. 1