23 Review: Semantics

$\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}} $

Instructions

This assignment is a review exercise in preparation for a subsequent assessment activity.

This is a peer-quizzing activity with two students. Each section has an even number of exercises. Student A quizzes Student B on the odd numbered exercises, and Student B quizzes Student A on the even numbered exercises.

To the best of your ability, give feedback using the learning-levels rubric below on where your peer is in reaching or exceeding Proficient (P) on each question live. Guidance of what a Proficient (P) answer looks like are given.

There may or may not be a member of the course staff assigned to your slot. It is expected that regardless of whether a member of the course staff is present, this is a peer-quizzing activity. If a member of the course staff is present, you may ask for their help and guidance on answering the questions and/or their assessment of where you are at in your learning level.

It is not expected that you can complete all exercises in the allotted time. You and your partner may pick and choose which sections you want to focus on and use the remaining questions as a study guide. You and your partner may, of course, continue working together after the scheduled session.

At the same time, most questions can be answered in a few minutes with a Proficient (P) level of understanding. Aim for 3–4 sections in 30 minutes.

Your submission for this session is an overall assessment of where your partner is in their reaching-or-exceeding-proficiency level. Be constructive and honest. Neither your nor your partners grade will depend on your learning-level assessment. Instead, your score for this assignment will be based on the thoughtfulness of your feedback to your partner.

Submit on Gradescope as a pair. That is, use Gradescope’s group assignment feature to submit as a group. The submission form has a spot for each of you to provide your assessment and feedback for each other.

Please proactively fill slots with an existing sign-up to have a partner. In case your peer does not show up to the slot, try to join another slot happening at the same time from the course calendar. If that fails and a course staff member is present, you may do the exercise with the staff member and get credit. If there is no staff member present, you may try to find a slot at a later time if you like or else write to the Course Manager on Piazza timestamped during the slot.

Learning-Levels Rubric

4 - Exceeding (E): Student demonstrates synthesis of the underlying concepts. Student can go beyond merely describing the solution to explaining the underlying reasoning and discussing generalizations.
3 - Proficient (P): Student is able to explain the overall solution and can answer specific questions. While the student is capable of explaining their solution, they may not be able to confidently extend their explanation beyond the immediate context.
2 - Approaching (A): Student may able to describe the solution but has difficulty answering specific questions about it. Student has difficulty explaining the reasoning behind their solution.
1 - Novice (N): Student has trouble describing their solution or responding to guidance. Student is unable to offer much explanation of their solution.

23.1 Dynamic versus Static Scoping

Exercise 23.1 Consider the following JavaScripty code. What is the resulting value you would expect from an interpreter that implements dynamic scoping? What about one that implements static scoping? Explain.

const x = 4;
const f = (y) => x * 2;
((x) => f(5))(8)

A Proficient (P) answer recognizes that the resulting value is different under dynamic versus static scoping. It discusses that this difference is due to the fact that an interpreter that implements dynamic scoping would evaluate the function (y) => x * 2 (which is bound to f) with the value environment at the time it is called, instead of the environment at the time it is defined. Static scoping, which is what we usually expect, evaluates functions with the value environment in which they were defined in.

An Exceeding (E) answer also explains how dynamic scoping arises accidentally in an interpreter that uses value environments, perhaps by giving an operational semantics rule for function call that exhibits dynamic scoping.

Exercise 23.2 Consider the following inference rules which define a big-step or small-step operational semantics for non-recursive function literals and function call expressions. For each one, write if it implements dynamic scoping or static scoping. Choose one rule to explain fully. In this explanation, discuss why the rule does or does not implement dynamic scoping. Also write out what each aspect of the rule is stating.

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

$\inferrule[DoCall]{ }{ (\texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}v_2\texttt{)} \longrightarrow{}[v_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' }{ v_1 \texttt{(}e_2\texttt{)} \longrightarrow v_1 \texttt{(}e_2'\texttt{)} }$

$\fbox{$E \vdash e \Downarrow v$}$

$\inferrule[EvalCall]{ E \vdash e_1 \Downarrow \texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e' \and E \vdash e_2 \Downarrow v_2 \and E[x \mapsto v_2] \vdash e' \Downarrow v' }{ E \vdash e_1\texttt{(}e_2\texttt{)} \Downarrow v' }$

