Adrian Hey <[EMAIL PROTECTED]>:
>The issue I'm thinking about is equational reasoning and program
>transformation. For a lazy (non-strict) language, transformations
>are constrained so that a function definition which is non-strict
>in an argument is never transformed into one which is strict in the
>same argument. (Or so I believe, please correct me if I'm wrong).
Well, if you want the transformations to preserve the semantics, yes.
(N.b. that a function with a nonstrict argument may be called in an
environment where we know something about the argument, for instance, that
it is always evaluated, which then makes it correct to replace *that call*
to the function with a call to a transformed function with a strict
argument.)
>This seems completely contrary to normal equational reasoning (which is
>one thing functional languages are supposed to support), where we aren't
>so constrained.
No. Equational reasoning simply means that we use equations which are valid
to transform expressions. When used for program transformations, the set of
valid equations is determined by the semantics of the language. This set of
equations will change depending on whether the language is strict or
nonstrict. For instance, a logical or which is strict in both arguments will
be commutative and associative, while a nonstrict or with a left-to-right
evaluation order of its arguments will be non-commutative but still
associative.
Nonstrict languages actually have the property that function definitions can
be seen as equations. I would say this is what makes the language
referentially transparent! This means that a function call can always be
symbolically unfolded without altering the semantics. Strict languages do
not have this property in general. So in this sense nonstrict languages are
more amenable to equational reasoning!
Note that if we want the transformations to preserve the semantics of the
language w.r.t. termination we will have to deal with bottom in equations
also in strict languages, since also strict languages contain certain
operations with nonstrict semantics (e.g., conditionals). Of course, we can
consider a coarser semantics without the bottom, where we do not distinguish
functions w.r.t. termination properties, and then have a different set of
equalities: a good example is x - x = 0 which is valid if bottom is
discarded but not valid if it is included. (I believe it may be this kind of
discrepancy which has lead you to think that nonstrict languages do not
permit equational reasoning.)
>So is it unfair to say that as soon as issues like strict vs. non-strict
>semantics become an important, the language is no longer purely functional?
It is not only unfair, it is wrong.
>Doesn't having to treat _|_ as a value spoil equational reasoning?
No, see above.
Bj�rn Lisper
