Selective Memoization with Box Types

Memoization is a useful technique to eliminate computational redundancy. A memo function remembers all the arguments to which it has been applied, together with their corresponding results, by storing them in a table. This table is consulted before each functional call to determine if the particular argument is in it. If so, the call is skipped and the stored result is returned; otherwise the call is performed and its result added to the table. Acar, Belloch and Harper present a framework to apply memoization selectively, that is, enabling the programmer to determine precisely the dependences between the input and the result of a function. This framework is efficient and yields programs whose performance can be analyzed using standard techniques. The language, implemented as an SML library, is based on a modal type system which allows the programmer to reveal the true data input/output dependences in a program. However, the modality seems to be an ad-hoc choice for the implementation. In this paper we develop selective memoization, using instead box types, corresponding to the necessitation modality □. We also include non-memoized functions, and provide full proofs of type safeness and soundness of the dynamic semantics with respect to an effect-free system which is later translated into the very well-known language PCF.