Lab for Automated Reasoning and Analysis LARA


This week you will implement type checking for Amy. The goal of type checking is to prevent certain errors based on the kind or shape of values that the program is manipulating. E.g. we should prevent an integer from being added to a boolean value.

Type checking is the last stage of the compiler frontend. Every program that reaches the end of this stage without an error is correct, and every program that does not is wrong. We are finally ready to interpret the program or compile it to binary code!

Typing rules for Amy are presented in detail in the Amy specification. Make sure to check correct typing for all expressions and patterns.


This assignment focuses on the file TypeChecker.scala. As usual, the skeleton and helper methods is given to you, and you have to complete the missing parts of the algorithm. In the case of type checking, this consists of implementing typing for all expressions.

The algorithm you will implement traverses the expression and checks each subexpression for correctness in a prefix ways as follows:

  • First, you need to recursively call the function on subexpressions, passing the correct expected type. E.g. for an addition, both operands should be integers. Pass None if you cannot restrict the type.
  • Then, you need to check the type of the current expression against the expected one. Look at the check method for help. You then need to return the type of the expression.
  • Additionally, when you encounter a new variable or parameter, you have to add it to the symbol table so you can find its type later.

Here are some additional notes:

  • There is a type in the tree module called NothingType, which is not meant as a type that any expression could have in Amy, but we will use it temporarily to denote the type of expressions like error() which can take any type.
  • Sometimes you cannot directly restrict the type of a subexpression, like the branches of equality, which can be anything (as long as they are the same). In those cases, you need to check that the types of the subexpressions are compatible after traversing them, i.e. if they are equal or one of them is Nothing. Use the provided lub and lub_* methods.
  • As usual, you can check against our reference compiler. Use the --interpret option. Make sure you have the latest version!


As usual, merge the stubs of the parser into your main branch by typing

git fetch –all

git merge origin/Lab05

(assuming that origin is the name of your remote repository).

The structure of your project src directory should be as following:

 ├── Main.scala                (updated)
 ├── analyzer   
 │    ├── SymbolTable.scala
 │    ├── NameAnalyzer.scala
 │    └── TypeChecker.scala    (new)
 ├── ast                         
 │    ├── Identifier.scala
 │    ├── Printer.scala
 │    └── TreeModule.scala
 ├── interpreter                     
 │    └── Interpreter.scala   
 ├── parsing
 │    ├── ASTConstructor.scala
 │    ├── ASTConstructorLL1.scala
 │    ├── Parser.scala)
 │    ├── Lexer.scala
 │    └── Tokens.scala
 └── utils
      ├── AmycFatalError.scala
      ├── Context.scala
      ├── Document.scala
      ├── Pipeline.scala
      ├── Position.scala
      ├── Reporter.scala
      └── UniqueCounter.scala


You can deliver this assignment after the midterm.

Deadline: Tuesday 28 November, 23:59

IMPORTANT: Please remember to deliver the commit you want us to grade under

cc17/labs_05.txt · Last modified: 2017/11/08 08:56 by manos