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.