Meaning of strictness

A Haskell developer explains that strictness analysis, a denotational concept, does not guarantee a function evaluates its argument on every code path, as demonstrated by the function \x y -> x `seq` y, which is strict in y but never evaluates y if x diverges. This gap between denotational semantics and operational behavior has caused practical issues in GHC that are difficult to fix without regressions.

Indeed, “ f is strict” is a neat mathy notion from topology, apparently remote from “computing”, yet it supposedly has actual operational content: any non-constant program f : Int - Int that reliably diverges/errors when its argument does must evaluate that argument on every code path at least once ; otherwise it solves the halting problem. That is the property we exploit in Haskell. Equational reasoning gives us a nice way to reason about a function’s strictness, and hence a way to reason about its operational behavior too Furthermore, we can justify switching from call-by-need to call-by-value an operational flavour by trusting the results of a strictness analysis a denotational flavour . The latter is justified by a denotational semantics, not by an operational one. In fact, there’s a subtlety. Strictness analysis is not actually a safe “evaluated at least once” analysis. The function \x y - x seq y is strict in both x and y , but if x diverges we never evaluate y So “strictness = evaluated at least once” is wrong if we actually start caring about diverging programs, or just the distinction between crashing and diverging or crashing differently . Another way to put it: strictness isn’t a safety property https://en.wikipedia.org/wiki/Safety and liveness properties . Being strict in y is supposed to guarantee that y gets evaluated, and a safety property would let us point to the exact step/trace prefix where that happens. But on the diverging x seq y trace there is no such step: we get stuck evaluating x , never reach y , yet f is still strict in y . The denotational semantics is blind to this, because it collapses every divergence to the same | . IMO that’s one of the big gaping holes in traditional non-trace-based denotational semantics.I think Lennart’s example points at the exact same problem at the intuitive level. This subtlety has resurfaced in GHC a number of times, and it’s practically unfixable without incurring regressions in production code.