The primary purpose of this lab to explore mutation or imperative updates in programming languages. With mutation, we explore two related language considerations: parameter passing modes and casting. Concretely, we extend JAVASCRIPTY with mutable variables and objects, parameter passing modes, (recursive) type declarations, type casting. At this point, we have many of the key features of JavaScript/TypeScript, except dynamic dispatch.

Parameters are always passed by value in JavaScript/TypeScript, so the parameter passing modes in JAVASCRIPTY is an extension beyond JavaScript/TypeScript. In particular, we consider parameter passing modes primarily to illustrate a language design decision and how the design decision manifests in the operational semantics. Call-by-value with addresses and callby-reference are often confused, but with the operational semantics, we can see clearly the distinction.

We will update our type checker and small-step interpreter from Lab 4 and see that mutation forces a global refactoring of our interpreter. To minimize the impact of this refactoring, we will be explore the functional programming idea of encapsulating computation in a data structure (known as a monad). We will also consider the idea of transforming code to a lowered form to make it easier to implement interpretation.

PL Ideas Imperative programming (memory, addresses, aliasing). Language design choices (via parameter passing modes as a case study).

FP Skills Encapsulating computation as a data structure.

Instructions. From your team of 8-10 persons in your lab section, find a new partner for this lab assignment (different from your Lab 1 partner). You will work on this assignment closely with your partner. However, note that each student needs to submit and are individually responsible for completing the assignment.

You are welcome to talk about these questions in larger groups. However, we ask that you write up your answers in pairs. Also, be sure to acknowledge those with which you discussed, including your partner and those outside of your pair.

Recall the evaluation guideline from the course syllabus.

Both your ideas and also the clarity with which they are expressed matterboth in your English prose and your code!

We will consider the following criteria in our grading:

1

• How well does your submission answer the questions? For example, a common mistake is to give an example when a question asks for an explanation. An example may be useful in your explanation, but it should not take the place of the explanation.
• How clear is your submission? If we cannot understand what you are trying to say, then we cannot give you points for it. Try reading your answer aloud to yourself or a friend; this technique is often a great way to identify holes in your reasoning. For code, not every program that works deserves full credit. We must be able to read and understand your intent. Make sure you state any preconditions or invariants for your functions (either in comments, as assertions, or as require clauses as appropriate).

Try to make your code as concise and clear as possible. Challenge yourself to find the most crisp, concise way of expressing the intended computation. This may mean using ways of expression computation currently unfamilar to you.

Finally, make sure that your file compiles and runs on COG. A program that does not compile will not be graded.

Submission Instructions. Upload to the moodle exactly four files named as follows: Lab5_YourIdentiKey.scala with your answers to the coding exercises

• Lab5Spec-YourIdentiKey.scala with any updates to your unit tests.
• Lab5-YourIdentiKey.jsy with a challenging test case for your JAVASCRIPTY
• Lab5_YourIdentiKey.pdf with your answers to the written exercises (only written exercise is for extra credit).

Replace YourIdentiKey with your IdentiKey (e.g., I would submit Lab5-bec.pdf and so forth). Dont use your student identification number. To help with managing the submissions, we ask that you rename your uploaded files in this manner.

Submit your Lab5.scala file to COG for auto-testing. We ask that you submit both to COG and to moodle in case of any issues.

Sign-up for an interview slot for an evaluator. To fairly accommodate everyone, the interview times are strict and will not be rescheduled. Missing an interview slot means missing the interview evaluation component of your lab grade. Please take advantage of your interview time to maximize the feedback that you are able receive. Arrive at your interview ready to show your implementation and your written responses. Implementations that do not compile and run will not be evaluated.

Getting Started. Clone the code from the Github repository with the following command: git clone -b lab5 https://github.com/bechang/pppl-labs.git lab5

