In this project, you will implement a type checker and a type inference analysis for the F language we introduced in project 1.
Grab this file to get started.
You should submit one file: f.ml that contains your solutions to parts 1 and 2. You only have to implement the type checking and type inference functions, but feel free to add in your implementations from project 1, too (fmain.ml will still try to evaluate the terms).
type term = ... | Lam of string * (typ option) * term ... type typ = TInt | TFun of typ * typWe ignored this then, but we'll use it now. In particular, the parser we provided you is able to take typing annotations such as Int and Int -> Int, as in
(Def int_id (Lam x:Int x)) (Def intfun_id (Lam x:Int->Int x))Parentheses are also permitted, to avoid ambiguity, as in (Int->Int)->Int.
Extend your interpreter from project 1 to define the function typecheck : (string * typ) list -> term -> typ, where the first argument is the typing environment, implemented as a list, and the second is the term to type check. We have provided a new fmain.ml that takes as an option -typecheck which, when set, will invoke your typecheck function. Use the simply-typed lambda calculus typing rules (i.e., do not use polymorphism for this part). If a term fails to type check, you will raise the exception Type_error(s) with s as some explanation of the problem.
Note that you will not be able to typecheck some of the terms from your encodings used in project 1, e.g., the Y combinator. Also, the type checker will expect that all lambda terms have a type annotation Some t. If a lambda term fails to have such an annotation (i.e., your type checker finds None) then that should be considered a type error.
type scheme = Type of typYou should extend this definition and your definition for typ to support type inference (the latter extension will cause you to add some boring cases to your type checker). In particular, you will need to add type variables to typ and a definition of polymorphic types to scheme. You can do this in any way you choose. You must also change the implementations of print_type and print_scheme to handle your extensions.
In the lecture notes, we showed you how, for monomorphic type inference, constraints are generated from derivations and solved separately. The alternative, as in algorithm W, is to solve the constraints on-line, while traversing the term. If we take this approach, we can implement type variables as follows, encoding a kind of union-find algorithm. First, 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 is a top-level primitive defined as
type 'a option = None | Some of 'a(This is built in to the OCaml compiler, so there's no real definition of it anywhere; there's only a comment in pervasives.ml.) 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. 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, we 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 we can end up having a type variable point to another type variable, which points to another type variable, etc. The last type in this chain is the ecr of the type.
You should generalize at Let and at each Def that is bound to a value (a Def is really a kind of top-level Let). Do this by implementing the function generalize : (string * scheme) list -> typ -> scheme. The scaffolding in fmain.ml will call this function to generalize top-level definitions. Your function should generalize the given type within the given environment; i.e., generalize env t will create a polymorphic type that quantifies those free variables in t that are not free in env. You should instantiate at variable occurrences, as described in class.
Using this algorithm, you are essentially implementing W. That said, you are free to implement type inference however you like; this is just a suggestion. Other miscellaneous issues:
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.