You must complete this program with the same partner you had for "Written: Continuations". This is the last coding project you will complete with this team.

Type Checker

In this assignment, you will work with a typed language that includes numbers, booleans, conditionals, functions, and numeric lists. The concrete syntax for the language is given by the following BNF grammars:

   <expr> ::= <num>
            | true
            | false
            | {+ <expr> <expr>}
            | {- <expr> <expr>}
            | {* <expr> <expr>}
            | {iszero <expr>}
            | {bif <expr> <expr> <expr>}

            | <id>
            | {with {<id> <expr>} <expr>}
            | {fun {<id> : <type>} : <type> <expr>}
            | {<expr> <expr>}

            | nempty
            | {ncons <expr> <expr>}
            | {nempty? <expr>}
            | {nfirst <expr>}
            | {nrest <expr>}

   <type> ::= number
            | boolean
            | nlist
            | (<type> -> <type>)
  
In the surface syntax for types, base types are represented by symbols, and the arrow type by a Scheme list of three elements: the type of the argument, the symbol ->, and the type of the result.

You have not implemented some of these constructs yet, but they should be familiar:

Design and Implement the Type Checker

Your type checker must be written in PLAI Restricted Scheme. We provide a template to help you get started. The template has define-type definitions for the abstract syntax of the language and its types. You should not change these definitions.

  1. Define the function parse, which consumes the concrete representation of a program, and returns its abstract syntax tree. To be precise,

    parse :: S-exp -> Expr
    You may assume that s-expression provided to parse conforms to the grammar.

  2. Write down type judgments for the five numeric list constructs: nempty, ncons, nempty?, nfirst, and nrest. You should turn in hard copy to the cs173 handin bin.

  3. Implement the function type-of, which consumes the abstract representation of a program (i.e. the result of parse) If the program has no type errors, type-of returns the type of the program, using the names of the types given in the grammar above. To be precise,

    type-of :: Expr -> Type
    However, if the program does have a type error, type-of invokes error with an appropriate error message. For example:
    (type-of (parse '{+ 1 2}))
    should produce (t-num), while:
    (type-of (parse '{3 4}))
    should call error with some string, e.g. "Number is not a function".

Handin

A single member of your group should handin the assignment. This applies for the type checker (electronic handin) and the type judgements (paper submission).

From the directory containing the files for the assignment you wish to hand in, execute

/course/cs173/bin/cs173handin typec

The type judgements should be submitted on paper; place them in the CS173 handin bin on the 2nd floor.