Semantics of Haskell's `seq`

Question

The section "The seq Function" on https://serokell.io/blog/haskell-to-core mentions that

The seq function, which forces evaluation of its argument to weak-head normal form, is desugared into a case-expression, relying on the fact that in Core, case-expressions are strict:

-- Haskell
seq a b

-- Core
case a of
  _ -> b

But running the two versions of code in Haskell says otherwise, i.e. it seems that seq a b is strict but case a of _ -> b is not.

Is this a difference in semantics between Haskell and Core? If so, is there some rationale for the behavior in Haskell being different from Core?

Answer 1

TLDR: Because the Haskell report says so

This is how seq is defined by the Haskell 98 report.

The function seq is defined by the equations:
seq (bottom) b = (bottom)
seq a b = b, if a != (bottom)

This is on section 6.2 of the Haskell 98 report. This does lead to the consequence that yes, seq a b != case a of {_ -> b}, iff a == (bottom)

(bottom) is replacing the unicode symbol ⊥, and is the type generated by nontermination - it cannot be inhabited by any actual value.

Therefore, your example is correct - GHC can and will optimise out the case undefined ..., but cannot optimise seq undefined ....

This can be shown by having a look at the Core generated for

main = do
  putStrLn (case undefined of { _ -> "Hello Case" })
  putStrLn (seq undefined "Hello Seq")

main
  = src<<source>:(3,1)-(5,38)>
    >>
      ... ( cut out IO monad stuff ) ...

      (src<<source>:4:3-52>
       putStrLn
         (src<<source>:4:12-52>
          GHC.CString.unpackCString# "Hello Case"#))

      (src<<source>:5:3-38>
       putStrLn
         (src<<source>:5:12-38>
          case undefined
                 ... (cut out debugging info) ...
          of
          { __DEFAULT ->
          src<<source>:5:27-37>
          GHC.CString.unpackCString# "Hello Seq"#
          }))

We can observe that the first case undefined has been eliminated, but the seq has not.

Answer 2

The first comment under the question is almost correct.

What the case expression does is what is known as a "conformality check"; Haskell must evaluate enough of the expression to ensure that the pattern matches. Everything, including bottom, matches the pattern _, so no evaluation is forced.

Consider these two almost identical functions:

f :: (Int,Int) -> Int
f p = case p of
          _ -> 0

g :: (Int,Int) -> Int
g p = case p of
          (_,_) -> 0

Here, f undefined returns 0, but g undefined evaluates its argument.

Haskell also supports irrefutable patterns which defer the pattern match to where it is actually needed. Note that irrefutable patterns only really make sense on product types (e.g. records or tuples).

h :: (Int,Int) -> Int
h p = case p of
          ~(a,b) -> f a b

-- A possible desugaring:
h :: (Int,Int) -> Int
h p = let e = p
          a = fst e
          b = snd e
      in f a b

In GHC Core, case expressions are the only constructs which force evaluation. So if evaluation is not needed in a case statement, GHC translates out that case when translating to Core.

-- Haskell source code:
case a of
  _ -> b

-- The above may desugar to something more like this:

let _ = a in b

Answer 3

Do note that Haskell's case is different to Core's case.

Specifically, case in Haskell is not necessarily strict. case e1 of x -> e2 is just another way of writing a non-recursive let binding let x = e1 in e2. It can also evaluate stuff deeply, for example case e of ((), ()) -> e2 will evaluate e, and the it will evaluate the components of the returned pair as well.

By contrast, Core's primitive case evaluates the scrutinee to weak-head normal form and subsequently does a shallow match (which is simply a switch in C). Nothing more, nothing less.

Of course, that means that Haskell's case cannot be translated 1-1 to Core's case.

In other words, your expectation is that

case a of
  _ -> b

in Haskell has the same semantics as

case a of _dead { __DEFAULT -> b }

in Core, which is not the case.