$\fbox{$E \vdash e \Downarrow v$}$

$\inferrule[EvalFun]{ }{ E \vdash \texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e \Downarrow \texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e [ E] }$

$\inferrule[EvalCall]{ E \vdash e_1 \Downarrow \texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e'[E'] \and E \vdash e_2 \Downarrow v_2 \and E'[x \mapsto v_2] \vdash e' \Downarrow v' }{ E \vdash e_1\texttt{(}e_2\texttt{)} \Downarrow v' }$

$\fbox{$e \Downarrow v$}$

$\inferrule[EvalCall]{ e_1 \Downarrow \texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e' \and e_2 \Downarrow v_2 \and {}[v_2/x]e' \Downarrow v' }{ e_1\texttt{(}e_2\texttt{)} \Downarrow v' }$

A Proficient (P) answer correctly states which rules implement dynamic scoping (2) and which do not (1, 3, 4). For the explanation, it explains what general strategy is used (e.g., big-step with value environments and closures) and why or why not does this strategy result in dynamic scoping. For example, using closures results in static scoping because the value environment in which the function was defined is saved in the closure. When functions are called, the value environment from the closure is extended with the parameter, and then the body is evaluated. A Proficient (P) answer also correctly states each aspect of the premise and conclusion of the rule.

23.2 Small-Step Semantics with Coercions

We consider a subset of JavaScripty that includes variables ($x$), variable binding ($\mathbf{const}$), arithmetic plus ($\texttt{+}$), arithmetic negation ($\mathop{\texttt{-}} $), boolean conjunction ($\texttt{\&\&}$), and boolean negation ($\mathop{\texttt{!}} $). The values of our language are numbers ($n$) and booleans ($b$). Below is the abstract syntax.

\[ \begin{array}{rrrll} \text{expressions} & e& \mathrel{::=}& x \mid\mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \mid e_1 \mathbin{\mathit{bop}}e_2 \mid\mathop{\mathit{uop}}e_1 \mid n\mid b \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{+} \mid\texttt{\&\&} \\ \text{unary operators} & \mathit{uop}& \mathrel{::=}& \texttt{-} \mid\texttt{!} \\ \text{values} & v& \mathrel{::=}& n\mid b \\ \text{variables} & x \end{array} \]

Figure 23.1: Syntax for JavaScripty with variables and some minimal arithmetic and boolean expressions.

Our rules for coercing a value to a number are as follows.

$\fbox{$v \rightsquigarrow n$}$

$\inferrule[ToNumberNum]{ }{ n \rightsquigarrow n }$

$\inferrule[ToNumberTrue]{ }{ \mathbf{true} \rightsquigarrow 1 }$

$\inferrule[ToNumberFalse]{ }{ \mathbf{false} \rightsquigarrow 0 }$

Exercise 23.3 Define the judgment form $v \rightsquigarrow b$. That is, write the inference rules for coercing a value to a boolean. Recall $\texttt{0}$ coerces to $\mathbf{false}$, and anything else coerces to $\mathbf{true}$.

A Proficient (P) answer correctly gives two rules. All rules are not inductive (i.e., do not have a $v \rightsquigarrow b$ judgment in the premise). For clarity, the judgment form should be given in a box above the rules.

Exercise 23.4 Write the $\TirName{Search}$ and $\TirName{Do}$ rules for stepping a $\mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2$ expression and a variable-use expression $x$. Our small-step judgment form is $e \longrightarrow e'$ that says, “Closed expression $e$ reduces to closed-expression $e'$ in one step.”

A Proficient (P) answer writes two correct rules. The rules are $\TirName{DoConst}$ and $\TirName{SearchConst}$. $\TirName{DoConst}$ should require that $e_1$ is a value, then step to $e_2$ with a substitution for the binding of variable $x$.

An Exceeding (E) answer writes all of the rules correctly, recognizes why we do not need a $\TirName{Do}$ rule for variable uses, and understands why substitution enables us to maintain the invariant that $e$ and $e'$ in $e \longrightarrow e'$ are closed expressions. There is no $\TirName{Do}$ rule for variable uses because expression $e$ must be a closed expression.

