5
$\begingroup$

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\Lambda X_2.\dots.\Lambda X_n.\lambda x:U.t)$ is a function of type $\forall \vec{X}.U\to T$ and we want to apply it to an argument of type $V$. Then we need to find types $W_1,\dots,W_n$ such that $U[\vec{X}/\vec{W}]=V$.

This is clearly another unification problem. Can we solve this problem as easily as the problem with one variable? What is the algorithm for doing this?

$\endgroup$
5
$\begingroup$

This can be solved as easily as the other problem, as in this solution. It's basically unification.

  1. Ensure that the variables $X_1,\ldots,X_n$ do not appear in $V$. Replace any variables that do by fresh ones and perform appropriate substitution into $W$.

  2. Unify $V$ and $W$ using an algorithm that finds the most general unifier (mgu). The essence of this is in the other algorithm, or, for example, page 10 of this.

  3. The resulting mgu $[\bar{X}/\bar{W}]$ is the subtitution you require.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.