Consider the following expression, denoted in the following problems by e.
fun x -> fun y -> fun z -> x (1 + y z)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\}.