Below is a small-step operational semantics for stepping unary expressions:

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

$\inferrule[DoNeg]{ v_1 \rightsquigarrow n_1 }{ \mathop{\texttt{-}} v_1 \longrightarrow- n_1 }$

$\inferrule[DoNot]{ v_1 \rightsquigarrow b_1 }{ \mathop{\texttt{!}} v_1 \longrightarrow\neg b_1 }$

$\inferrule[SearchUnary]{ e_1 \longrightarrow e_1' }{ \mathop{\mathit{uop}}e_1 \longrightarrow\mathop{\mathit{uop}}e_1' }$

Figure 23.2: A small-step operational semantics for the unary expressions.

Exercise 23.5 Complete the inductive definition of $e \longrightarrow e'$ by writing the $\TirName{Search}$ and $\TirName{Do}$ rules for stepping binary expressions. You need to write two $\TirName{Search}$ rules and two $\TirName{Do}$ rules.

An Proficient (P) answer writes four or five rules. There should be two $\TirName{Search}$ rules that should include a premise that one side of the binary expression takes a step. The $\TirName{Do}$ rules should probably use coercions following the example for unary expressions (e.g., $v_1 \rightsquigarrow n_1$).

An Exceeding (E) answer will consider different semantic choices. For the $\TirName{Search}$ rules, the answers can consider left-to-right evaluation, right-to-left evaluation, or non-deterministic evaluation. Such an answer will explain that a deterministic left-to-right or right-to-left would require the other side of the binary expression is already a value. For the $\TirName{DoAnd}$ rule(s), an Exceeding (E) answer will consider whether to implement short-circuiting or not.

Note that one possible correct solution for the rules asked about in the above exercises are given in the preceding chapters (cf. Chapter 21 or Section 22.5)

Exercise 23.6 Consider the following expression $e_0$:

\[ \mathbf{const}\;\texttt{h}\;\texttt{=}\;\mathbf{true}\texttt{;}\; \texttt{(}\texttt{h} \mathbin{\texttt{+}} \texttt{3}\texttt{)} \mathbin{\texttt{\&\&}} \mathbf{false} \]

Then, is the judgment

\[ \mathbf{const}\;\texttt{h}\;\texttt{=}\;\mathbf{true}\texttt{;}\; \texttt{(}\texttt{h} \mathbin{\texttt{+}} \texttt{3}\texttt{)} \mathbin{\texttt{\&\&}} \mathbf{false} \longrightarrow e_1 \]

for some expression $e_1$ derivable using your rules? If so, give the derivation with the appropriate $e_1$.

Then, is the judgment $e_1 \longrightarrow e_2$ derivable using your rules? If so, give the derivation with the appropriate $e_2$.

Repeat until giving derivations for $e_i \longrightarrow e_{i+1}$ until the step-judgment is not derivable. Explain why this last step-judgment is not derivable.

Explain how these derivations are connected to your interpreter implementation of these rules from the lab assignment.

A Proficient (P) shows derivations for the judgments \[ \mathbf{const}\;\texttt{h}\;\texttt{=}\;\mathbf{true}\texttt{;}\; \texttt{(}\texttt{h} \mathbin{\texttt{+}} \texttt{3}\texttt{)} \mathbin{\texttt{\&\&}} \mathbf{false} \longrightarrow \texttt{(}\mathbf{true} \mathbin{\texttt{+}} \texttt{3}\texttt{)} \mathbin{\texttt{\&\&}} \mathbf{false} \] \[ \texttt{(}\mathbf{true} \mathbin{\texttt{+}} \texttt{3}\texttt{)} \mathbin{\texttt{\&\&}} \mathbf{false} \longrightarrow \texttt{4} \mathbin{\texttt{\&\&}} \mathbf{false} \] \[ \texttt{4} \mathbin{\texttt{\&\&}} \mathbf{false} \longrightarrow \mathbf{false} \] It should state that there is no deriviation for the judgment $\mathbf{false} \longrightarrow e_4$ for any expression $e_4$ because the step-judgment form defines a reduction step and $\mathbf{false}$ is a value. Note that a Proficient (P) answer may give different judgments here corresponding to a different evaluation-order semantics. The particular judgments should correspond to the given rules. Each of the derivations has some number of $\TirName{Search}$ rule applications and ends with a $\TirName{Do}$ rule application as an axiom (reading from the bottom up).

