On this page:
parse
type-of

3.18 Type Checker

Complete this assignment with Team Three.

You must submit this in an archive named "typec.zip". This archive must contain a folder named "typec". This folder must contain all the files specified below. You must attach "typec.zip" to an email whose subject is "BYU - Fall 2010 - CS 330 - typec" and whose message body contains the name of everyone on your team (each on a separate line.) You must send this email to jay@cs.byu.edu before 5pm (Provo time) on 11/23. Ensure that what you are satisfied with what you submit, because only your chronologically first submission will be graded. Ensure that you follow these instructions exactly, since submissions that do not meet these requirements (i.e. do not have the correct format) will receive no credit, despite the time and energy you put into the assignment. Please see Turn In Policy for more information.

You must submit this in a file named "typec.rkt".

You must complete this assignment using a specific language. Choose Determine language from source in the DrRacket menu, then write
  #lang plai
as the first line of your program, overwritting the default #lang at the top of the file.

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)

You have not implemented some of these constructs yet, but they should be familiar:
  • iszero consumes a number, and returns true if it is 0, false otherwise

  • the test expression of bif ("boolean if") must evaluate to true or false

  • ncons consumes a number and a numeric list, and produces a numeric list

You must use the following template:
  (define-type Expr
    [num (n number?)]
    [id (v symbol?)]
    [bool (b boolean?)]
    [bin-num-op (op procedure?) (lhs Expr?) (rhs Expr?)]
    [iszero (e Expr?)]
    [bif (test Expr?) (then Expr?) (else Expr?)]
    [with (bound-id symbol?) (bound-body Expr?) (body Expr?)]
    [fun (arg-id symbol?)
         (arg-type Type?) (result-type Type?)
         (body Expr?)]
    [app (fun-expr Expr?) (arg-expr Expr?)]
    [nempty]
    [ncons (first Expr?) (rest Expr?)]
    [nfirst (e Expr?)]
    [nrest (e Expr?)]
    [isnempty (e Expr?)])
  
  (define-type Type
    [t-num]
    [t-bool]
    [t-nlist]
    [t-fun (arg Type?) (result Type?)])
  
  ; parse : s-expression -> Expr
  (define (parse sexp)
    (error 'parse "not implemented"))
  
  ; type-of : Expr -> Type
  (define (type-of e)
    (error 'type-of "not implemented"))

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

(parse sexp)  Expr?
  sexp : s-expression?
You may assume that s-expression provided to parse conforms to the grammar.

You should thoroughly test parse to ensure that it parses all valid syntaxes and in particular make sure that it parses things with type errors.

Write down type judgments for the five numeric list constructs: nempty, ncons, nempty?, nfirst, and nrest. (These count as special test cases.)

You must submit this in a file named "judgments.pdf".

Implement the function type-of, which consumes the abstract representation of a program (i.e. the result of parse) To be precise,

(type-of e)  Type?
  e : Expr?
This 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.

If the program has a type error, type-of should invoke 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 'type-of "NUmber is not a function").

You should thoroughly test type-of to ensure that every kind of expression can be typed in as many ways as is reasonable.

Similarly, make sure type-of catches every kind of type error.

In particular, you should make sure type-of does not catch run-time errors, such as (nfirst nempty).

Do not implement an evaluator, just a type checker.