It's our last interpreter, this time with parametric polymorphism and type inference. Mini-project 3 is due on Thursday 5/1 by 8:00PM. It cannot be dropped. This is the landing page for the project, it doesn't contain any information about the project specification. The details of the project are given in the file assigns/interp3/spec.pdf.
For the one-week check-in, you must submit:
parser.mly.principle_type, as detailed in the mini-project specification. You should be able to leave your implementations of the other functions partial or empty as long as your code builds.Note. We will not re-test parts of the mini-project from the one-week check-in. To recieve full credit on the mini-project, you must successfully submit both the one-week check-in and the complete mini-project.
fun x -> fun y -> fun z -> x (1 + y z)For each of the following problems, let e denote the above expression.
Determine the type \tau and constraints \mathcal C such that \cdot \vdash e : \tau \dashv \mathcal C is derivable in the constraint-based inference system for mini-project 3. You must provide the derivation, and you should use the compact derivation notation we gave in lecture.
Let \mathcal C denote the set of constraints determined in the previous part. Determine a most general unifier \mathcal S for \mathcal C using the algorithm we gave in lecture. Show your work.
Apply your unifier \mathcal S from the previous part to \tau (from the first part) and quantify over it's free variables. This is the principle type of e. That is, in the notation from lecture, write down the type \forall \alpha_1 \dots \forall \alpha_k . \mathcal S \tau where \mathsf{FV}(\mathcal S \tau) = \{\alpha_1, \dots, \alpha_k\}.