Editing Seq (section)

=== Controversy? ===

The presence of <code>seq</code> in Haskell does have some disadvantages:
:{|
|- style="vertical-align:top;"
|1.
|It is the only reason why Haskell programs are able to distinguish between the following two values:

<haskell>
undefined       :: a -> b
const undefined :: a -> b
</haskell>

This violates the principle of extensionality of functions, or eta-conversion from the lambda calculus, because <code>f</code> and <code>\x -> f x</code> are distinct functions, even though they return the same output for every input.
|- style="vertical-align:top;"
|2.
|It can invalidate [[Correctness of short cut fusion|optimisation techniques]] which would normally be safe, causing the following two expressions to differ:
 
<haskell>
foldr ⊥ 0 (build seq) = foldr ⊥ 0 (seq (:) []) = foldr ⊥ 0 [] = 0
seq ⊥ 0                                                       = ⊥
</haskell>

This weakens the ability to use parametricity, which implies <code>foldr k z (build g) == g k z</code> for suitable values of <code>g</code>, <code>k</code> and <code>z</code>.
|- style="vertical-align:top;"
|3.
|It can invalidate laws which would otherwise hold, also causing expressions to have differing results:

<haskell>
seq (⊥ >>= return :: State s a) True = True
seq (⊥ :: State s a) True            = ⊥
</haskell>

This violates the first [[Monad laws|monad law]], that <code>m >>= return == m</code>.
|}

But <code>seq</code> (sequential or otherwise) isn't alone in causing such difficulties:
:{|
|- style="vertical-align:top;"
|1.
|When combined with call-by-need semantics, the use of weak-head normal form [https://www.pauldownen.com/publications/first-class-call-stacks.pdf is also detrimental to extensionality].
|- style="vertical-align:top;"
|2.
|When combined with GADTs, the associated map functions which uphold the functor laws [https://arxiv.org/pdf/2105.03389v3 is also problematic for parametricity].
|- style="vertical-align:top;"
|3.
|The ability to define the fixed-point combinator in Haskell using recursion:

<haskell>
yet :: (a -> a) -> a
yet f = f (yet f)
</haskell>

means [https://dl.acm.org/doi/pdf/10.1145/99370.99404 parametricity is further restricted].
|- style="vertical-align:top;"
|4.
|Strictness must be considered when [https://ris.utwente.nl/ws/portalfiles/portal/284115323/thesis_M_Fokkinga.pdf deriving laws for various recursive algorithms] (see chapter 6).
|- style="vertical-align:top;"
|5.
|Similar to <code>seq</code> and <code>⊥</code>, the use of division and zero present their own challenges!
|}

Therefore all such claims against <code>seq</code> (or calls for its outright removal) should be examined <i>in this context</i>.