Meaning of strictness

Learn
1

Hello Haskell community. I’ve only been a spectator in this discourse so far, so this is my first time starting a post myself. Nice to meet you!

I thought I understood what strictness meant but I realized there were still some holes when I tried to put it into words more precisely.
I’m still a bit confused, so perhaps my formulation below may not be precise to begin with, but I’ll try my best.

I often see the definition:

f _|_ = _|_ <=> f strict

In purely theoretical terms, I think this definition makes sense.

But in Haskell discussions, strictness seems to mean more than just this.
For example, if we only care about the above definition, the following would be strict:

f !x = g x

f undefined      -- undefined
f (1 + undefined) -- undefined

[Aside: actually, if I took the definition at face value, then id undefined = undefined so id would be strict as well. I’m not sure who is responsible (the function itself or the caller) for evaluating the arguments in this definition]

But I think in typical Haskell discussions, this isn’t what is meant by strictness, especially if g is lazy and accumulates a lot of thunks.
Instead we would need at least something like:

f' x = let !y = g x in y

and only then would we say f' is strict. (or even this isn’t enough depending on g, such as with foldl')

But we may also differentiate the two and say f is strict in its argument and f' is strict in its result, or something along those lines.
e.g.

Either way, it’s a bit different from the definition f _|_ = _|_.
Put another way, in Haskell discussions, strictness isn’t so much about the handling of bottom, but more about thunk accumulation and evaluation, which I believe are related but not exactly the same thing. e.g. foldl'

But there are also cases where strictness does refer to the original definition, like Data.Function

And I find myself easily confused when I start thinking about related topic like evaluation and WHNF, the evaluate function, packages with lazy and strict versions, memory leaks such as those in Control.Monad.Trans.Writer.Strict vs Control.Monad.Trans.Writer.CPS (not entirely due to strictness, but still part of the problem), etc

I was wondering if there is a more precise definition of these different strictnesses in Haskell, and whether there is some comprehensive resource on this topic (I’ve looked so far in common places like the language report, GHC docs, Haskell wiki).
Thank you!

2

This is lazy and the same as f x = g x. There is no such thing as “strict in the result” (or alternatively: every function is strict in its result).

There is some nuance to the f ⊥ = ⊥ definition, which is that the laziness might be deeper in the argument if it is a data structure. For example, f (x, y) = g x y is technically strict, but in some sense it is still lazy in the x and y components of the tuple (assuming g is lazy in its arguments).

Higher-order functions complicate this even further. When a function can be given an arbitrary function as argent, GHC must assume that the argument function is lazy. Consider the naive foldl:

foldl k z [] = z
foldl k z (x:xs) = foldl k (k z x) xs

Here the first case is strict in z, but in the second case z is only used as an argument to k and that can be any function, so we must assume it is lazy. Note that this doesn’t mean that we need to allocate a thunk for z, but it does mean that we need to allocate a thunk to store the unevaluated k z x function which we later pass back into the z parameter of the next iteration of the foldl.

If you define foldl so that foldl k ⊥ xs = ⊥, for example by adding a bang pattern on z, then you really do have foldl'. That is basically the only difference. It is possible to define a foldl' with strict semantics that still leaks memory.

3

There is a series of four videos here on Laziness in Haskell, which (if you have not seen them) may interest you:

4

Thank you, @jaror !
I think I realized where my whole misunderstanding came from and feel quite embarrassed about the question now.
I’d committed the common mistake of conflating non-strict semantics with laziness, and confused myself with it.
In particular, I kept thinking about thunks when considering strictness (hence where the thought of strict in result came from), but that’s not really relevant at least as far as strictness is concerned, since it’s about denotational semantics and not evaluation…

To confirm my understanding:

we could make this strict by something like f (!x, !y) = g x y . So then it would be strict in both the pair and its values, regardless of the strictness of g.

I think I ended up confusing myself because performance discussions often mention making things “strict” or “stricter”. This is because strict functions typically perform better, but to be precise, strictness itself isn’t about performance (since it’s about denotational semantics).
Is this correct..?

5

@mpilgrem I recall watching bits of it a couple of years ago, but this would be a good opportunity to revisit. Thanks!

6

One must not confuse operational and denotational semantics. Experts like @sgraf may correct me, but a thunk is operational: A memory representation of a not-fully-evaluated piece of code. Even in a fully strict language, the run-time may choose to work with intermediate thunks. In contrast, bottom ⊥ is denotational.

The various strictness annotations in Haskell or GHC also have both operational and denotational consequences. When defining

data Foo = Foo {
   getA :: !A
   }

it means that the denotation of type Foo does not contain more elements than the denotation of type A. But it also means that pattern matching a Foo will operationally force any thunk that resides in the A. (Without the bang, the elements Foo ⊥ and ⊥ are distinct.)

Do you know the :print command in GHCi? It can be used to explore how strict a function is.

Prelude> nats = 0 : map succ nats :: [Integer]
Prelude> :print nats
nats = (_t1::[Integer])

This shows that currently, nats is basically a thunk, or just as good as ⊥.
Now let’s evaluate it a little:

Prelude> take 2 nats
[0,1]
Prelude> :print nats
nats = 0 : 1 : (_t2::[Integer])

