Notes on lambda calculus (part 2.7) and book Programming Distributed Computing Systems: A Foundational Approach by Varela present the sequencing combinator for normal order reduction:
$$\mathit{Seq} = \lambda x. \lambda y. ((\lambda z.y) \: x)$$
In the following example
$$((\mathit{Seq} \; (\text{display "hello"})) \; (\text{display "world"}))$$
it should guarantee that $(\text{display "hello"})$ is evaluated before $(\text{display "world"})$. But I don't understand why is $(\text{display "hello"})$ evaluated at all — why it isn't simply thrown away when evaluating
$$(\lambda z. (\text{display "world"})) \; (\text{display "hello"})$$
My reasoning: $z$ doesn't have free occurence in $(\text{display "world"})$ so substituting $(\text{display "hello"})$ for $z$ in $(\text{display "world"})$ results simply in $(\text{display "world"})$.
My question is related to Normal order sequencing vs applicative order sequencing.
seqis primitive in Haskell; it's not implementable as a lambda term. There are other things weird about this. It warns that "$z$ should not be free in $y$" but that makes no sense. $y$ is a bound variable. The only way $z$ could be free in $y$ is if $z = y$, but then why not worry about $y$ being free in $x$? If you want, you can makedisplayin Haskell usingunsafePerformIOand demonstrate thatdisplay "Hello"will not be evaluated. $\endgroup$se = \x -> \y -> ((\z -> y) x)followed by(se (putStrLn "hello") (putStrLn "world"))only prints "world" $\endgroup$putStrLn "hello"has been evaluated or not, only that it hasn't been executed.seq (putStrLn "hello") (putStrLn "world")will also not print "hello". (Technically, Haskell's evaluation is "non-strict" which gives it a lot of leeway in implementation, for example, it allows speculative evaluation. It wouldn't be incorrect for a Haskell implementation to evaluatedisplay "Hello"as in my previous comment. In practice, they don't, which is also a correct implementation of non-strictness.) $\endgroup$