2006/12/19, Neil Mitchell
Hi Joachim,
Why? In case the strictness analyzer was buggy?
I'd be perfectly happy if that analysis were just a note saying "run ghc with such-and-these options and inspect the intermediate code for function foo to see that the strictness analyzer determined it will always terminate".
I think you are asking too much from the strictness analyzer.
Why would you want strict code? Haskell's lazy semantics makes it much more amenable to equational reasoning. If you keep this laziness you can do all manner of proofs on the code.
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). Cheers minh thu