Selective Memoization

TL;DR

This paper introduces techniques for selective memoization in functional programming, allowing programmers to control dependencies and space, with an efficient implementation and formal correctness guarantees.

Contribution

It presents a novel approach to selective memoization using a modal type system in MFL, with an SML implementation that ensures correctness through runtime checks.

Findings

Efficient implementation of selective memoization.

Formal proof of soundness for MFL semantics.

Practical SML library supporting controlled memoization.

Abstract

This paper presents language techniques for applying memoization selectively. The techniques provide programmer control over equality, space usage, and identification of precise dependences so that memoization can be applied according to the needs of an application. Two key properties of the approach are that it accepts and efficient implementation and yields programs whose performance can be analyzed using standard analysis techniques. We describe our approach in the context of a functional language called MFL and an implementation as a Standard ML library. The MFL language employs a modal type system to enable the programmer to express programs that reveal their true data dependences when executed. We prove that the MFL language is sound by showing that that MFL programs yield the same result as they would with respect to a standard, non-memoizing semantics. The SML implementation cannot support the modal type system of MFL statically but instead employs run-time checks to ensure correct usage of primitives.