Programming Languages

EF♭ Type Inferencer

Due on Wednesday, November 26th 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 Courselore or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask and learn than to guess!

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 starter code similar to that of the F♭ interpreter. 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. A file named src/fb/fbinterp.ml exists and contains an empty implementation of eval. You may replace this fbinterp.ml with a copy of your F♭ interpreter, but you don’t need to do so; your typechecker will not (and must not) rely upon evaluation to work.

Instead, we are largely concerned with the files src/efb/efbtype.ml and src/efb/efbinference.ml. The file src/efb/efbtype.ml contains a definition of the efbtype data type and a pretty printer for it. The file src/efb/efbinference.ml contains a function infer_type which takes an expression and either returns an efbtype (the type of the provided expression) or raises a TypeError exception (if the expression contains 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 type 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. You are encouraged to consider cycle checking once you have completed the rest of the work and your instructor will happily discuss this task with you!
  2. You do not have to implement type checking for Let Rec expressions, though you are again encouraged to do so after the rest of the assignment if you’re feeling ambitious!
  3. You are not required to implement Let-polymorphism from PEF♭.

Note that you should not have to change the starter code files other than src/efb/efbinference.ml. You are permitted to create new files for organizational purposes if you prefer.

Reference Implementation

As before, you are provided a reference implementation of the EF♭ interpreter in the binaries directory. You can run this reference implementation using the command

./binaries/efb.exe

You may wish to use rlwrap for a nicer toploop interface.

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 possible but difficult to accomplish without the use of state. To assist, a helper function fresh_tvar has been provided in the starter code. For instance, you might write

let tv1 = fresh_tvar () in   (* produces a type variable *)
let tv2 = fresh_tvar () in   (* produces a *different* type variable *)
...

Each call to fresh_tvar () will create a different type variable. Note that this is unusual: in most of the OCaml we’ve written, a call to the same function with the same arguments always produces the same result. But the fresh_tvar function uses a reference cell _next_tvar_num to keep track of the next type variable it will produce in order to ensure that it is fresh. This side effect allows us to produce different results on each call.

Deliverables

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

Submitting

It is not enough to push your work. In your repository, you will find a Python script called submit.py. In order to submit your lab assignment, it should be sufficient to run that script by typing python3 submit.py in your terminal. For this script to work correctly, you must have committed all uncommitted files in your repository and pushed your work so that your repository is in sync with your GitHub remote repository.

The aforementioned Python script is designed to create a Git tag: a name for a specific commit in your repository. (The script also performs a series of checks to help ensure that the tag you create contains what you likely think it contains.) The tag will be named using the words “submission”, the name of your assignment, and a version number. Your instructor will know that you have submitted your work because this tag will appear in your repository. If you need to resubmit your work to correct changes after receiving a grade, you can simply create new commits and then create another tag (preferrably with submit.py). At any given time, only your most recent outstanding submission will be graded.

Lab Questionnaire

In addition to completing the lab itself, you’ll also need to complete a questionnaire describing your experience in the lab. Under most circumstances, this questionnaire will take only about a minute to complete and is part of your participation grade. Please make sure to do this; the information lets me know whether I’m asking for the right amount of work and helps to ensure that it’s a good use of your time.

If You Have Trouble…

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