A Foundation for Space-Safe Transformations of Call-by-Need Programs

AbstractWe introduce a space-improvement relation on programs which guarantees that whenever M is improved by N, replacement of M by N in a program can never lead to asymptotically worse space (heap or stack) behaviour, for a particular model of garbage collection. This study takes place in the context of a call-by-need programming language. For languages implemented using call-by-need, e.g., Haskell, space behaviour is notoriously difficult to predict and analyse, and even innocent-looking equivalences like x + y = y + x can change the asymptotic space requirements of some programs. Despite this, we establish a fairly rich collection of improvement laws, with the help of a context lemma for a finer-grained improvement relation. We briefly consider an application of the theory; we prove that inlining of affine-linear bindings (as introduced by a certain class of “used-once” type-systems) is work- and space-safe. We also show that certain weaker type systems for usage do not provide sufficient conditions for space-safe inlining