How do let and case differ in terms of lazyness?

How do let and case differ in terms of lazyness? Where do I find the information myself? And how do I experiment with it in ghci?

Some context

This incomplete piece of code is an excerpt from Parallel and Concurrent Programming in Haskell, specifically the section An Alternative Channel Implementation,

readTQueue :: TQueue a -> STM a
readTQueue (TQueue read write) = do
  xs <- readTVar read
  case xs of
    (x:xs') -> do writeTVar read xs'
                  return x
    [] -> do ys <- readTVar write
             case ys of
               [] -> retry
               _  -> do let (z:zs) = reverse ys
                        writeTVar write []
                        writeTVar read zs
                        return z

Marlow comments that

There is one subtlety here: we must be careful that the reverse is done lazily, which is why we use a let rather than case here. If we were to pattern-match on the result of the reverse strictly, the STM transaction could not complete until the reverse finished (see Performance).

I assume the alternative code would have looked like this (rewriting only the last 4 lines):

               _  -> case reverse ys of
                       (z:zs) -> do writeTVar write []
                                    writeTVar read zs
                                    return z
                       _ -> error "this is a programming error, i.e this should never happen"

Assuming that the last snippet is the alternative code that Marlow alludes to (if not, please, correct me), why would using case cause an eager evaluation of the whole list reverse ys? Where do I read this myself?

I've tried using :sprint (which I've seen for the first time reading this book, after 5 years since my first contact with Haskell, believe it or not) to experiment with let and case and work out the answer, but I haven't come up with anything senseible.

And by the way,

• let x = … in … is a let expression, right? But what is let x = … in a do expression called?

Is that last snippet the alternative code that Marlow alludes to? If not, what is it?

Yes, that's the right snippet to compare to.

Why using case should cause an eager evaluation of the whole list reverse ys? Where do I read this myself? In C++, I try to read the standard draft, but what about Haskell? Is it this one?

Yes, the Haskell Report is the canonical specification. (But see also the "Known Bugs and Infelicities -> Haskell standards vs. Glasgow Haskell: language non-compliance" section of the GHC manual.) The relevant paragraph of the Report for case is in section 3.13:

A case expression is evaluated by pattern matching the expression e against the individual alternatives. The alternatives are tried sequentially, from top to bottom.

The (implied) consequence of this is that the scrutinee must be evaluated far enough to know if an alternative matches. This won't in general require a full evaluation, but this case is special: it calls reverse, whose definition is given in section 9.1, and which does not produce its first constructor until it has processed the entire spine of its input.

The relevant paragraph for let is in section 3.12, and makes the difference abundantly clear:

The dynamic semantics of the expression let { d1 ; … ; dn } in e0 are captured by this translation: ...

let p = e1 in e0 = case e1 of ~p -> e0 where no variable in p appears free in e1

The ~ in the case translation makes the match lazy.

I've tried using :sprint (which I've seen for the first time reading this book, after 5 years since my first contact with Haskell, believe it or not) to experiment with let and case and work out the answer, but I haven't come up with anything senseible.

Here's a short ghci transcript demonstrating the difference.

> x = "abcde"
> case reverse x of _:_ -> ()
()
> :sprint x
x = "abcde" -- actually, this is an optimization; the spec only requires [_, _, _, _, _]
> x = "abcde"
> let _:_ = reverse x in ()
()
> :sprint x
x = _ -- not yet evaluated

let x = … in … is a let expression, right? But what is let x = … in a do expression called?

If I needed to draw this distinction, I would name it a let statement.