CS223 Homework 5
Due Friday, 5/14/2010

1. Define SML structures corresponding to the Num class instances for rationals and complex numbers from
Homework 3, Problem 1.  Include the EQ instances as well as part of the structures.  In the case of 
rationals, include normalization of representations as discussed in Homework 3 solution (sol3.txt).

2. (a) Define a Unify functor (parameterized module) implementing an abstract and generalized version unification
algorithm described in Lecture 13 (script13.pdf). The functor parameter should consist of an interface for
manipulating variables, terms, and substitutions in the ways required by the unification algorithm.
Here is a sample of some of the operations the generalized unification algorithm will need to perform
on variables, terms and substitutions (you might discover more are needed):

(i) Test whether a term is a variable or a compound term (treating constants as a kind of compound term).

(ii) Test whether a variable occurs in a term (for use in the occurrence test).

(iii) Test whether two compound terms have the same head function symbol.

(iv) Return a list of the immediate subterms of a term (i.e. for t = F(t1, t2, t3) this would be [t1,t2,t3]). 
This should be the empty list for a constant term (thinking of constants as nullary function symbols).

(v) Add a variable to term binding to a substitution.

(vi) Form the composition of two substitutions.

(vii) Apply a substitution to a term.


(b) Having defined this unification functor, define a argument structure for it that corresponds to the
particular term structure used in the unification example in Lecture 13.


(c) Here is another form of term which can the basis for unification.

    type var = string    (* variables are strings *)

    type atom = unit ref   (* atoms have no interesting properties other than equality *)

    type funsym = {name : string, arity: int, ident: atom}
    (* test equality of funsyms by comparing their ident values *)

    datatype term
      = Var of var
      | App of funsym * term list     (* for a well-formed term, the length of the list of args = arity of funsym *)

Define an appropriate argument structure for the Unify functor of part (a) based on this term structure,
and apply Unify to this argument to provide unification for these terms. Test on a couple of nontrivial
examples.


(d) Define a simple version of SML types as a term language based on this implement an argument 
structure for the Unify functor so that it provides unification of type terms, which could be 
used in an implementation of SML type inference.


Bonus Project.  Use the result in (d) as part of a type checker for a stripped down mini-ML language with
ints, bools, and lists, with polymorphic types and type inference.  This is nontrivial.  The type
terms would have to be extended with polymorphic types.