Description
Goals of this assignment include:
- Developing a type system for references
- Understanding the limitations of type systems using the division by zero example
Name: WRITE YOUR NAME HERE
// TEST HELPER
def passed(points: Int) {
require(points >=0)
if (points == 1) print(s"\n*** Tests Passed (1 point) ***\n")
else print(s"\n*** Tests Passed ($points points) ***\n")
}
Problem 1 (25 points)
In this problem, we will extend our type system for handling references. Here is a stripped down version of Lettuce that involves references.
We have a type system
A (5 points)
Fill out the missing type annotations labeled type1, type2, and type3 in the program below.
let x: type1 = 25 in
let y : type2 = NewRef( - x ) in
let f : type3 = NewRef(
function (z: ref(num)) DeRef(z) - x >= 45
) in
let z : ref(bool) = DeRef(f)(y) in
z
YOUR ANSWER HERE
B (10 points): Let us write some inference rules for working with ref types.
Recall from notes on “Types and Type Checking” that typeOf(e,α)typeOf(e,α) is the type of an expression ee under type environment αα. The type environment maps identifiers in the current scope to their annotated types.
Let us write a rule for NewRef.
It says that if ee receives type tt under type environment αα and it is not a type error, then NewRef(e)NewRef(e) must receive the type ref(t)ref(t) under αα.
(i) Complete the missing terms for the rule for DeRef
OK rule.
(ii) Complete the missing terms for the rule for DeRef
error.
(iii) Complete the missing terms for AssignRef
OK rule.
YOUR ANSWER HERE
C (10 points): Write the type checker with references by filling in the missing code.
sealed trait Type
case object NumType extends Type
case object BoolType extends Type
case class FunType(t1: Type, t2: Type) extends Type
// TODO: Write a new case class for RefType
??? // YOUR CODE HERE
sealed trait Program
sealed trait Expr
case class Const(f: Double) extends Expr
case class Ident(s: String) extends Expr
case class Plus(e1: Expr, e2: Expr) extends Expr
case class Minus(e1: Expr, e2: Expr) extends Expr
case class Geq(e1: Expr, e2: Expr) extends Expr
case class IfThenElse(e1: Expr, e2: Expr, e3: Expr) extends Expr
case class Let(x: String, xType: Type, e1: Expr, e2: Expr) extends Expr
case class FunDef(id: String, idType: Type, e: Expr) extends Expr
case class FunCall(calledFun: Expr, argExpr: Expr) extends Expr
case class NewRef(e: Expr) extends Expr
case class DeRef(e: Expr) extends Expr
case class AssignRef(e1: Expr, e2: Expr) extends Expr
case class TopLevel(e: Expr) extends Program
def typeEquals(t1: Type, t2: Type): Boolean = t1 == t2
case class TypeErrorException(s: String) extends Exception
def typeOf(e: Expr, alpha: Map[String, Type]): Type = {
def checkType(opName: String, e1: Expr, t1: Type, e2: Expr, t2: Type, resType: Type): Type = {
val t1hat = typeOf(e1, alpha)
if (! typeEquals(t1hat, t1)){
throw new TypeErrorException(s"Type mismatch in arithmetic/comparison/bool op $opName, Expected type $t1, obtained $t1hat")
}
val t2hat = typeOf(e2, alpha)
if (! typeEquals(t2hat, t2)){
throw new TypeErrorException(s"Type mismatch in arithmetic/comparison/bool op $opName, Expected type $t2, obtained $t2hat")
}
resType
}
e match {
case Const(f) => NumType
case Ident(s) => {if (alpha contains s)
alpha(s)
else
throw TypeErrorException(s"Unknown identifier $s")}
case Plus(e1, e2) => checkType("Plus", e1, NumType, e2, NumType, NumType)
case Minus(e1, e2) => checkType("Minus",e1, NumType, e2, NumType, NumType)
case Geq(e1, e2) => checkType("Geq", e1, NumType, e2, NumType, BoolType)
case IfThenElse(e, e1, e2) => {
val t = typeOf(e, alpha)
if (t == BoolType){
val t1 = typeOf(e1, alpha)
val t2 = typeOf(e2, alpha)
if (typeEquals(t1, t2))
t1
else
throw TypeErrorException(s"If then else returns unequal types $t1 and $t2")
} else {
throw TypeErrorException(s"If then else condition expression not boolean $t")
}
}
case Let(x, t, e1, e2) => {
val t1 = typeOf(e1, alpha)
if (typeEquals(t1, t)){
val newAlpha = alpha + (x -> t)
typeOf(e2, newAlpha)
} else {
throw TypeErrorException(s"Let binding has type $t whereas it is bound to expression of type $t1")
}
}
case FunDef(x, t1, e) => {
val newAlpha = alpha + (x -> t1)
val t2 = typeOf(e, newAlpha)
FunType(t1, t2)
}
case FunCall(e1, e2) => {
val ftype = typeOf(e1, alpha)
ftype match {
case FunType(t1, t2) => {
val argType = typeOf(e2, alpha)
if (typeEquals(argType, t1)){
t2
} else {
throw TypeErrorException(s"Call to function with incompatible argument type. Expected $t1, obtained $argType")
}
}
case _ => { throw TypeErrorException(s"Call to function but with a non function type $ftype")}
}
}
case NewRef(e) => {
??? // YOUR CODE HERE
}
case AssignRef(e1, e2) => {
??? // YOUR CODE HERE
}
case DeRef(e) => {
??? // YOUR CODE HERE
}
}
}
def typeOfProgram(p: Program) = p match {
case TopLevel(e) => {
val t = typeOf(e, Map())
println(s"Program type computed successfully as $t")
t
}
}
//BEGIN TEST
/*
let x : ref(num) = NewRef(10 ) in
let dummy: num = AssignRef(x, 30) in
DeRef(x)
*/
val p1 = Let("x", RefType(NumType), NewRef(Const(10)), Let("dummy", NumType, AssignRef(Ident("x"), Const(30) ), DeRef(Ident("x"))) )
val t1 = typeOfProgram(TopLevel(p1))
assert(t1 == NumType, "Test 1 failed: answer should be NumType")
passed(2)
//END TEST
//BEGIN TEST
/*
let x : ref(num) = NewRef(function(z: num) z + 10) in
let dummy: num = AssignRef(x, 30) in
DeRef(x)
*/
val fdef = FunDef("z", NumType, Plus(Ident("z"), Const(10)))
val p2 = Let("x", RefType(NumType), NewRef(fdef), Let("dummy", NumType, AssignRef(Ident("x"), Const(30) ), DeRef(Ident("x"))) )
val t2 = try {
typeOfProgram(TopLevel(p2))
assert(false, "The program should not receive a type")
} catch {
case TypeErrorException(msg) => s"OK -- caught a type error exception: $msg"
case e => print(e); assert(false, "Please throw TypeErrorException(message) when a type failure occurs")
}
passed(2)
//END TEST
//BEGIN TEST
/*
let x : ref(num => num) = NewRef(function(z: num) z + 10) in
let dummy: num = AssignRef(x, 30) in
DeRef(x)
*/
val fdef = FunDef("z", NumType, Plus(Ident("z"), Const(10)))
val p3 = Let("x", RefType(FunType(NumType, NumType)), NewRef(fdef), Let("dummy", NumType, AssignRef(Ident("x"), Const(30) ), DeRef(Ident("x"))) )
val t3 = try {
typeOfProgram(TopLevel(p3))
assert(false, "The program should not receive a type")
} catch {
case TypeErrorException(msg) => s"OK -- caught a type error exception: $msg"
case e => print(e); assert(false, "Please throw TypeErrorException(message) when a type failure occurs")
}
passed(2)
//END TEST
//BEGIN TEST
/*
let x : ref(num => num) = NewRef(function(z: num) z + 10) in
let dummy: num = AssignRef(NewRef(35), 30) in
DeRef(x)
*/
val fdef = FunDef("z", NumType, Plus(Ident("z"), Const(10)))
val p4 = Let("x", RefType(FunType(NumType, NumType)), NewRef(fdef), Let("dummy", NumType, AssignRef(NewRef(Const(35)), Const(30) ), DeRef(Ident("x"))) )
val t4 = typeOfProgram(TopLevel(p4))
assert(t4 == FunType(NumType, NumType), "Test failed")
passed(2)
//END TEST
//BEGIN TEST
val y = Ident("y")
val x = Ident("x")
val z = Ident("z")
val t1 = RefType(NumType)
val t2 = FunType(t1, NumType)
val t3 = RefType(t2)
val v1 = FunCall(DeRef(y), x)
val v2 = Let("z", RefType(BoolType), NewRef(Geq(DeRef(x), Const(25))), v1)
val fdef = FunDef("z", RefType(NumType), Plus(DeRef(z), DeRef(x)))
val v3 = Let("y", t3, NewRef(fdef), v2)
val v4 = Let("x", t1, NewRef(Const(10)), v3)
val p5 = TopLevel(v4)
assert(typeOfProgram(p5) == NumType, "Test failed")
passed(2)
//END TEST
Problem 2 (10 points): Attempted Type System for Division by Zero
In class, we mentioned that developing a static type system for catching run time errors is much harder. Let us try and see what happens.
Let us modify our type grammar to have two different types of numbers: zero and non-zero.
with the following subset of Lettuce just involving arithmetic and let bindings:
Goal: Guarantee that a numeric value that receives type ZeroNumType must be 00 and a numeric value that receives NonZeroNumType must always be non-zero.
Semantic Rules:
Constant: The new rule for constants are
Identifiers: The rule for identifiers remains unchanged (see notes).
Plus: The new rules for plus are
Division: The rules for division are
Let Binding: Rules are unchanged (see notes).
We claim that if a Lettuce program is annotated with the types ZeroNumType and NonZeroNumType, and the type annotations are according to the rules above, then any attempt to divide a number by zero will result in typeerror rather than a runtime exception thrown when evaluating the program using an interpreter.
(A) Write a Lettuce program that has the correct type annotations (you should use the concrete syntax for your answer) but results in a division by zero that is not detected as a typeerror.
(B) Point out which rule among the ones provided is incorrect (techically an incorrect type rule is called unsound).
YOUR ANSWER HERE