Regarding the interpreter implementation, a Proficient (P) answer should also recognize that a judgment $e_i \longrightarrow e_{i+1}$ corresponds to a call of step. An Exceeding (E) answer recognizes that each application of a $\TirName{Search}$ rule corresponds to a recursive call of step and observes that there is only one recursive call in each $\TirName{Search}$ rule to find the redex in which to apply a $\TirName{Do}$ rule.

23.3 Short-Circuit Evaluation and Evaluation Order

Exercise 23.7 Does the rule you wrote in Exercise 23.5 for $\texttt{\&\&}$ short circuit? Explain why or why not. If it does, rewrite the rule so that it does not short circuit. If it does not, rewrite it so it does short circuit.

A Proficient (P) answer understands why $\texttt{\&\&}$ does or does not short-circuit. This is determined by the $\TirName{DoAnd}$ rule(s). If $\TirName{DoAnd}$ rule(s) do not require each sub-expression to be a value before eliminating the $\texttt{\&\&}$ operator, then it does short circuit. If both sub-expressions are required to be a value before eliminating the $\texttt{\&\&}$ operator, then it does not short-circuit. Note that the direction that the $\TirName{DoAnd}$ rules depends on the way the $\TirName{SearchBinary}$ rules implement evaluation order.

Exercise 23.8 What is the evaluation order of the search rules you wrote in Exercise 23.5? Explain. Write new rules that changes the evaluation order (e.g., from left-to-right to right-to-left).

A Proficient (P) answer understands how $\TirName{Search}$ rules determine evaluation order. If $\TirName{SearchBinary2}$ requires $e_1$ to be a value ($v_1$) in order to step $e_2$, then the evaluation order is left-to-right. This is assuming $\TirName{SearchBinary1}$ is written correctly by not requiring either to be a value. These rules force $e_1$ to be evaluated before $e_2$ in a binary expression.

23.4 Big-Step Semantics with Substitution and Dynamic Type Errors

In the preceding chapters, we considered a big-step semantics with environments and a small-step semantics with substitution. We noted that these are orthogonal considerations, so in this section, consider one of the alternatives, namely big-step semantics with substitution.

We consider a subset of JavaScripty that includes potentially recursive and non-recursive function literals, function calls, and the binary expressions from the language described in Figure 23.1. The abstract syntax is as follows:

\[ \begin{array}{rrrll} \text{values} & v& \mathrel{::=}& n\mid b\mid x^{?}\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& x\mid n\mid b\mid x^{?}\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid e_1 \mathbin{\mathit{bop}}e_2 \mid e_1\texttt{(}e_2\texttt{)} \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{\&\&}\mid\texttt{+} \\ \text{optional variables} & x^{?}& \mathrel{::=}& x\mid\varepsilon \\ \text{variables} & x \end{array} \]

Below are the inference rules for evaluating values, binary expressions, and non-recursive function calls, that is, all except for potentially recursive function calls.

$\fbox{$e \Downarrow v$}$

$\inferrule[EvalVal]{ \phantom{ \Downarrow} }{ v \Downarrow v }$

$\inferrule[EvalPlus]{ e_1 \Downarrow n_1 \and e_2 \Downarrow n_2 }{ e_1 \mathbin{\texttt{+}} e_2 \Downarrow n_1 \mathbin{+} n_2 }$

$\inferrule[EvalAndTrue]{ e_1 \Downarrow\mathbf{true} \and e_2 \Downarrow b_2 }{ e_1 \mathbin{\texttt{\&\&}} e_2 \Downarrow b_2 }$

$\inferrule[EvalAndFalse]{ e_1 \Downarrow\mathbf{false} }{ e_1 \mathbin{\texttt{\&\&}} e_2 \Downarrow\mathbf{false} }$

$\inferrule[EvalCall]{ e_1 \Downarrow \texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e' \and e_2 \Downarrow v_2 \and {}[v_2/y]e' \Downarrow v' }{ e_1\texttt{(}e_2\texttt{)} \Downarrow v' }$

