27  Lazy Evaluation

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferrule}[3][]{ \let\and\qquad \begin{array}{@{}l@{}} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

We have seen short-circuiting evaluation (Section 21.6), which is a particular instance of lazy evaluation where some sub-expression is conditionally evaluated.

In this chapter, we consider call-by-name, which is another of form of lazy evaluation in defining the semantics of function call \(e_1\texttt{(}e_2\texttt{)}\). In contrast to call-by-value, call-by-name semantics does not evaluate the function argument to a value before starting to evaluate the function body. Instead, it takes the unevaluated argument expression and substitutes it for the formal parameter.

Consider two possible \(\TirName{DoCall}\) rules:

\(\inferrule[DoCallByValue]{ }{ (\texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(} v_2 \texttt{)} \longrightarrow {}[v_2/x]e_1 }\)

\(\inferrule[DoCallByName]{ }{ (\texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(} e_2 \texttt{)} \longrightarrow {}[e_2/x]e_1 }\)

It is one tiny difference on paper that is a substantively different semantically. The \(\TirName{DoCallByValue}\) rule requires that the argument be eagerly evaluated to a value before applying the substitution, while the \(\TirName{DoCallByName}\) rule does not. Call-by-name is lazy in that if \(e_1\) does not end up using the parameter \(x\) in the subsequent evaluation, then \(e_2\) will not be evaluated (i.e., like being “short-circuited”).

27.1 TypeScripty: Call-By-Name Parameters

Let us consider TypeScripty with functions (Section 26.5) and extend it with call-by-name parameters. Note that TypeScript does not have call-by-name parameters, so this is an extension beyond TypeScript.

27.1.1 Syntax

Let us consider the abstract syntax of TypeScripty with numbers and functions extended with parameter-passing modes:

\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{number}\mid\texttt{(}x\texttt{:}\, d\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \\ \text{values} & v& \mathrel{::=}& n\mid\texttt{(}x\texttt{:}\, d\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& n\mid\texttt{(}x\texttt{:}\, d\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid x \mid e_1\texttt{(}e_2\texttt{)} \mid d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \\ \text{parameter modes} & d& \mathrel{::=}& \mathbf{const}\mid\mathbf{name} \end{array} \]

Figure 27.1: Syntax of TypeScripty with number literals, function literals with parameter modes, and variable declarations, and function call expressions.

Function parameters are annotated with a mode \(d\) to be either call-by-value (\(\mathbf{const}\)) or call-by-name (\(\mathbf{name}\)). To emphasize that variable binding can be encoded as a function call and a function literal, we introduce the variable binding expression as declaring a variable with a mode (\(d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2\)). That is, variables can be bound by value (\(\mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2\)) or by name (\(\mathbf{name}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2\)).

Note that most languages have a default parameter-passing mode (e.g., by value in the case of JavaScript/TypeScript), so the concrete syntax may leave the mode declaration optional.

We can represent the abstract syntax of TypeScripty with parameter-passing modes in Scala as follows:

trait Typ                                                  // τ
case object TNumber extends Typ                            // τ ::= number
case class TFun(xt: (String, MTyp), tret: Typ) extends Typ // τ ::= (x: m τ) => τ'

case class MTyp(m: Mode, t: Typ) // m τ 

trait Mode                      // m
case object MConst extends Mode // m ::= const
case object MName extends Mode  // m ::= name

trait Expr                                                           // e
case class N(n: Double) extends Expr                                 // e ::= n
case class Fun(xt: (String, MTyp), e1: Expr) extends Expr            // e ::= (x: m τ) => e1
case class Var(x: String) extends Expr                               // e ::= x
case class Call(e1: Expr, e2: Expr) extends Expr                     // e ::= e1(e2)
case class Decl(m: Mode, x: String, e1: Expr, e2: Expr) extends Expr // e ::= m x = e1; e2

def isValue(e: Expr): Boolean = e match {
  case N(_) | Fun(_, _) => true
  case _ => false
}

defined trait Typ
defined object TNumber
defined class TFun
defined class MTyp
defined trait Mode
defined object MConst
defined object MName
defined trait Expr
defined class N
defined class Fun
defined class Var
defined class Call
defined class Decl
defined function isValue

We use the MTyp constructor for the pair of a mode \(d\) and a type \(\tau\) for clarity.

27.1.2 Small-Step Operational Semantics

Let us consider the small-step operational semantics of TypeScripty with parameter-passing modes:

\(\fbox{$e \longrightarrow e'$}\)

\(\inferrule[DoCallByValue]{ }{ (\texttt{(}x\texttt{:}\, \mathbf{const}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}v_2\texttt{)} \longrightarrow{}[v_2/x]e_1 }\)

\(\inferrule[DoCallByName]{ }{ (\texttt{(}x\texttt{:}\, \mathbf{name}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow{}[e_2/x]e_1 }\)

\(\inferrule[SearchCall1]{ e_1 \longrightarrow e_1' }{ e_1\texttt{(}e_2\texttt{)} \longrightarrow e_1'\texttt{(}e_2\texttt{)} }\)

\(\inferrule[SearchCall2]{ e_2 \longrightarrow e_2' }{ (\texttt{(}x\texttt{:}\, \mathbf{const}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow (\texttt{(}x\texttt{:}\, \mathbf{const}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1)\texttt{(}e_2'\texttt{)} }\)

\(\inferrule[DoConstDecl]{ }{ \mathbf{const}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 \longrightarrow {}[v_1/x]e_2 }\)

\(\inferrule[DoNameDecl]{ }{ \mathbf{name}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow {}[e_1/x]e_2 }\)

\(\inferrule[SearchConstDecl]{ e_1 \longrightarrow e_1' }{ \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow\mathbf{const}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 }\)

Figure 27.2: Small-step operational semantics of TypeScripty with number literals, function literals with parameter modes, variable declarations, and function call expressions.

Depending on the declared parameter-passing mode, either \(\TirName{DoCallByValue}\) or \(\TirName{DoCallByName}\) applies. Only \(\TirName{SearchCall1}\) is needed for call-by-name, so \(\TirName{SearchCall2}\) only applies for \(\mathbf{const}\) parameters.

We see the parallel of \(\TirName{DoConstDecl}\) and \(\TirName{DoNameDecl}\) with \(\TirName{DoCallByValue}\) and \(\TirName{DoCallByName}\), respectively. Similarly, \(\TirName{SearchConstDecl}\) matches up with \(\TirName{SearchCall2}\).

def subst(v: Expr, x: String, e: Expr) = {
  def subst(e: Expr): Expr = e match {
    case N(_) => e
    case Fun(yt @ (y, _), e1) => if (x == y) e else Fun(yt, subst(e1))
    case Var(y) => if (x == y) v else e
    case Call(e1, e2) => Call(subst(e1), subst(e2))
    case Decl(m, y, e1, e2) => Decl(m, y, subst(e1), if (x == y) e2 else subst(e2))
  }
  subst(e)
}

defined function subst

def step(e: Expr): Expr = {
  require(!isValue(e))
  e match {
    // DoCallByValue
    case Call(Fun((x, MTyp(MConst, _)), e1), v2) if isValue(v2) => subst(v2, x, e1)
    // DoCallByName
    case Call(Fun((x, MTyp(MName, _)), e1), e2) => subst(e2, x, e1)
    // SearchCall2
    case Call(v1 @ Fun((_, MTyp(MConst, _)), _), e2) => Call(v1, step(e2))
    // SearchCall1
    case Call(e1, e2) => Call(step(e1), e2)
    // DoConstDecl
    case Decl(MConst, x, v1, e2) if isValue(v1) => subst(v1, x, e2)
    // DoNameDecl
    case Decl(MName, x, e1, e2) => subst(e1, x, e2)
    // SearchConstDecl
    case Decl(MConst, x, e1, e2) => Decl(MConst, x, step(e1), e2)
  }
}

defined function step

We see that we can generalize slightly by defining a judgment form \(d\;\vdash e\;\mathsf{redex}\) to determine whether an actual argument expression \(e\) is reducible for a given parameter-passing mode \(d\). This helper judgment is then used for both \(\TirName{SearchCall2}\) and \(\TirName{SearchDecl}\) to reduce the argument expression as needed before applying the substitution in \(\TirName{DoCall}\) and \(\TirName{DoDecl}\), respectively:

\(\fbox{$e \longrightarrow e'$}\)

\(\inferrule[DoCall]{ d\;\nvdash e_2\;\mathsf{redex} }{ (\texttt{(}x\texttt{:}\, d\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow{}[e_2/x]e_1 }\)

\(\inferrule[SearchCall1]{ e_1 \longrightarrow e_1' }{ e_1\texttt{(}e_2\texttt{)} \longrightarrow e_1'\texttt{(}e_2\texttt{)} }\)

\(\inferrule[SearchCall2]{ d\;\vdash e_2\;\mathsf{redex} \and e_2 \longrightarrow e_2' }{ (\texttt{(}x\texttt{:}\, d\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow (\texttt{(}x\texttt{:}\, d\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1)\texttt{(}e_2'\texttt{)} }\)

\(\inferrule[DoDecl]{ d\;\nvdash e_1\;\mathsf{redex} }{ d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow {}[e_1/x]e_2 }\)

\(\inferrule[SearchDecl]{ d\;\vdash e_1\;\mathsf{redex} \and e_1 \longrightarrow e_1' }{ d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow d\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 }\)

We write \(d\;\nvdash e\;\mathsf{redex}\) for the judgment form when an actual argument expression \(e\) is not reducible for a given parameter-passing mode \(d\):

\(\fbox{$d\;\vdash e\;\mathsf{redex}$}\)

\(\inferrule[ConstMode]{ e\neq v }{ \mathbf{const}\;\vdash e\;\mathsf{redex} }\)

\(\fbox{$d\;\nvdash e\;\mathsf{redex}$}\)

\(\inferrule[NameMode]{ }{ \mathbf{name}\;\nvdash e\;\mathsf{redex} }\)

We can the \(d\;\vdash e\;\mathsf{redex}\) and \(d\;\nvdash e\;\mathsf{redex}\) judgment forms by defining a helper function isRedex that we use in a slightly more generalized version of step:

def isRedex(m: Mode, e: Expr): Boolean = m match {
  case MConst => !isValue(e)
  case MName => false
}

def step(e: Expr): Expr = {
  require(!isValue(e))
  e match {
    // DoCall
    case Call(Fun((x, MTyp(m, _)), e1), e2) if !isRedex(m, e2) => subst(e2, x, e1)
    // SearchCall2
    case Call(v1 @ Fun((_, MTyp(m, _)), _), e2) if isRedex(m, e2) => Call(v1, step(e2))
    // SearchCall1
    case Call(e1, e2) => Call(step(e1), e2)
    // DoDecl
    case Decl(m, x, e1, e2) if !isRedex(m, e1) => subst(e1, x, e2)
    // SearchDecl
    case Decl(m, x, e1, e2) if isRedex(m, e1) => Decl(m, x, step(e1), e2)
  }
}

defined function isRedex
defined function step

27.1.3 Static Typing

We see that call-by-name is a small change in the run-time of the language and thus the changes manifest in the operational semantics. The static semantics essentially stay the same as before, ignoring the \(\mathbf{const}\) or \(\mathbf{name}\) modes.

Exercise 27.1 Define the typing judgment \(\Gamma \vdash e : \tau\) for the above language.