#StackBounty: #type-theory #type-inference Proving that the failure of algorithm W implies that the program is not typable

Bounty: 100

How one does prove that if algorithm W failed for a given program $e$ and context $Gamma$, then there is no substitution $S$ and type $tau$ such that $SGamma vdash e : tau$ ?

The original paper states that from the completeness proof one can derive that “it is decidable whether $e$ has any type at all under the assumptions $Gamma$“. However, I didn’t found this proof in the literature.

The algorithm W has some failures cases: the unification algorithm failed, an identifier was not found in the context, a recursive call failed, etc.

I more interested in the hard cases, the easy ones I can do myself.

One hard case seems to be the failure of the unification.
In this case we know about the soundness and completeness of both recursive calls and, also, the non-existence of a unifier for $S_2tau_1$ and $tau_2rightarrow alpha$. How those informations can be used to prove $neg exists tau :S, SGamma vdash e_1 : e_2 : tau $ ?

This part of algorithm W may be relevant here:

$W(Gamma, e_1: e_2) =$

$quad (tau_1,S_1) leftarrow W(Gamma, e_1)$

$quad (tau_2,S_2) leftarrow W(S_1Gamma, e_2)$

$quad S leftarrow mathrm{unify}(S_2tau_1, tau_2rightarrow alpha)$ where
$alpha$ is fresh

$quad$return $(Salpha, S circ S_1 circ S_2)$

There are other hard cases, but I will be accepting an answer if it is about at least this one.

Get this bounty!!!

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.