[Haskell-cafe] Problems with strictness analysis?

[Luke Palmer]

On Mon, Nov 3, 2008 at 2:54 PM, Don Stewart <dons at galois.com> wrote:
> lrpalmer:
>> On Mon, Nov 3, 2008 at 2:35 PM, Don Stewart <dons at galois.com> wrote:
>> > Consider this program,
>> >
>> >            isum  0  s = s
>> >            isum  n  s = isum (n-1) (s+n)
>> >
>> >            main = case isum 10000000 0 {- rsum 10000000 -} of
>> >                     0 -> print 0
>> >                     x -> print x
>> >
>> > Now, isum is *not* strict in 's', [...]
>> >
>> > Of course, we make this strict in a number of ways:
>> >
>> > * Turning on optimisations:
>>
>> I am confused about your usage of "strict".  Optimizations are not
>> supposed to change semantics, so I don't know how it is possible to
>> make a function strict by turning on optimizations.  This function was
>> always strict in s, given a strict numeral type.  By induction on n:
>>
>>   isum 0 _|_ = _|_
>>   isum (n+1) _|_ = isum n (s+_|_) = isum n _|_ = _|_
>>
>> For negative n, it either wraps around to positive in which case the
>> above analysis applies, or it does not halt, which is strict (in the
>> same way "const _|_" is strict).
>
> "Optimisations" enable strictness analysis.

I was actually being an annoying purist.  "f is strict" means "f _|_ =
_|_", so strictness is a semantic idea, not an operational one.
Optimizations can change operation, but must preserve semantics.

But I'm not just picking a fight.  I'm trying to promote equational
reasoning over operational reasoning in the community, since I believe
that is Haskell's primary strength.

Luke