28 Lab: Static Type Checking

Learning Goals

The primary goals of this lab are:

Programming with higher-order functions.
Static type checking and understanding the interplay between type checking and evaluation.

Functional Programming Skills: Higher-order functions with collections and callbacks.
Programming Language Ideas: Static type checking and type safety. Records.

Instructions

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.

28.1 Static Typing: TypeScripty: Functions and Objects

Static Typing

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.

Multi-Parameter Recursive Functions

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} types & τ & ::= & (\overset{―}{y : τ}) = > τ^{'} \\ values & v & ::= & x^{?} (\overset{―}{y : τ}) τ^{?} = > e_{1} \\ expressions & e & ::= & x^{?} (\overset{―}{y : τ}) τ^{?} = > e_{1} ∣ e_{1} (e_{2}) \\ optional variables & x^{?} & ::= & x ∣ ε \\ optional type annotations & τ^{?} & ::= & : τ ∣ ε \end{array}$

We write a sequence of things using either an overbar or dots (e.g., $\overset{―}{y}$ or $y_{1}, \dots, y_{n}$ for a sequence of variables). Functions can now take any number of parameters $\overset{―}{y : τ}$ . We have a language of types $τ$ and function parameters $\overset{―}{y}$ are annotated with types $\overset{―}{τ}$ .

Functions can be named or unnamed $x^{?}$ and can be annotated with a return type or unannotated $τ^{?}$ . 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

Immutable Objects (Records)

Similarly, we now consider immutable objects that can have an arbitrary number of fields: $\begin{array}{rrrl} types & τ & ::= & {\overset{―}{f : τ}} \\ values & v & ::= & {\overset{―}{f : v}} \\ expressions & e & ::= & {\overset{―}{f : e}} ∣ e_{1} . f \end{array}$

An object literal expression ${f_{1} : e_{1}, \dots, f_{n} : e_{n}}$ 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: ${f_{1} : e_{1}, \dots, f_{n} : e_{n}} : {f_{1} : τ_{1}, \dots, f_{n} : τ_{n}}$

Note that an object value is an object literal expression where each field is a value:

${f_{1} : v_{1}, \dots, f_{n} : v_{n}}$

The field read expression $e_{1} . 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.f

defined 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, $undefined$ with printing, and $const$ -variable declarations. In summary, the type language $τ$ includes base types for numbers, booleans, strings, and $undefined$ , as well as constructed types for functions and objects described above:

$\begin{array}{rrrl} types & τ & ::= & number ∣ bool ∣ string ∣ Undefined \\ ∣ & (\overset{―}{y : τ}) = > τ^{'} ∣ {\overset{―}{f : τ}} \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.

28.2 Interpreter Implementation

We break our interpreter implementation into evaluation and type checking.

Small-Step Reduction

For evaluation, we continue with implementing a small-step operational semantics with a step that implements a single reduction step $e ⟶ 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 $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 ⟶ 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 Exception

defined 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

Static Type Checking

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 $Γ ⊢ e : τ$ , which says, “In type environment $Γ$ , expression $e$ has type $τ$ .” 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 ( $Γ$ ) and an expression e: Expr ( $e$ ) to return a type Typ ( $τ$ ). 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 Exception

defined 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.

Notes

For testing your implementation, there are some interface functions defined that calls your step and hastype implementations with some debugging information:

The iterateStep: Expr => Expr function repeatedly calls your step implementation until reaching a value.
The 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.

28.3 Base TypeScripty

28.3.1 Small-Step Reduction

We consider the base TypeScripty that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, $undefined$ with printing, and $const$ -variable declarations from previous assignments and remove all coercions.

$e ⟶ e^{'}$

$\begin{array}{l} DoNeg \\ \frac{n^{'} = - n_{1}}{- n_{1} ⟶ n^{'}} \end{array}$

$\begin{array}{l} DoArith \\ \frac{n^{'} = n_{1} bop n_{2} bop \in {+, -, *, /}}{n_{1} bop n_{2} ⟶ n^{'}} \end{array}$

$\begin{array}{l} DoPlusString \\ \frac{{str}^{'} = {str}_{1} {str}_{2}}{{str}_{1} + {str}_{2} ⟶ {str}^{'}} \end{array}$

$\begin{array}{l} DoInequalityNumber \\ \frac{b^{'} = n_{1} bop n_{2} bop \in {<, <=, >, >=}}{n_{1} bop n_{2} ⟶ b^{'}} \end{array}$

$\begin{array}{l} DoInequalityString \\ \frac{b^{'} = {str}_{1} bop {str}_{2} bop \in {<, <=, >, >=}}{{str}_{1} bop {str}_{2} ⟶ b^{'}} \end{array}$

$\begin{array}{l} DoEquality \\ \frac{b^{'} = (v_{1} bop v_{2}) bop \in {===,!==}}{v_{1} bop v_{2} ⟶ b^{'}} \end{array}$

$\begin{array}{l} DoNot \\ \frac{b^{'} = \neg b_{1}}{! b_{1} ⟶ b^{'}} \end{array}$

$\begin{array}{l} DoAndTrue \\ \frac{}{true && e_{2} ⟶ e_{2}} \end{array}$

$\begin{array}{l} DoAndFalse \\ \frac{}{false && e_{2} ⟶ false} \end{array}$

$\begin{array}{l} DoOrTrue \\ \frac{}{true || e_{2} ⟶ true} \end{array}$

$\begin{array}{l} DoOrFalse \\ \frac{}{false || e_{2} ⟶ e_{2}} \end{array}$

$\begin{array}{l} DoIfTrue \\ \frac{}{true ? e_{2} : e_{3} ⟶ e_{2}} \end{array}$

$\begin{array}{l} DoIfFalse \\ \frac{}{false ? e_{2} : e_{3} ⟶ e_{3}} \end{array}$

$\begin{array}{l} DoSeq \\ \frac{}{v_{1}, e_{2} ⟶ e_{2}} \end{array}$

$\begin{array}{l} DoPrint \\ \frac{v_{1} printed}{console . log (v_{1}) ⟶ undefined} \end{array}$

$\begin{array}{l} DoConst \\ \frac{}{const x = v_{1}; e_{2} ⟶ [v_{1} / x] e_{2}} \end{array}$

$\begin{array}{l} SearchUnary \\ \frac{e_{1} ⟶ e_{1}^{'}}{uop e_{1} ⟶ uop e_{1}^{'}} \end{array}$

$\begin{array}{l} SearchBinary1 \\ \frac{e_{1} ⟶ e_{1}^{'}}{e_{1} bop e_{2} ⟶ e_{1}^{'} bop e_{2}} \end{array}$

$\begin{array}{l} SearchBinary2 \\ \frac{e_{2} ⟶ e_{2}^{'}}{v_{1} bop e_{2} ⟶ v_{1} bop e_{2}^{'}} \end{array}$

$\begin{array}{l} SearchIf \\ \frac{e_{1} ⟶ e_{1}^{'}}{e_{1} ? e_{2} : e_{3} ⟶ e_{1}^{'} ? e_{2} : e_{3}} \end{array}$

$\begin{array}{l} SearchPrint \\ \frac{e_{1} ⟶ e_{1}^{'}}{console . log (e_{1}) ⟶ console . log (e_{1}^{'})} \end{array}$

$\begin{array}{l} SearchConst \\ \frac{e_{1} ⟶ e_{1}^{'}}{const x = e_{1}; e_{2} ⟶ const x = e_{1}^{'}; e_{2}} \end{array}$

Figure 28.1: Small-step operational semantics of base TypeScripty, including numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation,

undefined

with printing, and

const

-variable declarations.

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 ⟶ 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 $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.

Notes

You may use (or ignore) the provided helper function doInequality to implement the $DoInequalityNumber$ and $DoInequalityString$ rules.

28.3.2 Static Type Checking

We define static typing with the judgment form $Γ ⊢ e : τ$ of base TypeScripty that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, $undefined$ with printing, and $const$ -variable declarations.

$Γ ⊢ e : τ$

$\begin{array}{l} TypeNumber \\ \frac{}{Γ ⊢ n : number} \end{array}$

$\begin{array}{l} TypeString \\ \frac{}{Γ ⊢ str : string} \end{array}$

$\begin{array}{l} TypeNeg \\ \frac{Γ ⊢ e_{1} : number}{Γ ⊢ - e_{1} : number} \end{array}$

$\begin{array}{l} TypeArith \\ \frac{Γ ⊢ e_{1} : number Γ ⊢ e_{2} : number bop \in {+, -, *, /}}{Γ ⊢ e_{1} bop e_{2} : number} \end{array}$

$\begin{array}{l} TypePlusString \\ \frac{Γ ⊢ e_{1} : string Γ ⊢ e_{2} : string}{Γ ⊢ e_{1} + e_{2} : string} \end{array}$

$\begin{array}{l} TypeInequalityNumber \\ \frac{Γ ⊢ e_{1} : number Γ ⊢ e_{2} : number bop \in {<, <=, >, >=}}{Γ ⊢ e_{1} bop e_{2} : bool} \end{array}$

$\begin{array}{l} TypeInequalityString \\ \frac{Γ ⊢ e_{1} : string Γ ⊢ e_{2} : string bop \in {<, <=, >, >=}}{Γ ⊢ e_{1} bop e_{2} : bool} \end{array}$

$\begin{array}{l} TypeEquality \\ \frac{Γ ⊢ e_{1} : τ Γ ⊢ e_{2} : τ bop \in {===,!==}}{Γ ⊢ e_{1} bop e_{2} : bool} \end{array}$

$\begin{array}{l} TypeBool \\ \frac{}{Γ ⊢ b : bool} \end{array}$

$\begin{array}{l} TypeNot \\ \frac{Γ ⊢ e_{1} : bool}{Γ ⊢! e_{1} : bool} \end{array}$

$\begin{array}{l} TypeAndOr \\ \frac{Γ ⊢ e_{1} : bool Γ ⊢ e_{2} : bool bop \in {&&, ||}}{Γ ⊢ e_{1} bop e_{2} : bool} \end{array}$

$\begin{array}{l} TypeIf \\ \frac{Γ ⊢ e_{1} : bool Γ ⊢ e_{2} : τ Γ ⊢ e_{3} : τ}{Γ ⊢ e_{1} ? e_{2} : e_{3} : τ} \end{array}$

$\begin{array}{l} TypeUndefined \\ \frac{}{Γ ⊢ undefined : Undefined} \end{array}$

$\begin{array}{l} TypeSeq \\ \frac{Γ ⊢ e_{1} : τ_{1} Γ ⊢ e_{2} : τ_{2}}{Γ ⊢ e_{1}, e_{2} : τ_{2}} \end{array}$

$\begin{array}{l} TypePrint \\ \frac{Γ ⊢ e_{1} : τ_{1}}{Γ ⊢ console . log (e_{1}) : Undefined} \end{array}$

$\begin{array}{l} TypeVar \\ \frac{}{Γ ⊢ x : Γ (x)} \end{array}$

$\begin{array}{l} TypeConstDecl \\ \frac{Γ ⊢ e_{1} : τ_{1} Γ, x : τ_{1} ⊢ e_{2} : τ_{2}}{Γ ⊢ const x = e_{1}; e_{2} : τ_{2}} \end{array}$

Figure 28.2: Typing of base TypeScripty, including numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation,

undefined

with printing, and

const

-variable declarations.

Observe how closely the $Type$ rules align with the $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 $Γ ⊢ e : τ$ .

type TEnv = Map[String, Typ]
def hastype(tenv: TEnv, e: Expr): Typ = ???

defined type TEnv
defined function hastype

28.4 Immutable Objects (Records)

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.

28.4.1 Small-Step Reduction

We extend the reduction-step judgment form $e ⟶ e^{'}$ for immutable objects:

$e ⟶ e^{'}$

$\begin{array}{l} DoGetField \\ \frac{}{{f_{1} : v_{1}, \dots, f_{i} : v_{i}, \dots, f_{n} : v_{n}} . f_{i} ⟶ v_{i}} \end{array}$

$\begin{array}{l} SearchObject \\ \frac{e_{i} ⟶ e_{i}^{'} e_{j} = v_{j} for all j < i}{{f_{1} : e_{1}, \dots, f_{i} : e_{i}, \dots} ⟶ {f_{1} : e_{1}, \dots, f_{i} : e_{i}^{'}, \dots}} \end{array}$

$\begin{array}{l} SearchGetField \\ \frac{e_{1} ⟶ e_{1}^{'}}{e_{1} . f ⟶ e_{1}^{'} . f} \end{array}$

Figure 28.3: Small-step operational semantics of TypeScripty with immutable objects.

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 ⟶ e^{'}$ .

Notes

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 $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]
```

28.4.2 Static Type Checking

We extend the static typing judgment form $Γ ⊢ e : τ$ for immutable objects:

$\begin{array}{l} TypeObject \\ \frac{Γ ⊢ e_{i} : τ_{i} for all i}{Γ ⊢ {\dots, f_{i} : e_{i}, \dots} : {\dots, f_{i} : τ_{i}, \dots}} \end{array}$

$\begin{array}{l} TypeGetField \\ \frac{Γ ⊢ e : {\dots, f : τ, \dots}}{Γ ⊢ e . f : τ} \end{array}$

Figure 28.4: Typing of TypeScripty with immutable objects.

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 $Γ ⊢ e : τ$ .

Notes

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]
```

28.5 Multi-Parameter Recursive Functions

Finally, we extend our interpreter implementation for multi-parameter recursive functions.

28.5.1 Small-Step Reduction

We extend the reduction-step judgment form $e ⟶ e^{'}$ for multi-paramter recursive functions:

$e ⟶ e^{'}$

$\begin{array}{l} DoCall \\ \frac{}{((y_{1} : τ_{1}, \dots, y_{n} : τ_{n}) τ^{?} = > e) (v_{1}, \dots v_{n}) ⟶ [v_{1} / y_{1}] \dots [v_{n} / y_{n}] e} \end{array}$

$\begin{array}{l} DoCallRec \\ \frac{v = (x (y_{1} : τ_{1}, \dots, y_{n} : τ_{n}) : τ^{'} = > e)}{v (v_{1}, \dots v_{n}) ⟶ [v / x] [v_{1} / y_{1}] \dots [v_{n} / y_{n}] e} \end{array}$

$\begin{array}{l} SearchCall1 \\ \frac{e ⟶ e^{'}}{e (e_{1}, \dots, e_{n}) ⟶ e^{'} (e_{1}, \dots, e_{n})} \end{array}$

$\begin{array}{l} SearchCall2 \\ \frac{e_{i} ⟶ e_{i}^{'} e_{j} = v_{j} for all j < i}{v (e_{1}, \dots, e_{i}, \dots, e_{n}) ⟶ v (e_{1}, \dots, e_{i}^{'}, \dots, e_{n})} \end{array}$

Figure 28.5: Small-step operational semantics for TypeScripty with multi-parameter recursive functions.

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 ⟶ e^{'}$ .

Notes

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): B

You may want to use the zip method for the $DoCall$ and $DoCallRec$ cases to match up formal parameters and actual arguments.

You might want to use your mapFirst function from Homework 4 here.

28.5.2 Static Type Checking

We extend the static typing judgment form $Γ ⊢ e : τ$ for multi-parameter recursive functions:

$\begin{array}{l} TypeCall \\ \frac{Γ ⊢ e : (y_{1} : τ_{1}, \dots, y_{n} : τ_{n}) = > τ Γ ⊢ e_{1} : τ_{1} \dots Γ ⊢ e_{n} : τ_{n}}{Γ ⊢ e (e_{1}, \dots, e_{n}) : τ} \end{array}$

$\begin{array}{l} TypeFunction \\ \frac{Γ, y_{1} : τ_{1}, \dots,, y_{n} : τ_{n} ⊢ e^{'} : τ^{'}}{Γ ⊢ (\overset{―}{y : τ}) = > e^{'} : (\overset{―}{y : τ}) = > τ^{'}} \end{array}$

$\begin{array}{l} TypeFunctionAnn \\ \frac{Γ, y_{1} : τ_{1}, \dots,, y_{n} : τ_{n} ⊢ e^{'} : τ^{'}}{Γ ⊢ (\overset{―}{y : τ}) : τ^{'} = > e^{'} : (\overset{―}{y : τ}) = > τ^{'}} \end{array}$

$\begin{array}{l} TypeFunctionRec \\ \frac{Γ, x : τ_{x}, y_{1} : τ_{1}, \dots,, y_{n} : τ_{n} ⊢ e^{'} : τ^{'} τ_{x} = (\overset{―}{y : τ}) = > τ^{'}}{Γ ⊢ x (\overset{―}{y : τ}) : τ^{'} = > e^{'} : τ_{x}} \end{array}$

Figure 28.6: Typing of TypeScripty with multi-parameter recursive functions.

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 $Γ ⊢ e : τ$ .

Notes

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]

The ++ method on Maps appends two Maps together.