In System F à la Church, can we automatize type inference for the for-all elimination?

Question

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is it possible to construct a function $f$ taking two terms and returning a type such that $f<{\Lambda X.t}><{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

• $f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

• $f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R}.t^T)~s}>=T$

Answer 1

I'm not really sure I've understood the question. First, I try to reduce your problem to the following unification problem:

Given a system F type τ(X) with a free (type) variable X, and a type σ.
Is it possible to find a type γ such that τ(γ) = σ ?

Here is a pseudo-code (with an exception raised when not unifiable) for solving this problem.

unify (X, σ) = σ
unify (Y, Y) = Y
unify (τ₁ → τ₂, σ₁ → σ₂) = unify(τ₁,σ₁) → unify(τ₂,σ₂)
unify (∀Y.τ(Y), ∀Y.σ(Y)) = ∀Y.unify(τ(Y),σ(Y)) (with Y a fresh variable)
unify (_,_) = raise Not_unifiable

You can prove (by induction) that γ = τ(unify(τ(X),σ) works if and only an exception is not raised.

Now for your problem you can take

f (ΛX.t) (r) = match type of t with "τ₁ → τ₂" => unify (τ₁, type of r) | _ => fail end

(of course your function f should take as argument a context if your terms are open).