On Mon, Nov 3, 2008 at 2:54 PM, Don Stewart <[EMAIL PROTECTED]> wrote: > lrpalmer: >> On Mon, Nov 3, 2008 at 2:35 PM, Don Stewart <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe