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:
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:
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:
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.