Reasoning about simple and exhaustive demand in higher-order lazy languages

Abstract

In this work we describe an innovative strictness analysis method for reasoning about simple and exhaustive demand in higher-order lazy languages. By reasoning about simple demand, we mean determining whether a function requires its input in head normal form whenever its output is so required, i.e., is the function strict? Similarly, by exhaustive demand we mean determining whether a function requires its input in normal form whenever its output is so required, i.e., is the function fully strict?. Our method, which is based on type inference, supports reasoning about strictness and full-strictness within a unified framework by making essential use of subtypes. In contrast to previous proposals, our method does not require fixpoint iteration and hence should be more amenable to practical use. Furthermore, our method can handle such features as pattern-matching and user-defined datatypes which are important in practical programming. The insight behind our results is that program properties such as strictness can be treated as types possessed by programs. As a consequence, we are able to design an inference algorithm, which given program P constructs a representation for all possible “strictness” types deducible for P. This representation takes the form of a set of constraints. We show that strictness and full-strictness properties of P can be derived, in a precise formal sense, from this set of constraints. We include a systematic comparison between our techniques and results and those of higher-order abstract interpretation.