What does seq actually do in Haskell?

Question

From Real World Haskell I read

It operates as follows: when a seq expression is evaluated, it forces its first argument to be evaluated, then returns its second argument. It doesn't actually do anything with the first argument: seq exists solely as a way to force that value to be evaluated.

where I've emphasised the then because to me it implies an order in which the two things happen.

From Hackage I read

The value of seq a b is bottom if a is bottom, and otherwise equal to b. In other words, it evaluates the first argument a to weak head normal form (WHNF). seq is usually introduced to improve performance by avoiding unneeded laziness.

A note on evaluation order: the expression seq a b does not guarantee that a will be evaluated before b. The only guarantee given by seq is that the both a and b will be evaluated before seq returns a value. In particular, this means that b may be evaluated before a. […]

Furthermore, if I click on the # Source link from there, the page doesn't exist, so I can't see the code of seq.

That seems in line with a comment under this answer:

[…] seq cannot be defined in normal Haskell

On the other hand (or on the same hand, really), another comment reads

The 'real' seq is defined in GHC.Prim as seq :: a -> b -> b; seq = let x = x in x. This is only a dummy definition. Basically seq is specially syntax handled particularly by the compiler.

Can anybody shed some light on this topic? Especially in the following respects.

• What source is right?
• Is seq's implementation really not writable in Haskell?
  • If so, what does it even mean? That it is a primitive? What does this tell me about what seq actually does?
• In seq a b is a guaranteed to be evaluated before b at least in the case that b makes use of a, e.g. seq a (a + x)?

Answer 1

Others answers have already discussed the meaning of seq and its relationship to pseq. But there appears to be quite some confusion about what exactly the implications of seq’s caveats are.

It is true, technically speaking, that a `seq` b does not guarantee a will be evaluated before b. This may seem troubling: how could it possibly serve its purpose if that were the case? Let’s consider the example Jon gave in their answer:

foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' f acc [] = acc
foldl' f acc (x : xs)
  = acc' `seq` foldl' f acc' xs
  where
    acc' = f acc x

Surely, we care about acc' being evaluated before the recursive call here. If it is not, the whole purpose of foldl' is lost! So why not use pseq here? And is seq really all that useful?

Fortunately, the situation is not actually so dire. seq really is the right choice here. GHC would never actually choose to compile foldl' such that it evaluates the recursive call before evaluating acc', so the behavior we want is preserved. The difference between seq and pseq is rather what flexibility the optimizer has to make a different decision when it thinks it has particularly good reason to.

Understanding seq and pseq’s strictness

To understand what that means, we must learn to think a little like the GHC optimizer. In practice, the only concrete difference between seq and pseq is how they affect the strictness analyzer:

1. seq is considered strict in both of its arguments. That is, in a function definition like

   f a b c = (a `seq` b) + c
   

   f will be considered strict in all three of its arguments.

2. pseq is just like seq, but it’s only considered strict in its first argument, not its second one. That means in a function definition like

   g a b c = (a `pseq` b) + c
   

   g will be considered strict in a and c, but not b.

What does this mean? Well, let’s first define what it means for a function to “be strict in one of its arguments” in the first place. The idea is that if a function is strict in one of its arguments, then a call to that function is guaranteed to evaluate that argument. This has several implications:

• Suppose we have a function foo :: Int -> Int that is strict in its argument, and suppose we have a call to foo that looks like this:

  foo (x + y)
  

  A naïve Haskell compiler would construct a thunk for the expression x + y and pass the resulting thunk to foo. But we know that evaluating foo will necessarily force that thunk, so we’re not gaining anything from this laziness. It would be better to evaluate x + y immediately, then pass the result to foo to save a needless thunk allocation.

• Since we know there’s never any reason to pass a thunk to foo, we gain an opportunity to make additional optimizations. For example, the optimizer could choose to internally rewrite foo to take an unboxed Int# instead of an Int, avoiding not only a thunk construction for x + y but avoiding boxing the resulting value altogether. This allows the result of x + y to be passed directly, on the stack, rather than on the heap.

As you can see, strictness analysis is rather crucial to making an efficient Haskell compiler, as it allows the compiler to make far more intelligent decisions about how to compile function calls, among other things. For that reason, we generally want strictness analysis to find as many opportunities to eagerly evaluate things as possible, letting us save on useless heap allocations.

