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