The runtime now knows that nats is at least 0 : 1 : ⊥ but we have not looked further. Conclusion: take 2 is strict in the sense that take 2 undefined = undefined. But it is also lazy because it fails to distinguish 0 : 1 : undefined from e.g. 0 : 1 : 2 : [].

7

Semantic strictness is more than just about evaluation. Take the tail recursive factorial function

fact :: Int -> Int -> Int
fact r 0 = r
fact r n = fact (n*r) (n-1)
fac :: Int -> Int
fac = fact 1

Is fact strict in its first argument? It’s subtle. If we call fac with a negative number then fact will never reach the base case, so r will never get evaluated. So one might think that we cannot conclude that fact is strict in its first argument, but in fact it is! If we look at fact _|_ n, what can happen? If n>=0 we reach the base case and the result is _|_, if n<0 then fact will not terminate, which is also _|_. So no matter what, passing _|_ as the first argument will result in _|_, so fact is strict in its first argument. A strictness analyzer can figure this out (quite easily, in fact) and so the n*r multiplication can be perforrmed before doing the tail call. And so fact runs nicely in constant space.

8

@olf Thank you. I have been aware of these as features, but it all makes more sense now.

9

@augustss Thank you. So, in ghc this would be -fstrictness?

update: this indeed is a curious example. Taking a second look..

10

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.

11

It’ll take me a while to digest this but this is very fascinating.
I am tempted to explore further, though I fear it’ll be a very deep rabbit hole…

Nevertheless, I started reading a blog post which I believe is yours from a few years ago on strictness analysis: fixpt · All About Strictness Analysis (part 1)

I tried ghc -O2 strict.hs -ddump-stranal -fforce-recomp on @augustss 's factorial:

$wfact_s2be [InlPrag=[2], Occ=LoopBreaker, Dmd=LC(L,C(1,L))]
  :: GHC.Prim.Int# -> GHC.Prim.Int# -> GHC.Prim.Int#
[LclId[StrictWorker([])],
 Arity=2,
 Str=<L><1L>,
 Unf=Unf{Src=<vanilla>, TopLvl=True,
         Value=True, ConLike=True, WorkFree=True, Expandable=True,
         Guidance=IF_ARGS [0 30] 52 0}]
$wfact_s2be
  = \ (ww_s2b6 :: GHC.Prim.Int#)
      (ww_s2ba [Dmd=1L] :: GHC.Prim.Int#) ->
      case ww_s2ba of ds_X1 {
        __DEFAULT ->
          $wfact_s2be (GHC.Prim.*# ds_X1 ww_s2b6) (GHC.Prim.-# ds_X1 1#);
        0# -> ww_s2b6
      }

which I believe shows that it did infer strictness (and calls by value unboxed) in both arguments. And profiling fac 1000000000:

50,440 bytes allocated in the heap
           3,272 bytes copied during GC
          44,328 bytes maximum residency (1 sample(s))
          25,304 bytes maximum slop
               6 MiB total memory in use (0 MiB lost due to fragmentation)

...

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time    0.943s  (  0.944s elapsed)
  GC      time    0.000s  (  0.000s elapsed)
  EXIT    time    0.000s  (  0.011s elapsed)
  Total   time    0.944s  (  0.957s elapsed)

Just to play around, I tried the same with explicit strictness and the result was the same

fact' !r 0 = r
fact' !r n = fact' (n * r) (n - 1)

I apologize that this may be going off on a tangent, but I have one question from the example in the blog post.printListAverage and fact here seem similar in that both have an argument that may never get evaluated, and yet the opposite seems to be happening.

In the fact case, strictness analysis does determine that the function is strict in r despite for a negative n like fact undefined -1, the crash is not due to r but non-termination.

But for printListAverage, strictness analysis doesn’t make sum call-by-value, and this is attributed to the error call not being the same as undefined

printAverage (RunningTotal undefined 0) will print the expected error message instead of crashing due to undefined, which is the very definition of being lazy in sum. This extends to a call like go (RunningTotal undefined 0) [], so GHC can’t just unbox the sum field even if the recursive case of go is annotated.

Put another way, it seems like in fact’s case, the differences in ways of crashing/diverging doesn’t matter, whereas in printListAverage it does?
What am I missing..?

I’m using ghc 9.6.7.

p.s.
Changing the | count == 0 = error "..." to | count == 0 = undefined didn’t make a difference either… On the otherhand, putting the strictness on x in the list alone instead of printAverage (RunningTotal !sum count) appears to perform equally well, if I’m not mistaken.

  go rt [] = printAverage rt
  go (RunningTotal sum count) (!x : xs) = -- the only !
    go (RunningTotal (sum + x) (count + 1)) xs
12

A sharp realization :slight_smile: I think the reason is that print is lazy in its argument. Note that print does quite a lot of IO related things.

13

I’m sure people above have explained it well enough, but let me add one more interesting reference:

I remembered watching these 5 min of SPJ explaining the relationship between laziness and strictness by comparing Haskell to OCaml.

https://www.youtube.com/watch?v=xcB_LF3cdqw&list=WL&index=42&t=3202s

14

Ah right, it goes through print and the result is IO ()!