With this in mind, let’s return to our f and g examples above. Let’s think about what strictness we’d intuitively expect these functions to have:

1. Recall that the body of f is (a `seq` b) + c. Even if we ignore the special properties of seq altogether, we know that it eventually evaluates to its second argument. This means f ought to be at least as strict as if its body were just b + c (with a entirely unused).

   We know that evaluating b + c must fundamentally evaluate both b and c, so f must, at the very least, be strict in both b and c. Whether it’s strict in a is the more interesting question. If seq were actually just flip const, it would not be, as a would not be used, but of course the whole point of seq is to introduce artificial strictness, so in fact f is also considered strict in a.

   Happily, the strictness of f I mentioned above is entirely consistent with our intuition about what strictness it ought to have. f is strict in all of its arguments, precisely as we would expect.

2. Intuitively, all of the above reasoning for f should also apply to g. The only difference is the replacement of seq with pseq, and we know that pseq provides a stronger guarantee about evaluation order than seq does, so we’d expect g to be at least as strict as f… which is to say, also strict in all its arguments.

   However, remarkably, this is not the strictness GHC infers for g. GHC considers g strict in a and c, but not b, even though by our definition of strictness above, g is rather obviously strict in b: b must be evaluated for g to produce a result! As we’ll see, it is precisely this discrepancy that makes pseq so deeply magical, and why it’s generally a bad idea.

The implications of strictness

We’ve now seen that seq leads to the strictness we’d expect while pseq does not, but it’s not immediately obvious what that implies. To illustrate, consider a possible call site where f is used:

f a (b + 1) c

We know that f is strict in all its arguments, so by the same reasoning we used above, GHC should evaluate b + 1 eagerly and pass its result to f, avoiding a thunk.

At first blush, this might seem all well and good, but wait: what if a is a thunk? Even though f is also strict in a, it’s just a bare variable—maybe it was passed in as an argument from somewhere else—and there’s no reason for GHC to eagerly force a here if f is going to force it itself. The only reason we force b + 1 is to spare a new thunk from being created, but we save nothing but forcing the already-created a at the call site. This means a might in fact be passed as an unevaluated thunk.

This is something of a problem, because in the body of f, we wrote a `seq` b, requesting a be evaluated before b. But by our reasoning above, GHC just went ahead and evaluated b first! If we really, really need to make sure b isn’t evaluated until after a is, this type of eager evaluation can’t be allowed.

Of course, this is precisely why pseq is considered lazy in its second argument, even though it actually is not. If we replace f with g, then GHC would obediently allocate a fresh thunk for b + 1 and pass it on the heap, ensuring it is not evaluated a moment too soon. This of course means more heap allocation, no unboxing, and (worst of all) no propagation of strictness information further up the call chain, creating potentially cascading pessimizations. But hey, that’s what we asked for: avoid evaluating b too early at all costs!

Hopefully, this illustrates why pseq is seductive, but ultimately counterproductive unless you really know what you’re doing. Sure, you guarantee the evaluation you’re looking for… but at what cost?

The takeaways

Hopefully the above explanation has made clear how both seq and pseq have advantages and disadvantages:

• seq plays nice with the strictness analyzer, exposing many more potential optimizations, but those optimizations might disrupt the order of evaluation we expect.

• pseq preserves the desired evaluation order at all costs, but it only does this by outright lying to the strictness analyzer so it’ll stay off its case, dramatically weakening its ability to help the optimizer do good things.

How do we know which tradeoffs to choose? While we may now understand why seq can sometimes fail to evaluate its first argument before its second, we don’t have any more reason to believe this is an okay thing to let happen.

To soothe your fears, let’s take a step back and think about what’s really happening here. Note that GHC never actually compiles the a `seq` b expression itself in such a way that a is failed to be evaluated before b. Given an expression like a `seq` (b + c), GHC won’t ever secretly stab you in the back and evaluate b + c before evaluating a. Rather, what it does is much more subtle: it might indirectly cause b and c to be individually evaluated before evaluating the overall b + c expression, since the strictness analyzer will note that the overall expression is still strict in both b and c.

How all this fits together is incredibly tricky, and it might make your head spin, so perhaps you don’t find the previous paragraph all that soothing after all. But to make the point more concrete, let’s return to the foldl' example at the beginning of this answer. Recall that it contains an expression like this:

