The primary goals of this lab are:
A version of project files for this lab resides in the public pppl-lab4 repository. Please follow separate instructions to get a private clone of this repository for your work.
You will be replacing ??? or case _ => ??? in the Lab4.scala file with solutions to the coding exercises described below.
Your lab will not be graded if it does not compile. You may check compilation with your IDE, sbt compile, or with the “sbt compile” GitHub Action provided for you. Comment out any code that does not compile or causes a failing assert. Put in ??? as needed to get something that compiles without error.
You may add additional tests to the Lab4Spec.scala file. In the Lab4Spec.scala, there is empty test class Lab4StudentSpec that you can use to separate your tests from the given tests in the Lab4Spec class. You are also likely to edit Lab4.worksheet.sc for any scratch work. You can also use Lab4.worksheet.ts to write and experiment in a JavaScript file that you can then parse into a TypeScripty AST (see Lab4.worksheet.sc).
If you like, you may use this notebook for experimentation. However, please make sure your code is in Lab4.scala; code in this notebook will not graded.
As we have seen in the prior labs, dealing with coercions and checking for dynamic type errors complicate the interpreter implementation (i.e., step). Some languages restrict the possible programs that it will execute to ones that it can guarantee will not result in a dynamic type error. This restriction of programs is enforced with an analysis phase after parsing but before evalation known as type checking. Such languages are called statically-typed. In this lab, we implement a statically-typed version of JavaScripty that we affectionately call TypeScripty. We will not permit any type coercions and simultaneously guarantee the absence of dynamic type errors.
Using our skills working with higher-order functions on collections from previous assignments, we now consider functions with zero-or-more parameters (instead of exactly one):
\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \\ \text{values} & v& \mathrel{::=}& x^{?}\texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)}\tau^{?} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& x^{?}\texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)}\tau^{?} \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid e_1\texttt{(}e_2\texttt{)} \\ \text{optional variables} & x^{?}& \mathrel{::=}& x\mid\varepsilon \\ \text{optional type annotations} & \tau^{?}& \mathrel{::=}& \texttt{:}\,\tau \mid\varepsilon \end{array} \]
We write a sequence of things using either an overbar or dots (e.g., \(\overline{y}\) or \(y_1, \ldots, y_n\) for a sequence of variables). Functions can now take any number of parameters \(\overline{y\texttt{:}\,\tau}\). We have a language of types \(\tau\) and function parameters \(\overline{y}\) are annotated with types \(\overline{\tau}\).
Functions can be named or unnamed \(x^{?}\) and can be annotated with a return type or unannotated \(\tau^{?}\). To define recursive functions, the function needs to be named and annotated with a return type.
To represent an arbitrary number of function parameters or function call arguments in Scala, we use an appropriate List:
trait Typ // t
case class TFun(yts: List[(String,Typ)], tret: Typ) extends Typ // t ::= (yts) => tret
trait Expr // e
case class Fun(xopt: Option[String], yts: List[(String,Typ)], tretopt: Option[Typ], e1: Expr) extends Expr // e ::= xopt(yts)tretopt => e1
case class Call(e0: Expr, es: List[Expr]) extends Expr // e ::= e0(es)defined trait Typ defined class TFun defined trait Expr defined class Fun defined class Call
Similarly, we now consider immutable objects that can have an arbitrary number of fields: \[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{\{} \overline{ f\texttt{:}\,\tau } \texttt{\}} \\ \text{values} & v& \mathrel{::=}& \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} \\ \text{expressions} & e& \mathrel{::=}& \texttt{\{} \overline{ f\texttt{:}\,e } \texttt{\}} \mid e_1\texttt{.}f \end{array} \]
An object literal expression \[ \texttt{\{} f_1\texttt{:}\,e_1\texttt{,} \ldots\texttt{,} f_n\texttt{:}\,e_n \texttt{\}} \] is a comma-separated sequence of field names with initialization expressions surrounded by braces. Objects here are more like records in other programming languages compared to actual JavaScript objects, as we do not have any form of mutation or dynamic extension. Fields here correspond to what JavaScript calls properties but which can be dynamically added or removed from objects. We use the term fields to emphasize that they are fixed based on their type: \[ \texttt{\{} f_1\texttt{:}\,e_1\texttt{,} \ldots\texttt{,} f_n\texttt{:}\,e_n \texttt{\}} \quad:\quad \texttt{\{} f_1\texttt{:}\,\tau_1\texttt{,} \ldots\texttt{,} f_n\texttt{:}\,\tau_n \texttt{\}} \]
Note that an object value is an object literal expression where each field is a value:
\[ \texttt{\{} f_1\texttt{:}\,v_1\texttt{,} \ldots\texttt{,} f_n\texttt{:}\,v_n \texttt{\}} \]
The field read expression \(e_1\texttt{.}f\) evaluates \(e_1\) to an object value and then looks up the field named \(f\).
To represent object types and object literal expressions in Scala, we use an appropriate Map:
case class TObj(fts: Map[String, Typ]) extends Typ // t ::= { fts }
case class Obj(fes: Map[String,Expr]) extends Expr // e ::= { fes }
case class GetField(e1: Expr, f: String) extends Expr // e ::= e1.fdefined class TObj defined class Obj defined class GetField
Otherwise, we consider our base JavaScripty language that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, \(\mathbf{undefined}\) with printing, and \(\mathbf{const}\)-variable declarations. In summary, the type language \(\tau\) includes base types for numbers, booleans, strings, and \(\mathbf{undefined}\), as well as constructed types for functions and objects described above:
\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{number} \mid\texttt{bool} \mid\texttt{string} \mid\texttt{Undefined} \\ & & \mid& \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \mid\texttt{\{} \overline{ f\texttt{:}\,\tau } \texttt{\}} \end{array} \]
As an aside, we have chosen a concrete syntax that is compatible with the TypeScript language that adds typing to JavaScript. TypeScript is a proper superset of JavaScript, so it is not as strictly typed as TypeScripty is here in this lab.
We break our interpreter implementation into evaluation and type checking.
For evaluation, we continue with implementing a small-step operational semantics with a step that implements a single reduction step \(e \longrightarrow e'\) on closed expressions. Because of the static type checking, the reduction-step cases can be greatly simplified: we eliminate performing all coercions, and what’s cool is that we no longer need to represent the possibility of a dynamic \(\mathsf{typeerror}\) (e.g., with a Either[DynamicTypeError,Expr]).
We can use the more basic type signature for step:
def step(e: Expr): Expr = ???defined function step
corresponding to the more basic judgment form \(e \longrightarrow e'\) (given in the subsequent sections).
To make easier to identify implementation bugs, we introduce another Scala exception type to throw when there is no possible next step.
case class StuckError(e: Expr) extends Exceptiondefined class StuckError
However, the intent of this exception is that it should get thrown at run-time! If it does get thrown, that signals a bug in our interpreter implementation rather than an error in the TypeScripty test input.
In particular, if the TypeScripty expression e passed into step is closed and well-typed (i.e., inferType(e) does not throw StaticTypeError), then step should never throw a StuckError. This property is type safety.
Recall that to implement step, we need to implement a substitution function substitute corresponding to \({}[v/x]e\) that we use to eagerly apply variable bindings:
def substitute(v: Expr, x: String, e: Expr) = ???defined function substitute
We implement a static type checker that up front rules out programs that would get stuck in taking reduction steps. This type checker is very similar to a big-step interpreter. Instead of computing the value of an expression by recursively computing the value of each sub-expression, we infer the type of an expression, by recursively inferring the type of each sub-expression. An expression is well-typed if we can infer a type for it.
Given its similarity to big-step evaluation, we formalize a type inference algorithm in a similar way. That is, we define the judgment form \(\Gamma \vdash e : \tau\), which says, “In type environment \(\Gamma\), expression \(e\) has type \(\tau\).” We then implement a function hastype:
type TEnv = Map[String, Typ]
def hastype(tenv: TEnv, e: Expr): Typ = ???defined type TEnv defined function hastype
that corresponds directly to this judgment form. It takes as input a type environment tenv: TEnv (\(\Gamma\)) and an expression e: Expr (\(e\)) to return a type Typ (\(\tau\)). It is informative to compare the rules defining typing with a big-step operational semantics.
To signal a type error, we will use a Scala exception
case class StaticTypeError(tbad: Typ, esub: Expr, e: Expr) extends Exceptiondefined class StaticTypeError
where tbad is the type that is inferred sub-expression esub of input expression e. These arguments are used to construct a useful error message. We also provide a helper function err to simplify throwing this exception.
While it is possible to implement iterative reduction via step and type inference viahastype independently, it is generally easier to “incrementally grow the language” by going language-feature by-language-feature for all functions rather than function-by-function. In the subsequent steps, we describe the small-step operational semantics and the static typing semantics together incrementally by language feature.
For testing your implementation, there are some interface functions defined that calls your step and hastype implementations with some debugging information:
iterateStep: Expr => Expr function repeatedly calls your step implementation until reaching a value.inferType: Expr => Typ function calls your hastype function with an empty type environment.Note that the provided tests are minimal. You will want to add your own tests to cover most language features.
We consider the base TypeScripty that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, \(\mathbf{undefined}\) with printing, and \(\mathbf{const}\)-variable declarations from previous assignments and remove all coercions.
\(\fbox{$e \longrightarrow e'$}\)
\(\inferrule[DoNeg]{ n' = - n_1 }{ \mathop{\texttt{-}} n_1 \longrightarrow n' }\)
\(\inferrule[DoArith]{ n' = n_1 \mathbin{\mathit{bop}}n_2 \and \mathit{bop}\in \left\{ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{/} \right\} }{ n_1 \mathbin{\mathit{bop}}n_2 \longrightarrow n' }\)
\(\inferrule[DoPlusString]{ \mathit{str}' = \mathit{str}_1 \mathit{str}_2 }{ \mathit{str}_1 \mathbin{\texttt{+}} \mathit{str}_2 \longrightarrow\mathit{str}' }\)
\(\inferrule[DoInequalityNumber]{ b' = n_1 \mathbin{\mathit{bop}}n_2 \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ n_1 \mathbin{\mathit{bop}}n_2 \longrightarrow b' }\)
\(\inferrule[DoInequalityString]{ b' = \mathit{str}_1 \mathbin{\mathit{bop}}\mathit{str}_2 \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \mathit{str}_1 \mathbin{\mathit{bop}}\mathit{str}_2 \longrightarrow b' }\)
\(\inferrule[DoEquality]{ b' = (v_1 \mathbin{\mathit{bop}}v_2) \and \mathit{bop}\in \left\{ \texttt{===}, \texttt{!==} \right\} }{ v_1 \mathbin{\mathit{bop}}v_2 \longrightarrow b' }\)
\(\inferrule[DoNot]{ b' = \neg b_1 }{ \mathop{\texttt{!}} b_1 \longrightarrow b' }\)
\(\inferrule[DoAndTrue]{ }{ \mathbf{true} \mathbin{\texttt{\&\&}} e_2 \longrightarrow e_2 }\)
\(\inferrule[DoAndFalse]{ }{ \mathbf{false} \mathbin{\texttt{\&\&}} e_2 \longrightarrow\mathbf{false} }\)
\(\inferrule[DoOrTrue]{ }{ \mathbf{true} \mathbin{\texttt{||}} e_2 \longrightarrow\mathbf{true} }\)
\(\inferrule[DoOrFalse]{ }{ \mathbf{false} \mathbin{\texttt{||}} e_2 \longrightarrow e_2 }\)
\(\inferrule[DoIfTrue]{ }{ \mathbf{true}\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow e_2 }\)
\(\inferrule[DoIfFalse]{ }{ \mathbf{false}\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow e_3 }\)
\(\inferrule[DoSeq]{ }{ v_1 \mathbin{\texttt{,}} e_2 \longrightarrow e_2 }\)
\(\inferrule[DoPrint]{ \text{$v_1$ printed} }{ \texttt{console}\texttt{.}\texttt{log}\texttt{(}v_1\texttt{)} \longrightarrow\mathbf{undefined} }\)
\(\inferrule[DoConst]{ }{ \mathbf{const}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 \longrightarrow[v_1/x]e_2 }\)
\(\inferrule[SearchUnary]{ e_1 \longrightarrow e_1' }{ \mathop{\mathit{uop}}e_1 \longrightarrow\mathop{\mathit{uop}}e_1' }\)
\(\inferrule[SearchBinary1]{ e_1 \longrightarrow e_1' }{ e_1 \mathbin{\mathit{bop}}e_2 \longrightarrow e_1' \mathbin{\mathit{bop}}e_2 }\)
\(\inferrule[SearchBinary2]{ e_2 \longrightarrow e_2' }{ v_1 \mathbin{\mathit{bop}}e_2 \longrightarrow v_1 \mathbin{\mathit{bop}}e_2' }\)
\(\inferrule[SearchIf]{ e_1 \longrightarrow e_1' }{ e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow e_1'\;\texttt{?}\;e_2\;\texttt{:}\;e_3 }\)
\(\inferrule[SearchPrint]{ e_1 \longrightarrow e_1' }{ \texttt{console}\texttt{.}\texttt{log}\texttt{(}e_1\texttt{)} \longrightarrow\texttt{console}\texttt{.}\texttt{log}\texttt{(}e_1'\texttt{)} }\)
\(\inferrule[SearchConst]{ e_1 \longrightarrow e_1' }{ \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow\mathbf{const}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 }\)
Exercise 28.1 (Small-Step Reduction for Base TypeScripty) Implement step for base TypeScripty following the small-step operational semantics in Figure 28.1 defining the reduction-step judgment form \(e \longrightarrow e'\).
Note that your task here is simpler than what you have done before in previous assignments. There are no judgment forms or rules defining coercions (e.g., toBoolean) or stepping to a \(\mathsf{typeerror}\) result (e.g., Left(DynamicTypeError(e))).
You will need to implement a helper function substitute for base TypeScripty to perform scope-respecting substitution \({}[v/x]e\) as in previous assignments.
doInequality to implement the \(\TirName{DoInequalityNumber}\) and \(\TirName{DoInequalityString}\) rules.We define static typing with the judgment form \(\Gamma \vdash e : \tau\) of base TypeScripty that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, \(\mathbf{undefined}\) with printing, and \(\mathbf{const}\)-variable declarations.
\(\fbox{$\Gamma \vdash e : \tau$}\)
\(\inferrule[TypeNumber]{ }{ \Gamma \vdash n : \texttt{number} }\)
\(\inferrule[TypeString]{ }{ \Gamma \vdash \mathit{str} : \texttt{string} }\)
\(\inferrule[TypeNeg]{ \Gamma \vdash e_1 : \texttt{number} }{ \Gamma \vdash \mathop{\texttt{-}} e_1 : \texttt{number} }\)
\(\inferrule[TypeArith]{ \Gamma \vdash e_1 : \texttt{number} \and \Gamma \vdash e_2 : \texttt{number} \and \mathit{bop}\in \left\{ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{/} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{number} }\)
\(\inferrule[TypePlusString]{ \Gamma \vdash e_1 : \texttt{string} \and \Gamma \vdash e_2 : \texttt{string} }{ \Gamma \vdash e_1 \mathbin{\texttt{+}} e_2 : \texttt{string} }\)
\(\inferrule[TypeInequalityNumber]{ \Gamma \vdash e_1 : \texttt{number} \and \Gamma \vdash e_2 : \texttt{number} \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeInequalityString]{ \Gamma \vdash e_1 : \texttt{string} \and \Gamma \vdash e_2 : \texttt{string} \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeEquality]{ \Gamma \vdash e_1 : \tau \and \Gamma \vdash e_2 : \tau \and \mathit{bop}\in \left\{ \texttt{===}, \texttt{!==} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeBool]{ }{ \Gamma \vdash b : \texttt{bool} }\)
\(\inferrule[TypeNot]{ \Gamma \vdash e_1 : \texttt{bool} }{ \Gamma \vdash \mathop{\texttt{!}} e_1 : \texttt{bool} }\)
\(\inferrule[TypeAndOr]{ \Gamma \vdash e_1 : \texttt{bool} \and \Gamma \vdash e_2 : \texttt{bool} \and \mathit{bop}\in \left\{ \texttt{\&\&}, \texttt{||} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeIf]{ \Gamma \vdash e_1 : \texttt{bool} \and \Gamma \vdash e_2 : \tau \and \Gamma \vdash e_3 : \tau }{ \Gamma \vdash e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 : \tau }\)
\(\inferrule[TypeUndefined]{ }{ \Gamma \vdash \mathbf{undefined} : \texttt{Undefined} }\)
\(\inferrule[TypeSeq]{ \Gamma \vdash e_1 : \tau_1 \and \Gamma \vdash e_2 : \tau_2 }{ \Gamma \vdash e_1 \mathbin{\texttt{,}} e_2 : \tau_2 }\)
\(\inferrule[TypePrint]{ \Gamma \vdash e_1 : \tau_1 }{ \Gamma \vdash \texttt{console}\texttt{.}\texttt{log}\texttt{(}e_1\texttt{)} : \texttt{Undefined} }\)
\(\inferrule[TypeVar]{ }{ \Gamma \vdash x : \Gamma(x) }\)
\(\inferrule[TypeConstDecl]{ \Gamma \vdash e_1 : \tau_1 \and \Gamma, x : \tau_1 \vdash e_2 : \tau_2 }{ \Gamma \vdash \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 : \tau_2 }\)
Observe how closely the \(\TirName{Type}\) rules align with the \(\TirName{Do}\) rules in Figure 28.1, except for having a big-step evaluation structure with types.
Exercise 28.2 (Static Type Checking for Base TypeScripty) Implement a function hastype for base TypeScript following the static typing semantics in Figure 28.2 defining the typing judgment form \(\Gamma \vdash e : \tau\).
type TEnv = Map[String, Typ]
def hastype(tenv: TEnv, e: Expr): Typ = ???defined type TEnv defined function hastype
Next, we extend our interpreter implementation for immutable objects. We consider the implementation for immutable objects next, as it is a bit simpler than that for multi-parameter functions.
We extend the reduction-step judgment form \(e \longrightarrow e'\) for immutable objects:
\(\fbox{$e \longrightarrow e'$}\)
\(\inferrule[DoGetField]{ }{ \texttt{\{} f_1\texttt{:}\,v_1\texttt{,} \ldots\texttt{,} f_i\texttt{:}\,v_i\texttt{,} \ldots\texttt{,} f_n\texttt{:}\,v_n \texttt{\}} \texttt{.}f_i \longrightarrow v_i }\)
\(\inferrule[SearchObject]{ e_i \longrightarrow e_i' \and e_j = v_j \and \text{for all $j < i$} }{ \texttt{\{} f_1\texttt{:}\,e_1\texttt{,} \ldots\texttt{,} f_i\texttt{:}\,e_i\texttt{,} \ldots \texttt{\}} \longrightarrow \texttt{\{} f_1\texttt{:}\,e_1\texttt{,} \ldots\texttt{,} f_i \mathbin{\texttt{:}} e_i'\texttt{,} \ldots \texttt{\}} }\)
\(\inferrule[SearchGetField]{ e_1 \longrightarrow e_1' }{ e_1\texttt{.}f \longrightarrow e_1'\texttt{.}f }\)
Exercise 28.3 (Small-Step Reduction for Immutable Objects) Implement the cases in step for reducing immutable object expressions using the rules given in Figure 28.3 for the reduction-step judgment form \(e \longrightarrow e'\).
Field names \(f\) are different than variable names \(x\), even though they are both represented in Scala with a String. Object expressions are not variable binding constructs—what does that mean about substitute for them?
For \(\TirName{SearchObject}\), you should make the reduction step apply to the first non-value as given by the left-to-right iteration of the collection using the find method on Maps:
(m: Map[K,V]).find(f: ((K,V)) => Boolean): Option[(K,V)]Other helpful Scala library methods not previously mentioned to use here include the following:
(m: Map[K,V]).get(k: K): Option[V]We extend the static typing judgment form \(\Gamma \vdash e : \tau\) for immutable objects:
\(\inferrule[TypeObject]{ \Gamma \vdash e_i : \tau_i \and \text{for all $i$} }{ \Gamma \vdash \texttt{\{} \ldots\texttt{,} f_i\texttt{:}\,e_i\texttt{,} \ldots \texttt{\}} : \texttt{\{} \ldots\texttt{,} f_i\texttt{:}\,\tau_i\texttt{,} \ldots \texttt{\}} }\)
\(\inferrule[TypeGetField]{ \Gamma \vdash e : \texttt{\{} \ldots\texttt{,} f\texttt{:}\,\tau\texttt{,} \ldots \texttt{\}} }{ \Gamma \vdash e\texttt{.}f : \tau }\)
Exercise 28.4 (Static Type Checking for Immutable Objects) Implement the cases in hastype for typing immutable object expressions using the rules given in Figure 28.4 defining the typing judgment form \(\Gamma \vdash e : \tau\).
Other helpful Scala library methods not previously mentioned to use here include the following:
(m: Map[K,V]).map(f: ((K,V)) => (J,U)): Map[J,U]Finally, we extend our interpreter implementation for multi-parameter recursive functions.
We extend the reduction-step judgment form \(e \longrightarrow e'\) for multi-paramter recursive functions:
\(\fbox{$e \longrightarrow e'$} \quad\)
\(\inferrule[DoCall]{ }{ (\texttt{(} y_1\texttt{:}\,\tau_1\texttt{,}\ldots\texttt{,}y_n\texttt{:}\,\tau_n \texttt{)}\tau^{?} \mathrel{\texttt{=}\!\texttt{>}} e) \texttt{(}v_1, \ldots v_n\texttt{)} \longrightarrow [v_1/y_1]\cdots[v_n/y_n]e }\)
\(\inferrule[DoCallRec]{ v= (x\texttt{(} y_1\texttt{:}\,\tau_1\texttt{,}\ldots\texttt{,}y_n\texttt{:}\,\tau_n \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e) }{ v\texttt{(}v_1, \ldots v_n\texttt{)} \longrightarrow [v/x][v_1/y_1]\cdots[v_n/y_n]e }\)
\(\inferrule[SearchCall1]{ e\longrightarrow e' }{ e\texttt{(}e_1, \ldots, e_n\texttt{)} \longrightarrow e'\texttt{(}e_1, \ldots, e_n\texttt{)} }\)
\(\inferrule[SearchCall2]{ e_i \longrightarrow e_i' \and e_j = v_j \and \text{for all $j < i$} }{ v\texttt{(}e_1, \ldots, e_i, \ldots, e_n\texttt{)} \longrightarrow v\texttt{(}e_1, \ldots, e_i', \ldots, e_n\texttt{)} }\)
Exercise 28.5 (Small-Step Reduction for Multi-Parameter Recursive Functions) Implement the cases in step for reducing multi-parameter recursive functions using the rules given in Figure 28.5 for the reduction-step judgment form \(e \longrightarrow e'\).
Other helpful Scala library methods not previously mentioned to use here include the following:
(l: List[A]).map(f: A => B): List[B]
(l: List[A]).exists(f: A => Boolean): Boolean
(la: List[A]).zip(lb: List[B]): List[(A,B)]
(l: List[A]).forall(f: A => Boolean): Boolean
(l: List[A]).foldRight(f: (A,B) => B): Bzip method for the \(\TirName{DoCall}\) and \(\TirName{DoCallRec}\) cases to match up formal parameters and actual arguments.You might want to use your mapFirst function from Homework 4 here.
We extend the static typing judgment form \(\Gamma \vdash e : \tau\) for multi-parameter recursive functions:
\(\inferrule[TypeCall]{ \Gamma \vdash e : \texttt{(} y_1\texttt{:}\,\tau_1\texttt{,}\ldots\texttt{,}y_n\texttt{:}\,\tau_n \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau \and \Gamma \vdash e_1 : \tau_1 \quad\cdots\quad \Gamma \vdash e_n : \tau_n }{ \Gamma \vdash e\texttt{(}e_1, \ldots, e_n\texttt{)} : \tau }\)
\(\inferrule[TypeFunction]{ \Gamma, y_1 : \tau_1, \cdots, , y_n : \tau_n \vdash e' : \tau' }{ \Gamma \vdash \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e' : \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' }\)
\(\inferrule[TypeFunctionAnn]{ \Gamma, y_1 : \tau_1, \cdots, , y_n : \tau_n \vdash e' : \tau' }{ \Gamma \vdash \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e' : \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' }\)
\(\inferrule[TypeFunctionRec]{ \Gamma, x : \tau_x , y_1 : \tau_1, \cdots, , y_n : \tau_n \vdash e' : \tau' \and \tau_x = \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' }{ \Gamma \vdash x\texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e' : \tau_x }\)
Exercise 28.6 (Static Type Checking for Immutable Objects) Implement the cases in hastype for typing multi-parameter recursive function expressions using the rules given in Figure 28.6 defining the typing judgment form \(\Gamma \vdash e : \tau\).
Other helpful Scala library methods not previously mentioned to use here include the following:
(l: List[A]).foldLeft(f: (B,A) => B): B
(l: List[A]).foreach(f: A => Unit): Unit
(l: List[A]).length: Int
(m1: Map[K,V]).++(m2: Map[K,V]): Map[K,V]++ method on Maps appends two Maps together.