2006/12/19, Neil Mitchell
Hi minh thu,
Lazy semantics -> equational reasoning ? I thought that : lack of mutable state -> equational reasoning. For instance, I think to data flow variable in Oz (whcih I really don't know much / never used) : if a (Oz managed) thread attemps to read the value of an unbound (data flow) variable, it waits until another thread binds it. But the equational reasoning (referential transparency) remains (and the evaluation is eager by default).
Lack of mutable state, referentially transparent and laziness all help with equational reasoning. Inlining is much easier in a lazy language - and inlining is really handy for equational reasoning.
Imagine:
not_term = non_term f x = 12
Now evaluating:
main = f non_term
In a lazy language the value is always 12, in a strict language its always _|_. Now let's inline f:
main = 12
In a lazy language the value is still 12, in a strict language the value has changed. Sorry, I don't see how it has changed. Isn't it still _|_ ? i.e.
main = _|_ Thanks minh thu