LAMP: Exercise 3 Simply typed Lambda-Calculus

Exercise 3 Simply typed Lambda-Calculus

English only

Administrative Issue:

If you have not finished the Evaluator last week, you are kindly asked to do so, because you need it for today's exercise.

Exercise 3 Simply typed Lambda Calculus

Source Language

Internal Language

Values

E ::= x                            T ::= Num
      E E                                Bool
      \x: T.E                            T->T
      true
      false
      zero
      succ E
      pred E
      iszero E
      if E then E else E
      let x = E in E
      let rec x: T = E in E

E ::= x                            T ::= Num
      E E                                Bool
      \x: T.E                            T->T
      true
      false
      zero
      succ E             
      pred E             
      iszero E           
      if E then E else E 
      fix E       
      let x = E in E

V ::=  BV
       NV
       \x: T.E 

BV ::= true   
       false

NV ::= zero   
       succ NV

In this exercise, we are using an internal language. The transformation that the parser applies to a source program is described here:


let rec f:T = E₁ in E₂        ----> let f = fix \f:T.E₁ in E₂

As you can see, all fix nodes will always have a lambda as argument.

The new or changed tree nodes are (from Expr.scala)

case class Lam(inf: Int, n: String, tpe: Type, e: Expr) extends Expr; // \x:T.E
case class Let(inf: Int, n: String, e1: Expr, e2: Expr) extends Expr; // let x = e1 in e2
case class Fix(inf: Int, e: Expr) extends Expr;                       // fix E

class Type { ... }
case object TyBool extends Type;                                      // Bool
case object TyNum extends Type;                                       // Num
case class  TyFun(domain: Type, range:Type) extends Type;             // T -> T

Again, the first parameter is the sourcefile position to report useful error messages.

Type System

Γ |- true: Bool

 
 Γ |- false: Bool

 
 Γ |- zero: Num

x: T ∈ Γ 

Γ |- x: T

Γ |- E: Num

Γ |- pred E: Num

Γ |- E: Num

Γ |- succ E: Num

Γ |- E: Num

Γ |- iszero E: Bool

Γ |- E1: Bool  E2: T   E3: T

Γ |- if E1 then E2 else E3: T

Γ, x: T1 |-  E: T2

Γ |- \x: T1. E: T1->T2

Γ  |- E1: T1 ->T2   Γ  |- E2: T1

Γ |- E1 E2: T2

Γ |-  E1: T1   Γ, f: T1 |- E2:T2

Γ |- let f = E1 in E2: T2

Γ |-  E: T -> T

Γ |- fix E : T

The new computation rules for the nodes Let and Fix are as follows:

let x = E1 in E2  → [x/E1] E2

fix \f.E  → [f / fix \f.E] E

Task 3.1

Download the partial implementation

Implement the missing method analyze in class TypeChecking.scala according to the specification given above.

Task 3.2

Modify the evaluator so it can deal with the nodes Lam,Let and Fix.

You can copy the code from last weeks task and add some cases.

You can run the interpreter with scala slambda.Main <sourcefile>

source - Parser-> Expr (with RawVar nodes) - DeBruijnPhase-> Expr - TypeChecking-> Expr - Evaluator-> Expr(value)

Tips

The context Γ has to be updated with a type binding in the Lam case.

There is a new class case class VarBind(ty: Type) extends Binding; that you can use to make contexts Γ of the form x:T1,...,z:T3.

The class Context has now a method getTypeFromContext. You can call it with a name (must be a string) and a source file position i like this:

case Var(i:Int,j:Int) => ... // i = debugging info, j = de Bruijn index
                ctx.getTypeFromContext(i, ctx(vName), vName);

The first and third parameter are just to make useful error messages. Remember that you have to get the variable name from the context.

A context is updated just like before.

For error reporting, use the method Main.reportError, for instance

case App(inf, x1, x2) => ...Main.reportError(inf, " error in application ...");