Functional programming languages are informally classified into
pure and impure languages.
The precise meaning of this distinction has been a matter of controversy.
We therefore
investigate a formal definition of purity. We begin by showing that some
proposed definitions
which rely on confluence, soundness of the beta axiom, preservation of
pure observational
equivalences and independence of the order of evaluation, do not withstand
close scrutiny.
We propose instead a definition based on parameter-passing independence.
Intuitively, the definition implies that functions are pure mappings from
arguments to results; the operational
decision of how to pass the arguments is irrelevant. In the context
of Haskell, our definition
is consistent with the fact that the traditional call-by-name denotational
semantics coincides
with the traditional call-by-need implementation. Furthermore, our definition
is compatible
with the stream-based, continuation-based and monad-based integration of
computational
effects in Haskell. Finally, we observe that call-by-name reasoning principles
are unsound in
compilers for monadic Haskell.
A consistent extension of the lambda-calculus as a base for functional programming languages
