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.

  • 3
    $\begingroup$ It's just wrong. Your reasoning is correct even with their definitions. There's a reason seq is 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 make display in Haskell using unsafePerformIO and demonstrate that display "Hello" will not be evaluated. $\endgroup$ Apr 25, 2016 at 1:59
  • 1
    $\begingroup$ It can be made to work, but it requires complicated definitions that aren't in that document. Your reasoning is correct for a “reasonable” definition of the semantics of $(\mathrm{display} \: s)$. $\endgroup$ Apr 25, 2016 at 12:18
  • $\begingroup$ @Gilles: could you be more specific as to what would be necessary for it to work? $\endgroup$
    – Jay
    Apr 25, 2016 at 22:03
  • $\begingroup$ I tend to agree with the OP: the following Haskell program, se = \x -> \y -> ((\z -> y) x) followed by (se (putStrLn "hello") (putStrLn "world")) only prints "world" $\endgroup$
    – Jay
    Apr 25, 2016 at 22:13
  • $\begingroup$ @Jay That is not a good example. It doesn't tell you whether 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 evaluate display "Hello" as in my previous comment. In practice, they don't, which is also a correct implementation of non-strictness.) $\endgroup$ Apr 27, 2016 at 5:12


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.