The goal of this assignment is to write a Scala program to perform type checking and type inference on a simple λ-calculus language.

The small language of this assignment has the following expressions and statements.

sealed trait Exp 
case class Var(id: String) extends Exp
case class Num(n: Int) extends Exp
case class Bool(b: Boolean) extends Exp
case class Lambda(binder: String, body: Exp) extends Exp
case class Application(left: Exp, right: Exp) extends Exp
case class Conditional(cond: Exp, conseq: Exp, alter: Exp) extends Exp
case class Let(st: Stmt, body: Exp) extends Exp

sealed trait Stmt
case class Empty() extends Stmt
case class Assign(lhs: String, rhs: Exp) extends Stmt
case class Seq(left: Stmt, right: Stmt) extends Stmt

Your program will infer the following types for a given expression. The type variables are intended for the intermediate stages of inference. Your program will either find a type error in an expression, or, it infers a fully determined type with no type variables in it. As an example, your analyzer is not allowed to accept expressions like Lambda(“x”, Var(“x”)) that have type variables in their final types.

sealed trait Type
case class IntType() extends Type 
case class BoolType() extends Type
case class VarType(id: String) extends Type
case class ArrowType(src: Type, dst: Type) extends Type

Write the set of type inference rules for the language. You do not need to submit the typing rules – you will use them in your type checker. Having the typing rules will help you to understand where you need to generate constraints during type checking.

One way to define type constraints and substitutions (as described in Lecture 13) is the following:

type Constraint = Tuple2[Type,Type]
type Substitution = Map[VarType,Type]

Write a function to get a set (or a list) of type constraints and either find a set of substitutions to unify them, or fail to solve the constraints (because the constraints are not unifiable).

Write the type checking function:

def typeCheck(e: Exp): Option[Type] = {
  // ...
}

The function returns None when there is a type error in the expression. Assume that the environment is initially empty when checking an expression.

Write two tests for your type checker program that are typable, and two tests that fail to have a type. Try to come up with interesting tests, since we will use your tests against the type checker of other students for grading!

The deadline of this project is October 30 at 11:59pm (https://mycourses.rit.edu). Please do not upload binary and executable files. Make a zip from your files to make uploading the files easier.

• Read the Homework Assignment Policies for the assignment policies of the course.
• This project should be done individually.