Strictness analysis

In computer science, strictness analysis refers to any algorithm used to prove that a function in a non-strict functional programming language is strict in one or more of its arguments. This information is useful to compilers because strict functions can be compiled more efficiently. Thus, if a function is proven to be strict (using strictness analysis) at compile time, it can be compiled to use a more efficient calling convention without changing the meaning of the enclosing program.

Note that a function f is said to diverge if it returns ${\displaystyle \{\bot \}}$: operationally, that would mean that f either causes abnormal termination of the enclosing program (e.g., failure with an error message) or that it loops infinitely. The notion of "divergence" is significant because a strict function is one that always diverges when given an argument that diverges, whereas a lazy (or non-strict) function is one that may or may not diverge when given such an argument. Strictness analysis attempts to determine the "divergence properties" of functions, which thus identifies some functions that are strict.

Approaches to strictness analysis

Forward abstract interpretation

Strictness analysis can be characterized as a forward abstract interpretation which approximates each function in the program by a function that maps divergence properties of the arguments onto divergence properties of the results. In the classical approach pioneered by Alan Mycroft, the abstract interpretation used a two-point domain with 0 denoting the set ${\displaystyle \{\bot \}}$ considered as a subset of the argument or return type, and 1 denoting all values in the type.[1]

Demand analysis

The Glasgow Haskell Compiler (GHC) uses a backward abstract interpretation known as demand analysis to perform strictness analysis as well as other program analyses. In demand analysis, each function is modelled by a function from value demands on the result to value demands on the arguments. A function is strict in an argument if a demand for its result leads to a demand for that argument.[2]

Projection-based strictness analysis

Projection-based strictness analysis, introduced by Philip Wadler and R.J.M. Hughes, uses strictness projections to model more subtle forms of strictness, such as head-strictness in a list argument. (By contrast, GHC's demand analysis can only model strictness within product types, i.e., datatypes that only have a single constructor.) A function ${\displaystyle f}$ is considered head-strict if ${\displaystyle f=f\circ \pi }$, where ${\displaystyle \pi }$ is the projection that head-evaluates its list argument.[3]

There was a large body of research on strictness analysis in the 1980s.

References

1. Mycroft, Alan (1980). "The theory and practice of transforming call-by-need into call-by-value". Lecture Notes in Computer Science: Proc. 4th Intl. Symp. on Programming, Vol. 83. Springer-Verlag.
2. "The GHC Commentary: Demand analyser in GHC". Retrieved 2014-02-12.
3. Wadler, P.; R.J.M. Hughes (1987). "Projections for strictness analysis". Functional programming and computer architecture; LNCS 274. Springer-Verlag.