<p>The section &quot;The <code>seq</code> Function&quot; on <a href="https://serokell.io/blog/haskell-to-core" rel="noreferrer">https://serokell.io/blog/haskell-to-core</a> mentions that</p>
<blockquote>
<p>The <code>seq</code> 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:</p>
</blockquote>
<pre><code>-- Haskell
seq a b

-- Core
case a of
  _ -&gt; b
</code></pre>
<p>But running the two versions of code in Haskell <a href="https://ato.pxeger.com/run?1=m708I7E4OzUnZ8GCpaUlaboWN2NyEzPzFGwVUvK5FBQKSkuCS4p88hQ0khOLUxVK81JS0zLzUlMU8tMUqhXiFXTtFJQ8gLrzlRRqNVHUF6cWIimHKtKE2AG1CmYlAA" rel="noreferrer">says otherwise</a>, i.e. it seems that <code>seq a b</code> is strict but <code>case a of _ -&gt; b</code> is not.</p>
<p>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?</p>

<semantics><haskell>
Semantics of Haskell's `seq`
CC BY-SA 4.0
2023-06-13T05:35:32.197Z
My understanding is that at surface level `case` is defined only to evaluate "as much as necessary" to determine the branch to take, though I don't know exactly how that's determined. That would be a semantic difference with Core, or at least a surface-level `case` need not translate to an equivalent `case` in Core. I don't know where that's specified.
Michael Homer
<p>The first comment under the question is <em>almost</em> correct.</p>
<p>What the <code>case</code> expression does is what is known as a &quot;conformality check&quot;; Haskell must evaluate enough of the expression to ensure that the pattern matches. Everything, including bottom, matches the pattern <code>_</code>, so no evaluation is forced.</p>
<p>Consider these two almost identical functions:</p>
<pre class="lang-haskell prettyprint-override"><code>f :: (Int,Int) -&gt; Int
f p = case p of
          _ -&gt; 0

g :: (Int,Int) -&gt; Int
g p = case p of
          (_,_) -&gt; 0
</code></pre>
<p>Here, <code>f undefined</code> returns <code>0</code>, but <code>g undefined</code> evaluates its argument.</p>
<p>Haskell also supports <em>irrefutable</em> 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).</p>
<pre class="lang-haskell prettyprint-override"><code>h :: (Int,Int) -&gt; Int
h p = case p of
          ~(a,b) -&gt; f a b

-- A possible desugaring:
h :: (Int,Int) -&gt; Int
h p = let e = p
          a = fst e
          b = snd e
      in f a b
</code></pre>
<p>In GHC Core, <code>case</code> expressions are the only constructs which force evaluation. So if evaluation is not needed in a <code>case</code> statement, GHC translates out that <code>case</code> when translating to Core.</p>
<pre class="lang-haskell prettyprint-override"><code>-- Haskell source code:
case a of
  _ -&gt; b

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

let _ = a in b
</code></pre>

CC BY-SA 4.0
2023-06-13T07:57:18.903Z
2023-06-15T00:36:40.313Z
2023-06-15T00:36:40.313Z
Pseudonym
CC BY-SA 4.0
2023-06-13T12:00:31.727Z
While this answers why `case` isn't always strict, it doesn't answer why `seq undefined b` hangs. IMO I think a combination of both our answers would be ideal, as mine explains the other half - why `seq` hangs here.
blueberry
CC BY-SA 4.0
2023-06-14T00:01:49.883Z
@blueberry Yeah, I didn't want to repeat what you said.
Pseudonym
<h1>TLDR: Because the Haskell report says so</h1>
<p>This is how <code>seq</code> is defined by the Haskell 98 report.</p>
<pre><code>The function seq is defined by the equations:
seq (bottom) b = (bottom)
seq a b = b, if a != (bottom)
</code></pre>
<p>This is on section <code>6.2</code> of the Haskell 98 report.
This does lead to the consequence that yes, <code>seq a b</code> != <code>case a of {_ -&gt; b}</code>, iff a == (bottom)</p>
<p>(bottom) is replacing the unicode symbol <code>⊥</code>, and is the type generated by nontermination - it cannot be inhabited by any actual value.</p>
<p>Therefore, your example is correct - GHC can and will optimise out the <code>case undefined ...</code>, but cannot optimise <code>seq undefined ...</code>.</p>
<p>This can be shown by having a look at the Core generated for</p>
<pre class="lang-haskell prettyprint-override"><code>main = do
  putStrLn (case undefined of { _ -&gt; &quot;Hello Case&quot; })
  putStrLn (seq undefined &quot;Hello Seq&quot;)
