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

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$

• Your question would be a little more readable if you don't put the argument to f as sub/superscripts, each containing other sub/superscripts. – Dave Clarke Sep 16 '10 at 10:21
• For reference: This kind of problem is one of the two problems solved by "Local type inference" (dl.acm.org/citation.cfm?id=345100). Also relevant should be dl.acm.org/citation.cfm?id=1086383. – Blaisorblade Oct 13 '16 at 18:56

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).