Project 3

Updates

• None

Overview

In this project, you will implement a lambda calculus interpreter and Hindley-Milner style polymorphic type inference for lambda calculus. Lambda calculus terms will be represented using the following OCaml data type, provided in types.mli:

type term =
    Int of int
  | Var of string 
  | Lam of string * term
  | App of term * term
  | Plus of term * term
  | Let of string * term * term
  | Seq of term * term

In this AST (which you can envision as coming from a parser), variables are represented as strings, and you should use normal equality over strings (=) to decide whether a variable matches a binding in a Lam or Let. The term Let(x,e1,e2) introduces polymorphism: the type of e1 is generalized and bound to x in the body e2. The last form, Seq(e1,e2), is sequencing, in which e1 is evaluated and the result discarded, and then e2 is evaluated and returned. This form isn't all that useful in pure lambda calculus (since there are no side effects), but it will come in handy when testing polymorphism.

Your first task is to implement the function eval : term->term, declared in types.mli. This function takes a term and evaluates it sing call-by-value to a normal form, if one exists under call-by-value evaluation. Your implementation should go in types.ml

Your next task is to implement the function type_inf : term->typ, also declared in types.mli. You should write your implementation in types.ml. You should also implement (we've provided you a head start) print_type : typ->unit, which prints a type to standard output (we'll need this or grading. We've provdied you with some test case in test.ml as well as a Makefile.

In types.ml, we've given you an initial data type for types, which you can modify as needed:

type typ =
    TInt
  | TFun of typ * typ

We've included integer and function types. You'll also need to add type variables and type schemes (polymorphic types). You can do this in any way you choose, but here is one suggestion for type variables: add a constructor to typ of the form

  | TVar of int * (typ option ref)

In this representation, type variables are numbered as integers (you could also use strings) so that we can tell them apart. It also makes generating fresh type variables easy; just increment a global counter and build a TVar with the new name.

The other part of TVar is used for unification. It uses the option type, which we've seen before. As you perform type inference, you will need to unify type variables with other types. Rather than use an explicit substitution, we represent this information using a union-find data structure, as we discussed in class. Each type variable has an associated typ option ref that holds the equivalence class representative (ecr) of the variable. If the variable is currently its own ecr, i.e., it is unconstrained, then the ref points to None. For example, to make a fresh type variable, you can use TVar(<next var>, ref None). During type inference, when we discover that a type variable must be unified with some other type, we set the variable's ecr to point to the other type, i.e., x_ecr := Some <other type>, after doing a suitable occurs check. Note that you do not need to follow this implementation idea; it is just a suggestion.

Other miscellaneous issues:

• You should infer the most general type of a term (i.e., use algorithm W).
• You should assume that all terms are closed. Thus, most likely type_inf will call an internal function type_inf' : env->term->typ with the empty type environment. You will need to choose your own representation of environments.
• You should only generalize functions. In other words, in inferring a type for Let(x,e1,e2), don't generalize the type of e1 unless it is a syntactic Lam.
• Your type_inf function should raise Type_error when it is given a term that has no type.
• You can confirm your type inference implementation is producing the right results by translating your test cases into OCaml and then asking OCaml to give you their types.

Initial Code and What to Submit

Here is a skeleton for your project.

Please submit all files needed to build your application. You may of course create additional .ml files if you need. Please make sure we can build your application with make. We will test your code by plugging in our own test.ml, running make, and then checking the output.

Academic Integrity

The Campus Senate has adopted a policy asking students to include the following statement on each assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this assignment." Consequently your program is requested to contain this pledge in a comment near the top.

Please carefully read the academic honesty section of the course syllabus. Any evidence of impermissible cooperation on projects, use of disallowed materials or resources, or unauthorized use of computer accounts, will be submitted to the Student Honor Council, which could result in an XF for the course, or suspension or expulsion from the University. Be sure you understand what you are and what you are not permitted to do in regards to academic integrity when it comes to project assignments. These policies apply to all students, and the Student Honor Council does not consider lack of knowledge of the policies to be a defense for violating them. Full information is found in the course syllabus---please review it at this time.