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.

Note how in a strict language inlining is not as safe as it once was...

Thanks

Neil
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to