2
$\begingroup$

I'm trying to understand this lecture, section 2.7. Why would the normal order sequencing print out "hello" "world" and not "world" "hello"? I may be misinterpreting the order in which the arguments are applied.

It looks like the expression

$$ ((Seq (display "hello"))\; (display "world")) $$

would evaluate to

$$ \lambda z.((display "world")\; (display "hello")) $$

and that would, under normal order, would print out "world" "hello".

My question is whether the assumption I'm making is correct. If not, could you show the correct derivation of the end-expression?

$\endgroup$
7
$\begingroup$

You're misreading the combinator. In these lecture notes, lambda abstraction binds tighter than application (the opposite convention is more common — it's apparent from the spacing but the author should state that explicitly). I'll use extra (redundant) parentheses in my answers to avoid any potential for ambiguity. The combinator is $$ \mathit{Seq} = \lambda x. \lambda y. ((\lambda z.y) \: x)$$ So $$ \begin{align} & ((\mathit{Seq} \; (\text{display "hello"})) \; (\text{display "world"})) \\ &\qquad = (((\lambda x. \lambda y. ((\lambda z.y) \; x)) \; (\text{display "hello"})) \; (\text{display "world"})) \\ &\qquad \to^2 ((\lambda z. (\text{display "world"})) \; (\text{display "hello"})) \\ &\qquad \xrightarrow{\text{display "hello"}} (\text{display "world"}) \\ &\qquad \xrightarrow{\text{display "world"}} \mathord{?} \\ \end{align} $$ where $M \xrightarrow{\text{action}} N$ means that $M$ evaluates to $N$ performing the specified action.

$\endgroup$
  • $\begingroup$ I think this question reveals that Seq doesn't work as it should. $\endgroup$ – Anton Trunov Apr 25 '16 at 6:22
  • $\begingroup$ @AntonTrunov It works but the semantics is bizarre, since display is basically evaluated in applicative order. And I don't see that specified in the lecture notes. $\endgroup$ – Gilles 'SO- stop being evil' Apr 25 '16 at 12:16
  • $\begingroup$ Then why "hello" doesn't get printed after the first $\beta$-reduction? (when we substitute (display "hello") for $x$)). $\endgroup$ – Anton Trunov Apr 25 '16 at 12:24
  • $\begingroup$ A quote from the notes: "This combinator guarantees that $x$ is evaluated before $y$, which is important in programs with side-effects." I understand it as -- Seq is a "universal" combinator, so it should work not only for display (it's for the case when we make (display ...) a special form). $\endgroup$ – Anton Trunov Apr 25 '16 at 12:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.