Strictness analysis
Encyclopedia
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 compiler
s 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
: operationally, that would mean that
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
considered as a subset of the argument or return type, and 1 denoting all values in the type.
(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.
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
is considered head-strict if 
, where 
is the projection that head-evaluates its list argument.
There was a large body of research on strictness analysis in the 1980s.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, strictness analysis refers to any algorithm used to prove that a function in a non-strict functional programming
Functional programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
language is strict
Strict function
A strict function in the denotational semantics of programming languages is a function f where f\left = \perp. The entity \perp, called bottom, denotes an expression which does not return a normal value, either because it loops endlessly or because it aborts due to an error such as division by...
in one or more of its arguments. This information is useful to compiler
Compiler
A compiler is a computer program that transforms source code written in a programming language into another computer language...
s 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
Calling convention
In computer science, a calling convention is a scheme for how subroutines receive parameters from their caller and how they return a result; calling conventions can differ in:...
without changing the meaning of the enclosing program.
Note that a function
f is said to diverge if it returns : 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.Forward abstract interpretation
Strictness analysis can be characterized as a forward abstract interpretationAbstract interpretation
In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...
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
Alan Mycroft
Alan Mycroft is a reader at the University of Cambridge Computer Laboratory. He is a Fellow of Robinson College, Cambridge, where he is also director of studies for computer science.With Arthur Norman, he co-created the Norcroft C compiler...
, the abstract interpretation used a two-point domain
Domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
with 0 denoting the set
considered as a subset of the argument or return type, and 1 denoting all values in the type.Demand analysis
The Glasgow Haskell CompilerGlasgow Haskell Compiler
The Glorious Glasgow Haskell Compilation System, more commonly known as the Glasgow Haskell Compiler or GHC, is an open source native code compiler for the functional programming language Haskell. The lead developers are Simon Peyton Jones and Simon Marlow...
(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.
Projection-based strictness analysis
Projection-based strictness analysis, introduced by Philip WadlerPhilip Wadler
Philip Wadler is a computer scientist known for his contributions to programming language design and type theory. In particular, he has contributed to the theory behind functional programming and the use of monads in functional programming, the design of the purely functional language Haskell, and...
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
is considered head-strict if , where is the projection that head-evaluates its list argument.There was a large body of research on strictness analysis in the 1980s.