2006/12/19, Neil Mitchell <[EMAIL PROTECTED]>:
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
