cs173: Assignment 6  
Version 1, 20021116 10:52FAQPart I: UnificationImplement the unification algorithm from the 20021113 notes. The algorithm should work for a generic term representation, as defined below. A term is either:
In addition, you will need data types for representing a constraint (a pair of terms) and substitution (a variable and a term). The unification algorithm will consume a list of constraints and produce either a list of substitutions or an error string. Errors can arise from two situations: when the unification of two terms is impossible, or when the occurs check fails. In both cases, you should return a string with an appropriate error message. Finally, when comparing variables for equality, use Scheme's builtin eq? function. For symbols, it behaves exactly as symbol=?; for other values, it compares them for identity (like Java's == comparison). We will rely on identical variables being deemed equivalent by eq? when solving the constraints generated in the following section. Part II: Generating Type ConstraintsFollowing the 20021111 notes, derive type constraints 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 only novelty of this language is that the list operations are now polymorphic; that is, you can create lists of values of any type. Write a function which consumes an expression of this language, and returns a list of constraints (of the type defined in Part I). The correspondence between type constraints and the terms in Part I is as follows:
Part III: Inferring TypesTo infer the type of a program, first parse it, then generate constraints, and finally unify the constraints. The result will be a list of substitutions; by looking up the subsitution for the entire expression, you can access its type. Your code needs to define only one function, infertype, which consumes a concrete representation of the program, and produces either an error string or a representation of the inferred type. Represent types concretely as: <type> ::= number  boolean  (listof <type>)  (<type> > <type>)  <string>where strings are used to represent type variables. For example, the type of length would be: ((listof "a") > number) Extra CreditFor a very small amount of extra credit, write a program in this language for which your algorithm infers the type ("a" > "b"). You shouldn't attempt this problem until you've fully completed the assignment. What Not To DoYou do not need to implement an interpreter for this language. You do not need to implement letbased polymorphism. FAQ
