# seq

While its name might suggest otherwise, the `seq`

function's purpose is to introduce *strictness* to a Haskell program. As indicated by its type signature:

```
seq :: a -> b -> b
```

it takes two arguments of any type, and returns the second. However, it also has the important property that it is always strict in its first argument. In essence, `seq`

is defined by the following two equations:

```
⊥ `seq` b = ⊥
a `seq` b | a ≠ ⊥ = b
```

(See Bottom for an explanation of the `⊥`

symbol.)

### History

The need to specify an order of evaluation in otherwise-nonstrict programming languages has appeared before:

We can use

`VAL`

to define a "sequential evaluation" operator which evaluates its first argument and then returns its second:a ; b = (λx. b) val aand we can define other functions which control evaluation order [...]

- The Design and Implementation of Programming Languages (page 88 of 159).

`seq' applied to two values, returns the second but checks that the first value is not completely undefined. Sometimes needed, e.g. to ensure correct synchronisation in interactive programs.

> seq :: *->**->** ||defined internally

and in Haskell since at least 1996:

The

`seq`

combinator implements sequential composition. When the expression`e1 ‘seq‘ e2`

is evaluated,`e1`

is evaluated to weak head normal form first, and then the value of`e2`

is returned. In the following parallel`nfib`

function,`seq`

is used to force the evaluation of`n2`

before the addition takes place. This is because Haskell does not specify which operand is evaluated first, and if`n1`

was evaluated before`n2`

, there would be no parallelism. nfib :: Int -> Int nfib n | n <= 1 = 1 | otherwise = n1 ‘par‘ (n2 ‘seq‘ n1 + n2 + 1) where n1 = nfib (n-1) n2 = nfib (n-2)

...the same year `seq`

was introduced in Haskell 1.3 as a method of the (now-abandonded) `Eval`

type class:

```
class Eval a where
strict :: (a -> b) -> a -> b
seq :: a -> b -> b
strict f x = x ‘seq‘ f x
```

However, despite that need by the time Haskell 98 was released `seq`

had been reduced to a primitive strictness definition. But in 2009, all doubts about the need for a primitive sequencing definition were vanquished:

2.1 The need for`pseq`

The

`pseq`

combinator is used for sequencing; informally, it evaluates its first argument to weak-head normal form, and then evaluates its second argument, returning the value of its second argument. Consider this definition of`parMap`

: parMap f [] = [] parMap f (x:xs) = y ‘par‘ (ys ‘pseq‘ y:ys) where y = f x ys = parMap f xsThe intention here is to spark the evaluation of

`f x`

, and then evaluate`parMap f xs`

, before returning the new list`y:ys`

. The programmer is hoping to express anorderingof the evaluation:firstspark`y`

,thenevaluate`ys`

.

- Runtime Support for Multicore Haskell (page 2 of 12).

Alas, this confirmation failed to influence Haskell 2010 - to this day, `seq`

remains just a primitive strictness definition. So for enhanced confusion the only Haskell implementation still in widespread use now provides both `seq`

and `pseq`

.

### Demystifying `seq`

A common misconception regarding `seq`

is that `seq x`

"evaluates" `x`

. Well, sort of. `seq`

doesn't evaluate anything just by virtue of existing in the source file, all it does is introduce an artificial data dependency of one value on another: when the result of `seq`

is evaluated, the first argument must also (sort of; see below) be evaluated. As an example, suppose `x :: Integer`

, then `seq x b`

behaves essentially like `if x == 0 then b else b`

– unconditionally equal to `b`, but forcing `x`

along the way. In particular, the expression `x `seq` x`

is completely redundant, and always has exactly the same effect as just writing `x`

.

Strictly speaking, the two equations of `seq`

are all it must satisfy, and if the compiler can statically prove that the first argument is not ⊥, or that its second argument *is*, it doesn't have to evaluate anything to meet its obligations. In practice, this almost never happens, and would probably be considered highly counterintuitive behaviour on the part of GHC (or whatever else you use to run your code). So for example, in `seq a b`

it is perfectly legitimate for `seq`

to:

- 1. evaluate
`b`

- its*second*argument,

- 2. before evaluating
`a`

- its first argument,

- 3. then returning
`b`

.

In this larger example:

```
let x = ... in
let y = sum [0..47] in
x `seq` 3 + y + y^2
```

`seq`

immediately evaluating its second argument (`3 + y + y^2`

) avoids having to allocate space to store `y`

:

```
let x = ... in
case sum [0..47] of
y -> x `seq` 3 + y + y^2
```

However, sometimes this ambiguity is undesirable, hence the need for `pseq`

.

### Common uses of `seq`

`seq`

is typically used in the semantic interpretation of other strictness techniques, like strictness annotations in data types, or GHC's `BangPatterns` extension. For example, the meaning of this:

```
f !x !y = z
```

is this:

```
f x y | x `seq` y `seq` False = undefined
| otherwise = z
```

although that literal translation may not actually take place.

`seq`

is frequently used with accumulating parameters to ensure that they don't become huge thunks, which will be forced at the end anyway. For example, strict `foldl`

:

```
foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' _ z [] = z
foldl' f z (x:xs) = let z' = f z x in z' `seq` foldl' f z' xs
```

It's also used to define strict application:

```
($!) :: (a -> b) -> a -> b
f $! x = x `seq` f x
```

which is useful for some of the same reasons.

### Controversy?

The presence of `seq`

in Haskell does have some disadvantages:

1. It is the only reason why Haskell programs are able to distinguish between the following two values: undefined :: a -> b const undefined :: a -> b

This violates the principle of extensionality of functions, or eta-conversion from the lambda calculus, because

`f`

and`\x -> f x`

are distinct functions, even though they return the same output for every input.2. It can invalidate optimisation techniques which would normally be safe, causing the following two expressions to differ: foldr ⊥ 0 (build seq) = foldr ⊥ 0 (seq (:) []) = foldr ⊥ 0 [] = 0 seq ⊥ 0 = ⊥

This weakens the ability to use parametricity, which implies

`foldr k z (build g) == g k z`

for suitable values of`g`

,`k`

and`z`

.3. It can invalidate laws which would otherwise hold, also causing expressions to have differing results: seq (⊥ >>= return :: State s a) True = True seq (⊥ :: State s a) True = ⊥

This violates the first monad law, that

`m >>= return == m`

.

But `seq`

(sequential or otherwise) isn't alone in causing such difficulties:

1. When combined with call-by-need semantics, the use of weak-head normal form is also detrimental to extensionality. 2. When combined with GADTs, the associated map functions which uphold the functor laws is also problematic for parametricity. 3. The ability to define the fixed-point combinator in Haskell using recursion: yet :: (a -> a) -> a yet f = f (yet f)

4. Strictness must be considered when deriving laws for various recursive algorithms (see chapter 6). 5. Similar to `seq`

and`⊥`

, the use of division and zero present their own challenges!

Therefore all such claims against `seq`

(or calls for its outright removal) should be examined *in this context*.

## See also

- Parallelism in 6.6 and seq vs. pseq, Haskell mail archives.

- Questioning seq, Haskell mail archives.

- seq [bedlam], the GHC wiki.