acc' `seq` foldl' f acc' xs

In order to avoid the thunk blowup, we need acc' to be evaluated before the recursive call to foldl'. But given the above reasoning, it still always will be! The difference that seq makes here relative to pseq is, again, only relevant for strictness analysis: it allows GHC to infer that this expression is also strict in f and xs, not just acc', which in this situation doesn’t actually change much at all:

• The overall foldl' function still isn’t considered strict in f, since in the first case of the function (the one where xs is []), f is unused, so for some call patterns, foldl' is lazy in f.

• foldl' can be considered strict in xs, but that is totally uninteresting here, since xs is only a piece of one of foldl'’s arguments, and that strictness information doesn’t affect the strictness of foldl' at all.

So, if there is not actually any difference here, why not use pseq? Well, suppose foldl' is inlined some finite number of times at a call site, since maybe the shape of its second argument is partially known. The strictness information exposed by seq might then expose several additional optimizations at the call site, leading to a chain of advantageous optimizations. If pseq had been used, those optimizations would be obscured, and GHC would produce worse code.

The real takeaway here is therefore that even though seq might sometimes not evaluate its first argument before its second, this is only technically true, the way it happens is subtle, and it’s pretty unlikely to break your program. This should not be too surprising: seq is the tool the authors of GHC expect programmers to use in this situation, so it would be rather rude of them to make it do the wrong thing! seq is the idiomatic tool for this job, not pseq, so use seq.

When do you use pseq, then? Only when you really, really care about a very specific evaluation order, which usually only happens for one of two reasons: you are using par-based parallelism, or you’re using unsafePerformIO and care about the order of side effects. If you’re not doing either of these things, then don’t use pseq. If all you care about is use cases like foldl', where you just want to avoid needless thunk build-up, use seq. That’s what it’s for.

Answer 2

seq introduces an artificial data dependency between two thunks. Normally, a thunk is forced to evaluate only when pattern-matching demands it. If the thunk a contains the expression case b of { … }, then forcing a also forces b. So there is a dependency between the two: in order to determine the value of a, we must evaluate b.

seq specifies this relationship between any two arbitrary thunks. When seq c d is forced, c is forced in addition to d. Note that I don’t say before: according to the standard, an implementation is free to force c before d or d before c or even some mixture thereof. It’s only required that if c does not halt, then seq c d also doesn’t halt. If you want to guarantee evaluation order, you can use pseq.

The diagrams below illustrate the difference. A black arrowhead (▼) indicates a real data dependency, the kind that you could express using case; a white arrowhead (▽) indicates an artificial dependency.

• Forcing seq a b must force both a and b.

    │
  ┌─▼───────┐
  │ seq a b │
  └─┬─────┬─┘
    │     │  
  ┌─▽─┐ ┌─▼─┐
  │ a │ │ b │
  └───┘ └───┘
  

• Forcing pseq a b must force b, which must first force a.

    │
  ┌─▼────────┐
  │ pseq a b │
  └─┬────────┘
    │
  ┌─▼─┐
  │ b │
  └─┬─┘
    │
  ┌─▽─┐
  │ a │
  └───┘
  

As it stands, it must be implemented as an intrinsic because its type, forall a b. a -> b -> b, claims that it works for any types a and b, without any constraint. It used to belong to a typeclass, but this was removed and made into a primitive because the typeclass version was considered to have poor ergonomics: adding seq to try to fix a performance issue in a deeply nested chain of function calls would require adding a boilerplate Seq a constraint on every function in the chain. (I would prefer the explicitness, but it would be hard to change now.)

So seq, and syntactic sugar for it like strict fields in data types or BangPatterns in patterns, is about ensuring that something is evaluated by attaching it to the evaluation of something else that will be evaluated. The classic example is foldl'. Here, the seq ensures that when the recursive call is forced, the accumulator is also forced:

foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' f acc [] = acc
foldl' f acc (x : xs)
  = acc' `seq` foldl' f acc' xs
  where
    acc' = f acc x

That requests of the compiler that if f is strict, such as (+) on a strict data type like Int, then the accumulator is reduced to an Int at each step, rather than building a chain of thunks to be evaluated only at the end.