Programming Languages

EF♭ Type Inferencer

Due on Wednesday, April 18th at 11:59 PM. This is a team lab. You may work alone or you may work with a partner. If you’d like to work with a partner, make sure to indicate your preferred partner using Teammaker and be familiar with the Partner Etiquette guidelines. You may discuss the concepts of this lab with other classmates, but you may not share your code with anyone other than course staff and your lab partner(s). Do not look at solutions written by students other than your team. If your team needs help, please post on the Piazza forum or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask than to risk violating the Academic Integrity Policy.

Overview

In this lab, you will implement the EF♭ type inference algorithm from Section 6.6 in the book. Your implementation will be in OCaml in a freshly provided copy of the F♭ development kit. Once you are finished, your EF♭ interpreter will reject ill-typed expressions.

Working on the Assignment

The starter code provided in this assignment is very much like the starter code provided in the F♭ interpreter assignment. The fbinterp.ml file exists and contains an empty implementation of eval. You may replace this fbinterp.ml with a copy of your interpreter from the previous assignment, but you don’t need to do so; your typechecker will not (and must not) rely upon evaluation to work.

Instead, the file fbtype.ml is central to this assignment. Your goal is to implement the typecheck function, which accepts an expression and either returns a type for it (if the inference algorithm can assign it a type) or raises the TypeError exception (if the inference algorithm discovers a type error or inconsistency). The typecheck function should match the behavior of the algorithm in the book. Specifically,

  1. You must write a function which performs the initial inference of type equations for the expression.
  2. You must perform a deductive logical closure of that set of type equations.
  3. You must check that set of type equations for consistency.
  4. You must perform substitution on the resulting constrained type to provide a displayable type to the user.

To make the assignment more straightforward, there are some parts you are permitted to leave out.

  1. You are not required to perform cycle checking during your consistency check. Expressions with cyclic types may cause your inferencer to crash or loop forever. A correct implementation of cycle checking is worth a small bonus.
  2. You do not have to implement type checking for Let Rec expressions, though doing so will also earn a small bonus.
  3. You are not required to implement Let-polymorphism from PEF♭.

Note that you may not change any of the F♭DK files other than fbtype.ml. You are permitted to create new files for organizational purposes if you like.

Reference Implementation

As before, reference implementations of several languages are provided in the binaries directory. You may use ocamlrun to run them. In particular, you may wish to run

rlwrap ocamlrun binaries/fb.byte --typecheck

This will activate typechecking in the reference implementation. Your algorithm should behave the way that this typechecking algorithm behaves.

Coding in OCaml

The internal structure of your typechecking algorithm is up to you (although you will certainly have to write some helper functions!). You probably want at least one helper for each of the main steps of the algorithm above. Remember to refer to the OCaml Transition Guide if you have any questions about how to accomplish various algorithmic tasks in OCaml.

One task you will certainly want to perform involves the creation of “fresh” type variables. This is somewhat difficult to accomplish in pure OCaml code: each function would have to accept some parameter describing the next unusued type variable and return its new value. This is error-prone and tedious. Instead, we can make use of OCaml’s mutation features. You may put a single mutable variable in fbtype.ml, such as:

let _next_tvar = ref 0;;

When you need a new type variable, you can use this mutable variable as a counter to pick the next type variable in sequence (named e.g. a0, a1, etc.). The syntax in OCaml for accessing and updating reference cells is the same as in F♭S: e := e and !e.

Deliverables

Your grade on this assignment will be determined by the correctness of your type inferencer as defined in fbtype.ml. Don’t worry about efficiency; do worry about correctness!

Submitting

To submit your lab, just commit and push your work. The most recent pushed commit as of the due date will be graded. For more information on when assignments are due, see the Policies page.

If You Have Trouble…

…then please contact your instructor! Piazza is the preferred method, but you can reach out via e-mail as well. Good luck!