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

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

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

<pre><code>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
</code></pre>

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

<p>Now for your problem you can take </p>

<pre><code>f (ΛX.t) (r) = match type of t with "τ₁ → τ₂" =&gt; unify (τ₁, type of r) | _ =&gt; fail end
</code></pre>

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

CC BY-SA 2.5
2010-09-16T13:08:23.643Z
2010-09-16T13:08:23.643Z
Marc
<p>The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by <em>applying</em> this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.</p>

<p>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&lt;{\Lambda X.t}>&lt;{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?</p>

<p>Some examples:</p>

<ul>
<li><p>$f&lt;{\Lambda X.\lambda x^{X\to X}.t}>&lt;{\lambda x^T.x}>=T$.</p></li>
<li><p>$f&lt;{\Lambda X.\lambda x^X.r}>&lt;{(\lambda x^{R}.t^T)~s}>=T$</p></li>
</ul>

CC BY-SA 3.0
2016-10-13T18:56:26.763Z
For reference: This kind of problem is one of the two problems solved by "Local type inference" (http://dl.acm.org/citation.cfm?id=345100).
Also relevant should be http://dl.acm.org/citation.cfm?id=1086383.
Blaisorblade
CC BY-SA 2.5
2010-09-16T10:21:16.580Z
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
<type-theory><polymorphism><type-inference>
In System F à la Church, can we automatize type inference for the for-all elimination?
Alejandro DC
# In System F à la Church, can we automatize type inference for the for-all elimination?

(Asked by: username_0 on 2010-09-16)

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$

**Tags:** type-theory, polymorphism, type-inference

> **Comments:**
> **username_2**: 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.  
> **username_1**: For reference: This kind of problem is one of the two problems solved by "Local type inference" (http://dl.acm.org/citation.cfm?id=345100). Also relevant should be http://dl.acm.org/citation.cfm?id=1086383.  

---

## 1 answers

### Answer by username_3 on 2010-09-16. Score: 8 | Accepted answer

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


---

