Thank you Tarik, you're spot-on correct.

It's better to try to model execution using lambda calculus.

The most dominant factor in languages like Haskell is lambda calculus. Think through lambda calculus for a mental model.

I presume it's this advice that Michael is complaining about in his long comment on the cafe yesterday. In particular, Haskell is unusual even amongst functional programming languages in its lazy evaluation. So to try to correct Michael's misunderstanding:

...

When I write C, or even C++, I have a mental model of how execution will proceed.

Firstly, 'execution' in Haskell does not proceed in anything like the sequence-of-steps and update-of-locations/frame-on-the-stack of C or C++ (or Fortran or ALGOL or COBOL or ...). In particular, 'variables' in Haskell are not overwritable locations in the sense of a procedural language. Variables are just a name for an expression (might be a lambda expression). This is what we mean by 'referential transparency' that procedural languages do not have. We can replace any variable by the expression it denotes, or by any other equivalent expression. Secondly, there's an important theorem (Church-Rosser) in Lambda calculus [see wikipedia], that if Beta-reduction terminates, it'll produce the same 'reduced form' of the initial expression whether it proceeds inside-out or outside-in or both-sides-to-the-middle. You don't need to second-guess how the compiler proceeds, because you don't need to know. You do need to understand Beta-reduction (that's easy). You also need to understand why Alpha-renaming is needed hand-in-hand with Beta-reduction (not so easy, but work a few examples with a recursive function, such as stepping through a list). And you need to stop immediately trying to imagine Haskell semantics as some sort of crazy Turing machine: you'll go mad. Turing himself [1937] proved the semantics are equivalent; but that paper is impenetrable for ordinary mortals like me.