Personal tools

Seq

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m
(6 intermediate revisions by 2 users not shown)
Line 1: Line 1:
  +
<span>{{DISPLAYTITLE:seq}}</span>
  +
 
The <tt>seq</tt> function is the most basic method of introducing strictness to a Haskell program. <tt>seq :: a -> b -> b</tt> takes two arguments of any type, and returns the second. However, it also has the important property that it is magically strict in its first argument. In essence, <tt>seq</tt> is defined by the following two equations:
 
The <tt>seq</tt> function is the most basic method of introducing strictness to a Haskell program. <tt>seq :: a -> b -> b</tt> takes two arguments of any type, and returns the second. However, it also has the important property that it is magically strict in its first argument. In essence, <tt>seq</tt> is defined by the following two equations:
   
Line 6: Line 8:
 
</haskell>
 
</haskell>
   
A common misconception regarding <tt>seq</tt> is that <tt>seq x</tt> "evaluates" <tt>x</tt>. Well, sort of. <tt>seq</tt> 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 <tt>seq</tt> is evaluated, the first argument must also be evaluated. As an example, suppose <tt>x :: Integer</tt>, then <tt>seq x b</tt> behaves essentially like <tt>if x == 0 then b else b</tt> – unconditionally equal to <tt>b</tt>, but forcing <tt>x</tt> along the way. In particular, the expression <tt>x `seq` x</tt> is completely redundant, and always has exactly the same effect as just writing <tt>x</tt>.
+
See [[Bottom]] for an explanation of the symbol.
   
Strictly speaking, the two equations of <tt>seq</tt> are all it must satisfy, and if the compiler can statically prove that the first argument is not ⊥, it doesn't have to evaluate it 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). However, it ''is'' the case that evaluating <tt>b</tt> and ''then'' <tt>a</tt>, then returning <tt>b</tt> is a perfectly legitimate thing to do; it is to prevent this ambiguity that <tt>pseq</tt> was invented, but that's another story.
+
A common misconception regarding <tt>seq</tt> is that <tt>seq x</tt> "evaluates" <tt>x</tt>. Well, sort of. <tt>seq</tt> 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 <tt>seq</tt> is evaluated, the first argument must also (sort of; see below) be evaluated. As an example, suppose <tt>x :: Integer</tt>, then <tt>seq x b</tt> behaves essentially like <tt>if x == 0 then b else b</tt> unconditionally equal to <tt>b</tt>, but forcing <tt>x</tt> along the way. In particular, the expression <tt>x `seq` x</tt> is completely redundant, and always has exactly the same effect as just writing <tt>x</tt>.
  +
  +
Strictly speaking, the two equations of <tt>seq</tt> 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). However, it ''is'' the case that evaluating <tt>b</tt> and ''then'' <tt>a</tt>, then returning <tt>b</tt> is a perfectly legitimate thing to do; it is to prevent this ambiguity that <tt>pseq</tt> was invented, but that's another story.
   
 
=== Common uses of <tt>seq</tt> ===
 
=== Common uses of <tt>seq</tt> ===
Line 46: Line 48:
 
=== Controversy! ===
 
=== Controversy! ===
   
Note that <tt>seq</tt> is the ''only'' way to force evaluation of a value with a function type. It is the only reason why Haskell programs are able to distinguish between the following two values:
+
Note that <tt>seq</tt> is the ''only'' way to force evaluation of a value with a function type (except by applying it, which is liable to cause other problems). As such, it is the only reason why Haskell programs are able to distinguish between the following two values:
   
 
<haskell>
 
<haskell>
Line 54: Line 56:
   
 
This violates the principle from lambda calculus of extensionality of functions, or eta-conversion, because <tt>f</tt> and <tt>\x -> f x</tt> are distinct functions, even though they return the same output for ''every'' input. For this reason, <tt>seq</tt>, and this distinction, is sometimes ignored e.g. when assessing the correctness of [[Correctness of short cut fusion|optimisation techniques]] or type class instances.
 
This violates the principle from lambda calculus of extensionality of functions, or eta-conversion, because <tt>f</tt> and <tt>\x -> f x</tt> are distinct functions, even though they return the same output for ''every'' input. For this reason, <tt>seq</tt>, and this distinction, is sometimes ignored e.g. when assessing the correctness of [[Correctness of short cut fusion|optimisation techniques]] or type class instances.
  +
  +
== See also ==
  +
  +
* [http://stackoverflow.com/questions/12687392/why-is-seq-bad Why is seq bad?]
  +
  +
[[Category:Glossary]]

Revision as of 03:09, 27 December 2012

The seq function is the most basic method of introducing strictness to a Haskell program. seq :: a -> b -> b takes two arguments of any type, and returns the second. However, it also has the important property that it is magically strict in its first argument. In essence, seq is defined by the following two equations:

⊥ `seq` b = ⊥
a `seq` b = b

See Bottom for an explanation of the ⊥ symbol.

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). However, it is the case that evaluating b and then a, then returning b is a perfectly legitimate thing to do; it is to prevent this ambiguity that pseq was invented, but that's another story.

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

2 Controversy!

Note that seq is the only way to force evaluation of a value with a function type (except by applying it, which is liable to cause other problems). As such, 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 from lambda calculus of extensionality of functions, or eta-conversion, because f and \x -> f x are distinct functions, even though they return the same output for every input. For this reason, seq, and this distinction, is sometimes ignored e.g. when assessing the correctness of optimisation techniques or type class instances.

3 See also