Type Checker FAQ -- Updated 2003-10-28
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:
-
iszero
consumes a number, and returnstrue
if it is0
,false
otherwise -
the test expression of
bif
("boolean if") must evaluate totrue
orfalse
-
ncons
consumes a number and a numeric list, and produces a numeric list
-
Define the function
parse
, which consumes the concrete representation of a program, and returns its abstract syntax tree. -
Write down type judgments for the five numeric list constructs:
nempty
,ncons
,nempty?
,nfirst
, andnrest
. You should turn in hard copy to the cs173 handin bin. -
Implement the function
type-of
, which consumes the abstract representation of a program (i.e. the result ofparse
) and an escape continuation that accepts a string. 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. If the program does have a type error,type-of
invokes the continuation with some string as an argument. For example:(let/cc esc (type-of (parse '{+ 1 2}) esc))
should producenumber
, while:(let/cc esc (type-of (parse '{3 4}) esc))
would invokeesc
with some string, (e.g. "Number is not a function").
Updates
- You may assume that the input program has no parse errors. In other words, don't waste time making your parser more robust, we really just want you to focus on the type system.