[Haskell-cafe] Re: A suggestion for the next high profile Haskell project [Was: Re: What is a hacker?]

[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.

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

Thanks

Neil