*Form new groups of two for this assignment. We will not accept this
assignment from people working individually or with a partner from the previous
assignments. Email cs173tas@cs.brown.edu the names of the members of your group
by 5pm on Friday, 11/09/07 (only one member needs to send this email). If you
cannot find a partner, send us an email by the same deadline and you will be
assigned a partner. In order to avoid being assigned a random partner, we
suggest staying after class on Friday to find a partner in person. Missing the
email deadline will lower your grade for this assignment by 10% per day
late.*

### Type Inference

For this assignment, we will use *PLAI Pretty Big Scheme*.

#### Part I: Parsing the Language

Write a parser for this language:

<expr> ::= <num> | true | false | {+ <expr> <expr>} | {- <expr> <expr>} | {* <expr> <expr>} | {iszero <expr>} | {bif <expr> <expr> <expr>} | <id> | {with {<id> <expr>} <expr>} | {rec {<id> <expr>} <expr>} | {fun {<id>} <expr>} | {<expr> <expr>} | tempty | {tcons <expr> <expr>} | {tempty? <expr>} | {tfirst <expr>} | {trest <expr>}

The support code specifies the abstract syntax that your parser should return. Your parse function must have the name and contract

parse :: S-exp -> Expr

*You may assume that the s-expressions supplied to*.

`parse`

are valid#### Part II: Constraint Generation

Write a function called `generate-constraints`

that accepts
an expression and returns a list of constraints. You have the freedom to
determine the precise contract of this function, including the representation of
your constraints. However, we strongly recommend that you use the
`Type`

data structures as defined in the support code as part of your
representation of constraints. A few things to note:

List operations are polymorphic; that is, you can create lists of numbers or booleans.

The bound body of a rec binding does not have to be a syntactic function. However, you may assume that the rec-bound identifier only appears under a

`{fun ...}`

in the bound body. In other words, the following expressions are legal:{rec {f {fun {x} {f x}}} ...} {rec {f {with {y 4} {fun {x} {f y}}}} ...}

while the following are not legal:{rec {f f} ...} {rec {f {+ 1 f}} ...}

During constraint generation, you will need to generate fresh identifiers. The function

`gensym`

returns a unique symbol each time it is applied. (`gensym`

accepts an optional symbol as an argument; the result of`(gensym 'x)`

is then a unique symbol that "looks like "`'x`

.)

#### Part III: Unification

Implement the unification algorithm from the lecture notes. Call the function
`unify`

. The `unify`

function should accept a list of
constraints and return a substitution. However, `unify`

should
signal an error if two types cannot be unified or if the *occurs check*
fails. Again, the precise contract of `unify`

is up to you to
define.

#### Part IV: Inferring Types

To infer the type of a program, parse it, generate constraints, and unify the constraints to get a substitution. From the substitution, you can determine the type of the program.

In particular, define the function

infer-type :: Expr -> Type

#### Part V: Testing and War-Grading

`infer-type`

returns a `Type`

, so you will need to test
types for equality. This can be tricky due to type variables, particularly if
`generate-constraints`

calls `(gensym)`

to generate unique
type variables. The support code defines a function ```
((type=? t1)
t2)
```

that returns `true`

if `t1`

and `t2`

are equal, modulo renaming of variables. We've included a few examples that
show you how to use `type=?`

with `test/pred`

and
`test/exn`

. You are free to modify this function as you see fit or
to not use it at all.

You should write unit tests for all functions that you write. However, for
the purpose of war-grading, ensure that your test suites just use ```
parse ::
S-exp -> Expr
```

and `infer-type :: Expr -> Type`

. If you chose
to use the `type=?`

function we have provided, include it with your
test suite.

#### Extra Credit

For a very small amount of extra credit, write a program in this language for which your algorithm infers the type

(t-fun (t-var 'a) (t-var 'b))You shouldn’t attempt this problem until you’ve fully completed the assignment.

#### What Not To Do

You do *not* need to implement an interpreter for this language.

You do *not* need to implement let-based polymorphism.

#### Handin

A single member of your team should handin the assignment. From the directory containing the files for the assignment you wish to hand in, execute

/course/cs173/bin/cs173handin typei