Strictness analysis

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.

: 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.

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

[2] Projection-based strictness analysis, introduced by Philip Wadler and R.J.M.

(By contrast, GHC's demand analysis can only model strictness within product types, i.e., datatypes that only have a single constructor.)