</code></pre>
<pre><code>main
  = src&lt;&lt;source&gt;:(3,1)-(5,38)&gt;
    &gt;&gt;
      ... ( cut out IO monad stuff ) ...

      (src&lt;&lt;source&gt;:4:3-52&gt;
       putStrLn
         (src&lt;&lt;source&gt;:4:12-52&gt;
          GHC.CString.unpackCString# &quot;Hello Case&quot;#))

      (src&lt;&lt;source&gt;:5:3-38&gt;
       putStrLn
         (src&lt;&lt;source&gt;:5:12-38&gt;
          case undefined
                 ... (cut out debugging info) ...
          of
          { __DEFAULT -&gt;
          src&lt;&lt;source&gt;:5:27-37&gt;
          GHC.CString.unpackCString# &quot;Hello Seq&quot;#
          }))
</code></pre>
<p>We can observe that the first <code>case undefined</code> has been eliminated, but the <code>seq</code> has not.</p>

CC BY-SA 4.0
2023-06-13T06:29:25.887Z
2023-06-13T06:50:58.640Z
2023-06-13T06:50:58.640Z
blueberry
<p>Do note that Haskell's <code>case</code> is different to Core's <code>case</code>.</p>
<p>Specifically, <code>case</code> in Haskell is not necessarily strict. <code>case e1 of x -&gt; e2</code> is just another way of writing a non-recursive let binding <code>let x = e1 in e2</code>.
It can also evaluate stuff deeply, for example <code>case e of ((), ()) -&gt; e2</code> will evaluate <code>e</code>, and the it will evaluate the components of the returned pair as well.</p>
<p>By contrast, Core's primitive <code>case</code> evaluates the scrutinee to weak-head normal form and subsequently does a shallow match (which is simply a <code>switch</code> in C). Nothing more, nothing less.</p>
<p>Of course, that means that Haskell's <code>case</code> cannot be translated 1-1 to Core's <code>case</code>.</p>
<p>In other words, your expectation is that</p>
<pre class="lang-hs prettyprint-override"><code>case a of
  _ -&gt; b
</code></pre>
<p>in Haskell has the same semantics as</p>
<pre><code>case a of _dead { __DEFAULT -&gt; b }
</code></pre>
<p>in Core, which is not the case.</p>

CC BY-SA 4.0
2024-06-24T14:31:38.400Z
2024-06-24T14:31:38.400Z
Sebastian Graf
# Semantics of Haskell's `seq`
Posted by: username_0 on 2023-06-13
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?
**Tags:** semantics haskell
> **Comments:**
> **username_1**: My understanding is that at surface level `case` is defined only to evaluate "as much as necessary" to determine the branch to take, though I don't know exactly how that's determined. That would be a semantic difference with Core, or at least a surface-level `case` need not translate to an equivalent `case` in Core. I don't know where that's specified.  
---
## 3 answers
### Answer by username_2 on 2023-06-13. Score: 5
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
> **Comments:**
> **username_3** (2023-06-13): While this answers why `case` isn't always strict, it doesn't answer why `seq undefined b` hangs. IMO I think a combination of both our answers would be ideal, as mine explains the other half - why `seq` hangs here.  
> **username_2** (2023-06-14): @blueberry Yeah, I didn't want to repeat what you said.  
---
### Answer by username_3 on 2023-06-13. Score: 5
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<:(3,1)-(5,38)>
    >>
      ... ( cut out IO monad stuff ) ...

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

      (src<:5:3-38>
       putStrLn
         (src<:5:12-38>
          case undefined
                 ... (cut out debugging info) ...
          of
          { __DEFAULT ->
          src<: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 by username_4 on 2024-06-24. Score: 2
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.
---
