11:59:59pm (via the submit server)

- 10/3 6pm: updated the tarball to fix
small problems in fmain.ml (prints better now) and added file
`tests.f`for testing type inference. - 10/8 8:30am: updated the tarball to print a more useful error message when the final term fails to type check.

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

(Def int_id (Lam x:Int x)) (Def intfun_id (Lam x:Int->Int x))Parentheses are also permitted, to avoid ambiguity, as in

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

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

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

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:

- You should only generalize values, according to the value restriction.
- You can confirm that 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.

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.