Figure 23.3: A big-step operational semantics for JavaScripty with function literals, function calls, and some binary expressions.

Exercise 23.9 Consider the rules in Figure 23.3, why do we not need a rule for evaluating variables?

A Proficient (P) answer understands that we do not need a rule for evaluating variables because we are using substitution. Variable uses will always be replaced by their values using substitute.

An Exceeding (E) answer also recognizes that we are requiring all of our expressions to be closed in our evaluation judgment form $e \Downarrow v$. Considering an implementation, open expressions would lead to a match error for not matching on a top-level Var.

Exercise 23.10 Is the judgment

\[ \texttt{(} \texttt{(} \texttt{x} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \texttt{(}\texttt{(} \texttt{y} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \texttt{y} \mathbin{\texttt{+}} \texttt{x} \texttt{)} \texttt{)} \texttt{(}\texttt{2}\texttt{)} \Downarrow v \]

derivable using the rules given above? If so, give the derivation. If not, explain why not.

Assume that the concrete syntax allows JavaScripty programmers to parenthesize expressions, so the expression is syntactially valid.

An Proficient (P) answer states the value $v$ is the function value $\texttt{(} \texttt{y} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \texttt{y} \mathbin{\texttt{+}} \texttt{2} $ and gives a correct derivation with four rule applications. Reading bottom up, the root rule application is an $\TirName{EvalCall}$ with three sub-derivations each being applications of $\TirName{EvalVal}$.

An Exceeding (A) answer might also first observe that the expression is well-typed, so the judgment should hold before proceeding to giving a correct derivation.

Exercise 23.11 Write the inference rule for recursive function calls.

A Proficient (P) answer gives the correct rule for recursive function calls. This rule must:

Show that $e_1$ evaluates to the identified recursive function value, say $v_1$.

Correctly substitute the function identifier with $v_1$ in the expression $e_1$ with the formal parameter substituted with the actual argument.

Show that the evaluation of the above expression is what the call evaluates to.

Exercise 23.12 The Scala AST representation for our JavaScripty language has the Var constructor for variables, N for numbers, B for booleans, and Fun for functions. We will represent $x^{?}$ (function identifiers) with the Option[String] type. Implement the remainder of the following substitute function for our small-step interpreter.

trait Expr
case class Var(x: String) extends Expr
case class N(n: Double) extends Expr
case class B(b: Boolean) extends Expr
case class Fun(xopt: Option[String], y: String, e1: Expr) extends Expr
case class Binary(bop: Bop, e1: Expr, e2: Expr) extends Expr
case class Call(e1: Expr, e2: Expr) extends Expr

trait Bop
case object And extends Bop
case object Plus extends Bop

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

def substitute(v: Expr, x: String, e: Expr): Expr = {
    def subst(e: Expr): Expr = e match {
        case Var(y) => ???
        case _ => ???
    }
    ???
}

defined trait Expr
defined class Var
defined class N
defined class B
defined class Fun
defined class Binary
defined class Call
defined trait Bop
defined object And
defined object Plus
defined function isValue
defined function substitute

A Proficient (P) answer implements cases for all Expr cases. For Var, the answer needs to distinguish between shadowing and not shadowing. For Fun, the answer needs to consider the binding of the formal parameter and the possible binding of the optional parameter for the function name. The N and B can be done in the same pattern match, though having them separate is fine. The other cases are not binding constructs, so the answer just needs to reconstruct with recursively calling subst on each sub-expression. Finally, the answer needs to call subst.

An Exceeding (E) answer implements all substitution cases correctly. It might observe that the subst helper function is not strictly necessary but convenient since the v and x are fixed throughout the recursion. It should also note that we have an unstated requirement that v is closed, so we do not need to worry about the possiblity of free-variable capture.

In Figure 23.3, we define evaluation only for well-typed terms. Let us extend the evaluation judgment form with dynamic type checking.

A dynamic type error $\mathop{\mathsf{typeerror}}e$ results if the $\texttt{\&\&}$ operator is applied to numbers, if $\texttt{+}$ is applied to booleans, or if a non-function value is called. We extend our evaluation judgment form $e \Downarrow r$ to return evaluation-results that may be a $\mathsf{typeerror}$ or a value:

\[ \begin{array}{rrrl} \text{evaluation-results} & r& \mathrel{::=}& \mathop{\mathsf{typeerror}}e \mid v \end{array} \]

Some of our dynamic type error rules are given below:

$\fbox{$e \Downarrow r$}$

$\inferrule[TypeErrorPlus1]{ e_1 \Downarrow v_1 \and v_1 \neq n_1 }{ e_1 \mathbin{\texttt{+}} e_2 \Downarrow \mathop{\mathsf{typeerror}}(e_1 \mathbin{\texttt{+}} e_2) }$

$\inferrule[TypeErrorAnd2]{ e_2 \Downarrow v_2 \and v_2 \neq b_2 }{ e_1 \mathbin{\texttt{\&\&}} e_2 \Downarrow \mathop{\mathsf{typeerror}}(e_1 \mathbin{\texttt{\&\&}} e_2) }$

$\inferrule[TypeErrorCall]{ e_1 \Downarrow v_1 \and v_1 \neq x^{?}\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 }{ e_1\texttt{(}e_2\texttt{)} \Downarrow \mathop{\mathsf{typeerror}} (e_1\texttt{(}e_2\texttt{)}) }$

$\inferrule[PropagateBinary2]{ e_2 \Downarrow \mathop{\mathsf{typeerror}}e }{ e_1 \mathbin{\mathit{bop}} e_2 \Downarrow \mathop{\mathsf{typeerror}}e }$

Exercise 23.13 Give the missing rules $\TirName{TypeError}$ and $\TirName{Propagate}$ rules.

A Proficient (P) answer gives correct rules analogous to the above rules for $\TirName{TypeErrorPlus2}$, $\TirName{TypeErrorAnd1}$, $\TirName{PropagateBinary1}$, $\TirName{PropagateCall1}$, and $\TirName{PropagateCall2}$.

An Exceeding (E) answer also understands why we need the $\TirName{Propagate}$ rules and can explain the issue with not having them. It also explains what would happen in an implementation if they were not given. An Exceeding (E) answer may be able to give one or two rules explicitly and could explain the others unambiguously without necessarily giving them explicitly.

Exercise 23.14 Implement enough cases of the dynamic type-checking evaluator you defined in Exercise 23.13 in Scala using the Either[DynamicTypeError, Expr] type for an evaluation-result $r$ to be able to evaluate expressions in the sub-language:

\[ \begin{array}{rrrll} \text{expressions} & e& \mathrel{::=}& n\mid b\mid e_1 \mathbin{\mathit{bop}}e_2 \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{+} \end{array} \]

case class DynamicTypeError(e: Expr)
def eval(e: Expr): Either[DynamicTypeError, Expr] = ???

defined class DynamicTypeError
defined function eval

Recall that the constructors for Either[Err,A] are Left(err: Err) and Right(a: A) and the map and flatMap methods transform Right values.

A Proficient (P) answer recognizes that the $\TirName{EvalVal}$, $\TirName{EvalPlus}$, $\TirName{TypeErrorPlus1}$, and $\TirName{TypeErrorPlus2}$ rules, as well as $\TirName{PropagateBinary1}$ and $\TirName{PropagateBinary2}$ rules instantiated for $\texttt{+}$ need to implemented for this sub-language:

def eval(e: Expr): Either[DynamicTypeError, Expr] = e match {
    // EvalVal
    case v if isValue(v) => Right(v)
    case Binary(Plus, e1, e2) => eval(e1) match {
        case Right( N(n1) ) => eval(e2) match {
            // EvalPlus
            case Right( N(n2) ) => Right( N(n1 + n2) )
            // TypeErrorPlus2
            case Right(_) => Left(DynamicTypeError(e))
            // PropagateBinary2 (for Plus)
            case err @ Left(_) => err
        }
        // TypeErrorPlus1
        case Right(_) => Left(DynamicTypeError(e))
        // PropagateBinary1 (for Plus)
        case err @ Left(_) => err
    }
    case _ => ???
}

defined function eval

An Exceeding (E) answer may use flatMap to more conveniently implement the $\TirName{Propagate}$ rules, though it should recognize that those rules are indeed being implemented within the calls to flatMap.