BYU CS classes

Learn how to implement type checking in an interpreter.

Implement the CITypes interpreter using the provided shell.

The CITypes language is based on the CI3 language, just like your Extended Interpreter. You do not need to add any functionality from your previous assignments.

To make the type system more interesting, the CITypes language adds booleans and numeric lists. A new operator “iszero” is added, which tests to see if a number is zero and returns a boolean result.

The language includes two new boolean literals:

• true
• false

The “if0” function is replaced by “ifb”, which requires that the conditional return a boolean value (like in Java). So that the language can be statically type checked, both branches of “ifb” must return the same type.

The language also requires that the types of formal parameters be specified with the function is declared:

  (lambda <id> : <type> <expr>)

To support this, the language's grammar also includes a new nonterminal “<type>”, which can be “number”, “boolean”, “nlist”, or a function type signature of the form “(<type> : <type>)”.

For example, a simple numeric increment function would be written as

  (lambda x : number (+ x 1))

and a function lambda that takes as input a function f from numbers to numbers would look like this:

  (lambda f : (number : number) (f 3))

There are five new types of expressions for handling numeric lists:

• nempty, which returns an empty numeric list
• nisempty, which returns whether a numeric list is empty
• ncons, which prepends a number to a numeric list
• nfirst, which returns the first number in a numeric list
• nrest, which returns the rest of a numeric list after the first item

Here is the grammar for the CITypes language:

<expr> ::= <number>
         | true
         | false
         | (+ <expr> <expr>)
         | (- <expr> <expr>)
         | (iszero <expr>)
         | (ifb <expr> <expr> <expr>)
         | (with <id> <expr> <expr>)
         | <id>
         | (lambda <id> : <type> <expr>)
         | (<expr> <expr>)
         | nempty
         | (ncons <expr> <expr>)
         | (nisempty <expr>)
         | (nfirst <expr>)
         | (nrest <expr>)
 
<type> ::= number
         | boolean
         | nlist
         | (<type> : <type>)

A working parser for this grammar is already provided as part of the shell. Note: since the focus here is on type checking, this parser works for syntactically valid input but does not adequately reject invalid input. You do not need to bulletproof or otherwise modify the parser.

Notice that there is a new non-terminal for type declarations, which is also handled by the parser.

You should implement a function “type-of-expression” that returns the type of an expression. As with “calc” in the earlier interpreters, there is a top-level version of the function that takes only an expression and then calls (using multiple dispatch) the corresponding function for that kind of abstract syntax node, passing to it an empty type environment.

The shell includes implementations of this function for numeric literals and the plus/minus operators, which you can use as examples.

The form of these functions is always the same:

1. Recursively use type-of-expression to type check and determine the types of any subexpressions
2. Verify that types are being used correctly in this expression
3. Return the type of the result of this expression

The type checker should perform no evaluation of the code, only type checking.

In class, we went over the type judgments for the expressions other than those that work with lists. You will need to determine them for the five list-handling expressions yourself.

Some of the tests will involve comparing two types, and a “same_types” function is provided to do a (recursive if necessary) comparison.

When your type checker catches an error, it should throw an exception with a descriptive error message.

• The “calcf” function in the CI3 interpreter that read in a test file, ran it through lex / parse / calc has been replaced with a “typef” function that similarly reads in a test file and runs it through lex / parse / type_of_expression. You can use it to run your own test cases. [Still under construction.]
• Make sure you test not only for validly typed expressions but for each kind of type error.