What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

Question

I was given an exercise that asked me to assign a simple type to the lambda term: $$ \lambda a.a(\lambda yt.t)(ya) $$ but I couldn't find one, furthermore, the lambda term seems untypable to me because of the double reference to $a$.

This is my reasoning:

• let $t$ be of type $\alpha$, then $\lambda t.t$ has type $\alpha \rightarrow \alpha$;
• let then $y$ have type $\beta$, and so $\lambda yt.t$ has type $\beta \rightarrow \alpha \rightarrow \alpha$;
• let now give $a$ the type $\beta \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$, in order for the term $a(\lambda yt.t)$ to be of type $\alpha \rightarrow \alpha$.

From here I want $(ya)$ to be of type $\alpha$, so that the final term $a(\lambda yt.t)(ya)$ has a well-defined type, but the problem is that $y$ and $a$ both have already some defined types, which are not compatible (I cannot apply $a$ to $y$). However I assign types to $y$ and $a$, and I cannot find a type compatibility.

Can you please help me out? Is the lambda term typable in the first place? And if so, where am I wrong?

Answer 1

Be careful: the two $y$ aren't “the same”, there's a bound one and a free one. You should first perform an α-equivalence step to rename the former: $$\lambda a.a(\lambda yt.t)(ya) =_α λa.a(λzt.t)(ya). $$

Also, in the third step you make an erroneous assumption: by assigning to $a$ the type $\beta \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$, you assume that $(ya)$ is of type $α$ and that the whole term is also of type $α$ (ie. have the same type as $t$). There is no reason why this should be the case.

Let's start again from the beginning:

• $λzt.t$ is of type $β\to α\to α$ for some $α,β$,
• $(ya)$ is of type $\delta$, where $y$ is of type $\gamma \to \delta$ and $a$ is of type $\gamma$, for somme $\gamma,\delta$,
• then $a(λzt.t)$ must be of type $\delta\to\epsilon$, for some $\epsilon$,
• then $a$ must be of type $(β\to α\to α)\to \delta \to \epsilon$, for some $\epsilon$,
• and finally the whole term is of type $((β\to α\to α)\to \delta \to \epsilon) \to \epsilon$.

$\gamma$ disappeared but we know it is equal to $((β\to α\to α)\to \delta \to \epsilon) \to \delta$.

However, instead of writing the proof like this, you should write a derivation tree which would enable you to keep better track of the context (ie. the type of the free variables in subterms).