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

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?

• As a gentle suggestion, any Haskell or OCaml compiler will be able to find any simple type, should one exist.
– cody
Commented Sep 9, 2023 at 2:38
• There's also the matter of that $y$ variable which seems to be out of scope in your term.
– cody
Commented Sep 9, 2023 at 2:40

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

• Thanks so much for the answer. Yes, I know about the tree structure to solve the problem but I didn't know how to write it here. I didn't think about the two y as different variables, but now everything makes sense. Thanks again! Commented Sep 9, 2023 at 9:57