Strictly capturing non-strict closures

ABSTRACTAll functional languages need closures. Closure-conversion is a compiler transformation that embeds static code into the program for creating and manipulating closures, avoiding the need for special run-time closure support. For call-by-value languages, closure-conversion has been the focus of extensive studies concerning correctness, such as type preservation and contextual equivalence, and performance, such as space usage. Unfortunately, non-strict languages have been neglected in these studies. This paper aims to fill this gap. We begin with both a call-by-name and a call-by-need source language whose semantics automatically generates closures at run-time. Next, we give type-preserving closure-conversions for these two non-strict languages into a lower-level target language without automatic closure generation at run-time. Despite the fact that our source languages are non-strict, we show that closures must be created eagerly, which requires a strict notion of product in the target language. We extend logical relation techniques used to prove compiler correctness for call-by-value languages, to apply to non-strict languages too. In doing so, we identify some important properties for reasoning about memoization with a heap.