Resource Analysis for Lazy Evaluation with Polynomial Potential
Sara Moreira, Pedro B. Vasconcelos, Mário Florido · 2020
Space 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 on the sizes of inputs. This paper presents an extension of these analyses with the method of polynomial potential (due to Hofmann and Hoffmann), allowing the system to derive univariate polynomial resource bounds. We present the analysis as a type system for tracking allocations in a simple functional lazy functional language with lists and pairs, an operational semantics (serving as cost model), and worked examples of deriving resource bounds. We also highlight some limitations and conclude with further research directions.