A suggested way to get familiar with Scala is to do some small lessons with Scala Koans (http://www.scalakoans.org/).

sealed class DoWith[W,R] private (doer: W => (W,R)) {

def apply(w: W) = doer(w)

def map[B](f: R => B): DoWith[W,B] = new DoWith[W,B]({

(w: W) => { val (wp, r) = doer(w)

(wp, f(r))

} })

def flatMap[B](f: R => DoWith[W,B]): DoWith[W,B] = new DoWith[W,B]({

(w: W) => { val (wp, r) = doer(w)

f(r)(wp) // same as f(r).apply(wp)

}

})

}

def doget[W]: DoWith[W,W] = new DoWith[W,W]({ w => (w, w) }) def doput[W](w: W): DoWith[W, Unit] = new DoWith[W, Unit]({ _ => (w, ()) }) def doreturn[W,R](r: R): DoWith[W,R] = new DoWith[W,R]({ w => (w,r) }) def domodify[W](f: W => W): DoWith[W,Unit] = new DoWith[W,Unit]({ w => (f(w),()) })

Figure 1: The DoWith type.

1. Feedback. Complete the survey on the linked from the moodle after completing this assignment. Any non-empty answer will receive full credit.
2. Warm-Up: Encapsulating Computation. To implement our interpreter for JAVASCRIPTY with memory, we introduce the idea of encapsulating computation with the DoWith[W,R] type. This idea builds on the concepts of abstract data types, collections, and higher-order functions introduced in Lab 4.

The DoWith type constructor is defined for you in the jsy.lab5 package and shown in Figure 1. The essence of the DoWith[W,R] type is that it encapsulates a function of type W=>(W,R), which is a computation that returns a value of type R with an input-output state of type W. The doer field holds precisely a function of the type W=>(W,R).

We should view DoWith[W,R] as a collection somewhat like List[A]. A value of type List[A] encapsulates a sequence of elements of type A and has methods to process and transform those elements. Similarly, a value of type DoWith[W,R] encapsulates a computation with a input-output state W for a result R and has methods to process and transform that computation.

Consider the map method shown in Figure 1. Let us focus on the signature of the map method:

class DoWith[W,R] { def map[B](f: R => B): DoWith[W,B] }

From the signature, we see that the map method transforms a DoWith holding a computation with a W for a R to one for a B using the callback f. Intuitively, the input computation (bound to this) that will yield a result r:R and map transforms it to computation that will yield the result f(r):B. The flatMap method

class DoWith[W,R] { def flatMap[B](f: R => DoWith[W,B]): DoWith[W,B] }

is quite similar to map, but it allows the callback f to return a DoWith[W,B] computation. Intuitively, flatMap sequences the input computation (bound to this) that will yield a result r:R with the computation obtained from f(r).

We have four functions doget, doput, doreturn, and domodify for constructing DoWith objects (and disallow the direct construction of DoWith objects). The doget method creates a computation whose result is the current state w. The doput[W](w : W) method creates a computation that sets the state to w (and whose result is just unit ()). The doreturn[W,R](r : R) method creates a computation that leaves the state untouched whose result is r. Finally, the domodify[W](f : W=>W) method creates a computation that modifies the state according to f. The doreturn and domodify functions are strictly needed, as they can be defined in terms of doget, doput, map, and flatMap, but we provide them because they are commonly-needed operations.

In this question, we practice using the DoWith[W,R] type.

• Implement a function def rename(env: Map[String, String], e: Expr): DoWith[Int,Expr]

that yields a computation to yield a resulting expression that is a version of the input expression e with bound variables renamed. The environment env maps names for free variables in e to what they should be renamed to in the result. You should use the provided helper function def fresh: DoWith[Int,String] for creating fresh variable names.

For the purposes of this exercise, we will only consider the subset of the expression language, consisting of the following:

e ::= x | n | e₁ + e₂ |const x = e₁; e₂

The strategy that we will use for renaming will be to globally renaming all variables uniquely using an integer counter. For example, we will rename

const a = (const a = 1; a ); (const a = 2; a )

to

const x0 = (const x1 = 1; x1); (const x2 = 2; x2) .

Note that we will completely ignore the names given in the input, so the following expression will also be renamed to the syntactically same expression as above:

const a = (const b = 1; b ); (const c = 2; c ) .

This policy for new variable names is captured in given helper function fresh, and we will rename expressions from left-to-right.

Seeing the DoWith[Int,Expr] type as an encapsulated Int=>(Int,Expr), we see that the signature our rename is conceptually def rename(env: Map[String, String], e: Expr): (Int => (Int, Expr))

The rename function is thus conceptually a curried function that takes as input first env and e, which returns a function that takes an integer i to return a integer-expression pair (i0,e0). The integer state captures the next available variable number.

Hint: The only functions or methods for manipulating DoWith objects in this exercise are doreturn, map, and flatMap. The doget and doput functions are used in fresh, but you will not need to call them directly.

3. JavaScripty Implementation

At this point, we are used to extending our interpreter implementation by updating our type checker typeInfer and our small-step interpreter step. The syntax with extensions highlighted is shown in Figure 2 and the new AST nodes are given in Figure 3.

Mutation. In this lab, we add mutable variables declared as follows:

var x = e₁; e₂

and then include an assignment expression:

e1 = e2

that writes the value of e₂ to a location named by expression e₁. Expressions may be mutable variables x or fields of objects e₁.f . We make all fields of objects mutable as is the default in JavaScript.

We remove the AST node ConstDecl and replace it with the node Decl with an additional parameter mut : Mutability that specifies the mutability of the variable, that is, whether the variable is const or var.

Aliasing. In JavaScript and in this lab, objects are dynamically allocated on the heap and then referenced with an extra level of indirection through a heap address. This indirection means two program variables can reference the same object, which is called aliasing. With mutation, aliasing is now observable as demonstrated by the following example:

const x = { f : 1 } const y = x x.f = 2

console.log(y.f)

expressions valueslocation expressions location values unary operators binary operators	e ::= x | n | b |undefined| uope1 | e1 bop e2 | e1 ? e2 : e3| mut x = e1; e2 |console.log(e1)| str |function p(params)tann e1 | e0(e)| { f : e } | e1.f | e1 = e2 | a |null| interface T { f : } ; e1 v ::= n | b |undefined| str |function p(params)tann e1| a |null le ::= x | e1.flv ::= a | a.fuop ::= |!||bop ::= ,|+||*|/|===|!==|<|<=|>|>=|&&|||
types	::= number|bool|string|Undefined| (params) 0 | { f : }| Null| T |Interface T
variables	x
numbers (doubles)	n
booleans strings	b ::= true|falsestr
function names function parameters field names	p ::= x |params ::= x : | mode x : f
type annotations mutability passing mode addresses	tann ::= : |mut ::= const|varmode ::= name|var|ref a
type variables	T
type environments	::= |[mut x 7]
memories contents	M ::= | M[a 7 k] k ::= v | { f : v }

Figure 2: Abstract Syntax of JAVASCRIPTY

/* Declarations */

case class Decl(mut: Mutability, x: String, e1: Expr, e2: Expr) extends Expr

Decl(mut, x, e₁, e₂) mut x =e₁; e₂ case class InterfaceDecl(tvar: String, tobj: Typ, e: Expr) extends Expr InterfaceDecl(T, , e) interfaceT ; e

sealed abstract class Mutability case object Const extends Mutability

MConst const case object Var extends Mutability MVar var

/_* Addresses and Mutation _*/ case class Assign(e1: Expr, e2: Expr) extends Expr

Assign(e₁, e₂) e₁=e₂ case object Null extends Expr

Null null case class A(addr: Int) extends Expr

A() a case object Deref extends Uop Deref

/* Functions */

type Params = Either[ List[(String,Typ)], (PMode,String,Typ) ] case class Function(p: Option[String], paramse: Params, tann: Option[Typ], e1: Expr) extends Expr

Function(p, params, tann, e₁) functionp(params)tanne₁

sealed abstract class PMode case object PName extends PMode

PName name case object PVar extends PMode

PVar var case object PRef extends PMode PRef ref

/* Casting */ case class Cast(t: Typ) extends Uop Cast(⁾

/* Types */ case class TVar(tvar: String) extends Typ

TVar(T) T case class TInterface(tvar: String, t: Typ) extends Typ TInterface(T, ) InterfaceT

Figure 3: Representing in Scala the abstract syntax of JAVASCRIPTY. After each caseclass or caseobject, we show the correspondence between the representation and the concrete syntax.

The code above should print 2 because x and y are aliases (i.e., they are bound to the same object value). Aliasing makes programs more difficult to reason about and is often the source of subtle bugs.

To model allocation, object literals of the form { f : v } are no longer values, rather they evaluate to an address a, which are then the values representing objects (as shown below):

values v ::= | a |null

With objects allocated on the heap, we also introduce the null value (or often called the null pointer). We consider an unbounded set of addresses that is disjoint from the null value (i.e., a cannot stand for null). Addresses a are also included in program expressions e because they arise during evaluation. However, there is no way to explicitly write an address in the source program. Addresses are an example of an enrichment of program expressions as an intermediate form solely to express small-step evaluation.

Parameter Passing Modes. We can annotate function parameters with var, ref, or name to specify a parameter passing mode. The annotation var says the parameter should be callby-value with an allocation for a new mutable parameter variable initialized the argument value. The ref and annotations specify call-by-reference and call-by-name, respectively. In Lab 4, all parameters were call-by-value with an immutable variable, conceptually a const parameter. This call-by terms are defined by their respective DOCALL rules in Figure 9. The intellectual exercise here is to decode what these call-by terms mean by reading their respective rules. Observe from the rules that the ref requires an intermediate language with addresses (and mutation to be interesting), but name could be a useful language feature in a pure setting. Call-by-name is a specific instance of lazy evaluation.

To simplify the lab implementation, we consider in the syntax two kinds of function parameters params that are either a sequence of pass-by-value with immutable variables x : (as before and conceptually const parameters) or a single parameter with one of the new parameter passing modes mode x : . This choice is purely for pedagogical reasons so that you do not need to deal with parameter lists when thinking about parameter passing modes. From the programmers perspective, this would be a bit strange, as one would expect to be able specify a parameter list with independent passing modes for each parameter. In the AST nodes, the two kinds of function parameters are implemented via the Scala Either type (see Figure 3).

Casting. In the previous lab, we carefully crafted a very nice situation where as long as the input program passed the type checker, then evaluation would be free of run-time errors. Unfortunately, there are often programs that we want to execute that we cannot completely check statically and must rely on some amount of dynamic (run-time) checking.

We want to re-introduce dynamic checking in a controlled manner, so we ask that the programmer include explicit casts, written e. Executing a cast may result in a dynamic type error but intentionally nowhere else. Our step implementation should only result in throwing DynamicTypeError when executing a cast. For simplicity, we limit the expressivity of casts to between object types.

The null value has type Null and is not directly assignable to something of object type, but we make Null castable to any object type. However, there is a cost to this flexibility, with null, we have to introduce another run-time check. We add another kind of run-time error for null dereference errors, which we write as nullerror and implement in step by throwing NullDereferenceError.

Abstract Syntax Trees. In Figure 3, we show the updated and new AST nodes. Note that Deref and Cast are Uops (i.e., they are unary operators).

(a) Exercise: Type Checking. The inference rules defining the typing judgment form are given in Figures 4, 5, and 6.

• Similar to before, we implement type inference with the function def typeInfer(env: Map[String,(Mutability,Typ)], e: Expr): Typ

that you need to complete. Note that the type environment maps a variable name to a pair of a mutability (either MConst or MVar) and a type.

• The type inference should use a helper function def castOk(t1: Typ, t2: Typ): Boolean

that you also need to complete. This function specifies when type t1 can be casted to type t2 and implements the judgment form _{1 2} given in Figure 6.

A template for the Function case for typeInfer is provided that you may use if you wish.

` e :

TYPENEG TYPENOT TYPESEQ

TYPEVAR` x : (x)

`e1 : number`e1 : number

`e1 : bool` !e1 : bool

`e1 : 1 `e2 : 2`e1 , e2 : 2

TYPEARITH TYPEPLUSSTRING

`e<sub>1</sub> : number `e₂ : number bop {+,,,/} `e<sub>1</sub> : string `e₂ : string

`e<sub>1</sub> bope<sub>2</sub> : number `e₁ +e₂ : string

TYPEINEQUALITYNUMBER

`e<sub>1</sub> : number `e₂ : number bop {<,<=,>,>=}

`e₁ bope₂ : bool

TYPEINEQUALITYSTRING

`e<sub>1</sub> : string `e₂ : string bop {<,<=,>,>=}

`e₁ bope₂ : bool

TYPEEQUALITY

`e<sub>1</sub> : `e₂ : has no function types bop {===,! ==}

`e1 bope2 : bool
TYPEANDOR`e1 : bool `e2 : bool bop {&&,||}`e1 bope2 : bool	TYPEPRINT`e1 : 1`console.log(e1) : Undefined
TYPEIF`e1 : bool `e2 : `e3 : TYPENUMBER`e1 ? e2 : e3 : `n : number	TYPEBOOL TYPESTRING`b : bool `str : string
TYPEOBJECT	TYPEGETFIELD
TYPEUNDEFINED `ei : i (for all i) `e : { , f : , }`undefined : Undefined ` { , fi : ei, } : { , fi : i, } `e.f :

Figure 4: Typing of non-imperative primitives and objects of JAVASCRIPTY (no change from the previous lab).

` e :

TYPEDECL TYPEFUNCTION

`e<sub>1</sub> : <sub>1</sub> [mutx 7<sub>1</sub>] `e₂ : ₂ [constx 7 ] `e₁ : 0

`mut x =e<sub>1</sub>; e<sub>2</sub> : <sub>2</sub> ` function (x : ) e₁ : (x : ) 0

TYPEFUNCTIONANN TYPERECFUNCTION

[constx 7 ] `e<sub>1</sub> : 0 [constx<sub>0</sub> 7 00][constx 7] `e₁ : 0 ⁰⁰ = (x : ) 0

` function (x : ) : 0 e<sub>1</sub> : (x : ) 0 ` functionx₀(x : ) : 0 e₁ : 00

TYPEFUNCTIONMODE

[mut(mode)x 7] `e₁ : 0

` function (modex : ) e₁ : (modex : ) 0

TYPEFUNCTIONANNMODE

[mut(mode)x 7] `e₁ : 0

` function (modex : ) : 0 e₁ : (modex : ) 0

TYPERECFUNCTIONMODE _def

[constx0 7 00][mut(mode)x 7] `e1 : 0 mut(name) defdef=== const

mut(var) var ` functionx0(modex : ) : 0 e1 : (modex : ) ⁰ mut(ref) var

Figure 5: Typing of objects and binding constructs of JAVASCRIPTY.

` e :

TYPEASSIGNVAR TYPEASSIGNFIELD TYPENULL`e<sub>1</sub> : { , f : , } `e₂ :

`null : Null`e₁.f =e₂ :

TYPECALL`e : (x1 : 1,,xn : n) 0 `e1 : 1 `en : n`e(e1,,en) : 0TYPECALLNAMEVAR TYPECALLREF
`e1 : (modex : ) 0 `e2 : mode 6=ref		`e1 : (refx : ) 0 `le2 : `e1(le2) : 01 2
`e1(e2) : 0 Requires Additional Dynamic Checking	TYPECAST`e1 : 1 1 `e1 :
CASTOKEQ CASTOKNULL Null { }	CASTOKOBJECT i =0i	(for all 1 i n m)
	{ , fi : i,, fn : n,, fm : m } { , fi : 0i,, fn : 0n }

CASTOKOBJECT

_i =0_i (for all 1 i n m)

{ , f_i : _i,, f_n : _n } { , f_i : _i⁰,, f_n : _n0,, f_m : 0_m }

Figure 6: Typing of imperative and type casting constructs of JAVASCRIPTY.

(b) Exercise: Reduction. We also update step from Lab 4. A small-step operational semantics is given in Figures 710.

The small-step judgment form is now as follows:^[1]

M,eM0,e⁰

that says informally, In memory M, expression e steps to a new configuration with memory M0 and expression e0. The memory M is a map from addresses a to contents k, which include values and object values. The presence of a memory M that gets updated during evaluation is the hallmark of imperative computation.

Note that the change in the judgment form necessitates updating all ruleseven those that do not involve imperative features as in Figure 7. For these rules, the memory M is simply threaded through (see Figure 7).

• The step function now has the following signature def step(e: Expr): DoWith[Mem,Expr]

corresponding to the updated operational semantics. This function needs to be completed.

Seeing the DoWith[Mem,Expr] type as an encapsulated Mem=>(Mem,Expr), we see how the judgment form M,e M0,e⁰ corresponds to the signature of step. In particular, the signature our step is conceptually

def step(e: Expr): (Mem => (Mem, Expr))

The step function is thus conceptually a curried function that takes as input first e, which returns a function that takes M to return (M0,e0).

The Crucial Observation. The main advantage of using the encapsulated computation type DoWith[Mem,Expr] is that we can put this common-case threading into the DoWith data structure.

Some rules require allocating fresh addresses. For example, DOOBJECT specifies allocating a new address a and extending the memory mapping a to the object. The address a is stated to be fresh by the constraint that a dom(M). In the implementation, you call memalloc(k) to get a fresh address with the memory cell initialized to contents k.

(c) Exercise: Call-By-Name. The final wrinkle in our interpreter is that call-by-name requires substituting an arbitrary expression into another expression. Thus, we must be careful to avoid free variable capture (cf., Notes 3.2). We did not have to consider this case before because we were only ever substituting values that did not have free variables.

In this lab, you will need to modify your substitute function to avoid free variable capture. A function to rename bound variables is given that def avoidCapture(avoidVars: Set[String], e: Expr): Expr

M,eM0,e⁰

DONEG DONOT n0 =n b0 =b DOSEQ

M,nM,n⁰ M,!bM,b⁰ M,v₁ , e₂M,e₂

DOARITH n0 =n1 bopn2 bop {+,,,/}M,n1 bopn2M,n0	DOPLUSSTRINGstr0 =str1+str2M,str1 +str2M,str0
DOINEQUALITYNUMBER b0 =n1 bopn2 bop {<,<=,>,>=}M,n1 bopn2M,b0	DOINEQUALITYSTRING b0 =str1 bopstr2 bop {<,<=,>,>=}M,str1 bopstr2M,b0

DOEQUALITY

b⁰ = (v1 bopv2) bop {===,! ==} DOANDTRUE DOANDFALSE

M,v₁ bopv₂M,^b0 M,true && e₂M,e₂ M,false && e₂M,false

DOPRINT DOORTRUE DOORFALSE v₁ printed

M,true||e₂M,true M,false||e₂M,e₂ M,console.log(v₁)M,undefined

SEARCHUNARY DOIFTRUE DOIFFALSE M,e₁M0,e₁0

M,true ? e₂ : e₃M,e₂ M,false ? e₂ : e₃M,e₃ M,uope₁M0,uope₁⁰

SEARCHBINARY1 SEARCHBINARY2

M,e₁M0,e₁0 M,e₂M0,e₂0

M,e₁ bope₂M0,e₁0 bope₂ M,v₁ bope₂M0,v₁ bope₂⁰

SEARCHPRINT SEARCHIF

M,e₁M0,e₁0 M,e₁M0,e₁0

M,console.log(e₁)M0,console.log(e₁0 ) M,e₁ ? e₂ : e₃M0,e₁0 ? e₂ : e₃

Figure 7: Small-step operational semantics of non-imperative primitives of JAVASCRIPTY. The only change compared to the previous lab is the threading of the memory.

renames bound variables in e to avoid variables given in avoidVars. Note that you will also need to call the function def freeVars(e: Expr): Set[String] that computes the set of free variables of an expression.

Memory. One might notice that in our operational semantics, the memory M only grows and never shrinks during the course of evaluation. Our interpreter only ever allocates memory and never deallocates! This choice is fine in a mathematical model and for this lab, but a production run-time system must somehow enable collecting garbageallocated memory locations that are no longer used by the running program. Collecting garbage may be done manually by the programmer (as in C and C++) or automatically by a conservative garbage collector (as in JavaScript, Scala, Java, C#, Python).

One might also notice that we have a single memory instead of a stack of activation records for local variables and a heap for objects as discussed in Computer Systems. Our interpreter instead simply allocates memory for local variables when they are encountered (e.g., DOVAR). It never deallocates, even though we know that with local variables, those memory cells become inaccessible by the program once the function returns. The key observation is that the traditional stack is not essential for local variables but rather is an optimization for automatic deallocation based on function call-and-return.

Type Safety. There is delicate interplay between the casts that we permit statically with

1 2

and the dynamic checks that we need to perform at run-time (i.e., in

M,eM0,e⁰

as with TYPEERRORCASTOBJ or NULLERRORDEREF).

We say that a static type system (e.g., our ` e : judgement form) is sound with respect to an operational semantics (e.g., our M,eM0,e⁰) if whenever our type checker defined by our typing judgment says a program is well-typed, then our interpreter defined by our small-step semantics never gets stuck (i.e., never throws StuckError).

Note that if the equality checks _i =⁰_i in the premises of CASTOKOBJECT and CASTOKOBJECT were changed slightly to cast ok checks (i.e., _i ⁰_i), then our type system would become unsound with respect to our current operational semantics. For extra credit, carefully explain why by giving an example expression that demonstrates the unsoundness. Then, carefully explain what run-time checking you would add to regain soundness. First, give the explanation in prose, and then, try to formalize it in our semantics (if the challenge excites you!).

M,eM0,e⁰

DOOBJECT DOGETFIELD

a dom(M) M(a) = { , f : v, }

M,{ f : v }M[a 7 { f : v }],a M,a.f M,v

SEARCHOBJECT SEARCHGETFIELD

M,e_iM0,e_i0 M,e₁M0,e₁0

M,{ , f_i : e_i, }M0,{ , f_i : e_i0, } M,e₁.f M0,e₁0 .f

DOVAR DOCONST a dom(M)

M,constx = v₁; e₂M,e₂[v₁/x] M,varx = v₁; e₂M[a 7 v₁],e₂[a/x]

DODEREF a dom(M)M,aM,M(a)	SEARCHDECLM,e1M0,e10 M,mut x =e1; e2M0,mut x =e10 ; e2
DOASSIGNVAR a dom(M)M,a = vM[a 7 v],v	DOASSIGNFIELDM(a) = { , f : v, }M,a.f = v0M[a 7 { , f : v0, }],v0
SEARCHASSIGN1	SEARCHASSIGN2

M,e₁M0,e₁0 e₁ 6=lv₁ M,e₂M0,e₂0

M,e₁ =e₂M0,e₁0 =e₂ M,lv₁ =e₂M0,lv₁ =e₂0

DOCALL DOCALLREC

v =function (x₁ : ₁,,x_n : _n)tanne v =functionx(x₁ : ₁,,x_n : _n)tanne

M,v(v₁,v_n)M,e[v_n/x_n][v₁/x₁] M,v(v₁,v_n)M,e[v_n/x_n][v₁/x₁][v/x]

SEARCHCALL1

M,eM0,e⁰

M,e(e₁,,e_n)M0,e0(e₁,,e_n)

SEARCHCALL2

M,e_iM0,e_i0

M,functionp(x : ) e(v₁,,v_i1,e_i,,e_n)M0,functionp(x : ) e(v₁,,v_i1,e_i0,,e_n)

Figure 8: Small-step operational semantics of objects, binding constructs, variable and field assignment, and function call of JAVASCRIPTY.

M,eM0,e⁰

DOCALLNAME v =function (namex1 : )tanne1M,v(e2)M,e1[e2/x1]	DOCALLRECNAME v =functionx(namex1 : )tanne1M,v(e2)M,e1[e2/x1][v/x]
DOCALLVAR v =function (varx1 : )tanne1 a dom(M)M,v(v2)M[a 7 v2],e1[a/x1]	DOCALLRECVAR v =functionx(varx1 : )tanne1 a dom(M)M,v(v2)M[a 7 v2],e1[a/x1][v/x]
DOCALLREF v =function (refx1 : )tanne1M,v(lv2)M,e1[lv2/x1]SEARCHCALLVAR	DOCALLRECREF v =functionx(refx1 : )tanne1M,v(lv2)M,e1[lv2/x1][v/x]
M,e2M0,e20

M,functionp(varx : ) e₁(e₂)M0,functionp(varx : ) e₁(e₂0 )

SEARCHCALLREF

M,e₂M0,e₂0 e₂ 6=lv₂

M,functionp(refx : ) e₁(e₂)M0,functionp(refx : ) e₁(e₂0 )

Figure 9: Small-step operational semantics of function call with parameter passing modes of JAVASCRIPTY.

M,eM0,e⁰

DOCAST DOCASTNULL

v 6=null v 6= a = { } or InterfaceT { }

M,vM,v M,nullM,null

DOCASTOBJ

M(a) = { } = { , fi : i, } or InterfaceT { , fi : i, }M,aM,aTYPEERRORCASTOBJ	fi dom(M(a)) for all i
M(a) = { } = { , fi : i, } or InterfaceT { , fi : i, }M,a typeerror	fi dom(M(a)) for some i
NULLERRORGETFIELD NULLERRORASSIGNFIELDM,null.f nullerror M,null.f =e nullerror	typeerror and nullerror propagation rules elided

Figure 10: Small-step operational semantics of type casting and null dereference errors of

JAVASCRIPTY. Ignore the or Interface parts unless attempting the extra credit implementation.

4. Extra Credit: Type Declarations and Recursive Types.

This exercise is for extra credit. Please only attempt this exercise if you have fully completed the rest of the lab.

Object types become quite verbose to write everywhere, so we introduce type declarations for them: interface T ; e

that says declare at type name T defined to be type that is in scope in expression e. We limit to be an object type. We do not consider T and to be same type (i.e., conceptually using name type equality for type declarations), but we permit casts between them. This choice enables typing of recursive data structures, like lists and trees (called recursive types).

(a) Lowering: Removing Interface Declarations. Type names become burdensome to work with as-is (e.g., requiring an environment to remember the mapping between T and ). Instead, we will simplify the implementation of our later phases by first getting rid of interface type declarations, essentially replacing for T in e. We do not quite do this replacement because interface type declarations may be recursive and instead replace T with a new type form Interface T that bundles the type name T with its definition . In Interface T , the type variable T should be considered bound in this construct.

This lowering should be implemented in the function def removeInterfaceDecl(e: Expr): Expr

This function is very similar to substitution, but instead of substituting for program variables x (i.e., Var(x)), we substitute for type variables T (i.e., TVar(T)). Thus, we need an environment that maps type variable names T to types (i.e., the env parameter of type Map[String,Typ]).

In the removeInterfaceDecl function, we need to apply this type replacement anywhere the JAVASCRIPTY programmer can specify a type . We implement this process by recursively walking over the structure of the input expression looking for places to apply the type replacement.

Finally, we remove interface type declarations

interface T ; e

by extending the environment with [T 7Interface T ] and applying the replacement in e.

(b) Updating Type Checking and Reduction

To update type checking with interface declarations, we only need to update castOk with the rules given in Figure 11.

The update to step is also quite small. We only need to update a few cases corresponding to casting shown in Figure 10.

1 2

CASTOKROLL 1 02[InterfaceT 02/T]1 InterfaceT 02

CASTOKUNROLL01[InterfaceT 01/T] 2InterfaceT 01 2

Figure 11: Type casting with interfaces.

[1] Technically, the judgment form is not quite as shown because of the presence of the run-time error markers typeerror and nullerror.