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 automatic
amortisation approach developed by Jost and Hofmann, 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 analyed using a
prototype implementation of our analysis.