# Check if a lambda constructor is well-typed

In basic type inference for 𝜆-calculus with parametric polymorphism à la Hindley–Milner, when can we say that we cannot give a type to a lambda constructor? For example $$(λx.λy.y(x\ y))(λz.z)$$

A term $$M$$ is well-typed if and only if there is a type derivation that leads to a judgement of the form $$\Gamma \vdash M : \tau$$ for some context $$\Gamma$$ and some type $$\tau$$. (I use the word “type” in its general sense which can include quantified variables; in the terminology commonly used with Hindler-Milner, that's a type scheme.) So, to prove that you cannot give a type to a lambda term from first principles, you prove that there is no type derivation that leads to such a judgement.

Hindley-Milner has a nice property in this respect: it's syntax-directed, i.e. it's presented as a set of deduction rules such that for any term, there is a single rule that can be used to end a deduction of this term. (Being syntax-directed is actually a property of a presentation of the type system, not a property of the type system. In this post, I use the classical syntax-directed presentation which builds generalization into the let rule, rather than having a separate rule for generalization.)

Another nice property (shared by almost every type system) is that unused variables can always be removed from the context. So for example, if $$(\lambda x y.y (x y)) (\lambda z.z)$$ is well-typed, it must have a type derivation ending with the App rule and, since the term has no free variable, an empty context: $$\dfrac{\vdash (\lambda x y.y (x y)) : \tau_1 \to \tau_0 \qquad \vdash (\lambda z. z) : \tau_1} {\vdash (\lambda x y.y (x y)) (\lambda z.z) : \tau_0}$$

You can of course make use of any theorem that you already know. In particular, the principal typing theorem can be useful: if a term is well-typed then all of its types are instances of a particular one. For example, the identity function $$(\lambda z.z)$$'s possible types are all instances of $$\forall \alpha. \alpha \to \alpha$$. Similarly, it's easy to see that the function $$(\lambda x y.y (x y))$$ has the most general type $$\forall \beta \gamma. ((\beta \to \gamma) \to \beta) \to ((\beta \to \gamma) \to \gamma)$$.

In order to find a type for $$(\lambda x y.y (x y)) (\lambda z.z)$$, we saw above that we need to find types $$\tau_0$$ and $$\tau_1$$ such that $$\tau_1 \to \tau_0$$ is an instance of $$\forall \beta \gamma. ((\beta \to \gamma) \to \beta) \to ((\beta \to \gamma) \to \gamma)$$ and $$\tau_1$$ is an instance of $$\forall \alpha. \alpha \to \alpha$$. This means that there must exist base types $$T_1$$, $$T_2$$ and $$T_3$$ which satisfy the equations \begin{align} \tau_1 &= \forall \alpha \beta \gamma. (T_2 \to T_3) \to T_2 \\ \tau_0 &= \forall \alpha \beta \gamma. (T_2 \to T_3) \to T_3 \\ \tau_0 &= \forall \alpha \beta \gamma. T_1 \to T_1 \\ \end{align} Hence $$T_3 = T_1 = (T_2 \to T_3)$$. But this is impossible due to the structure of types: a type can't be a strict subterm of itself. Therefore the premise of was wrong: the term $$(\lambda x y.y (x y)) (\lambda z.z)$$ is not well-typed.

chi's answer shows how to use another theorem about Hindley-Milner to shorten the proof: subject reduction, i.e. the property that if a term is well-typed and it reduces to another term then that other term also has the same type. Since $$(\lambda x y.y (x y)) (\lambda z.z) \to_\beta^* \lambda y. y y$$, if the original term has a type then so does $$\lambda y. y y$$. By contraposition, if $$\lambda y. y y$$ is not well-typed then neither is the original term. You can show that $$\lambda y. y y$$ is not well-typed by a shorter application of the methodology above: note that if it is well-typed, it must be an application of the lambda typing rule, which leads to a type equation of the form $$T_1 \to T_1 = T_1$$, which has no solution for the same reason as before.

There are, of course, other type systems where the term in question is well-typed. These type systems must have some additional ways of typing terms that Hindley-Milner doesn't have. I'll give two examples:

• If you extend the syntax of types to allow them to be recursive (as with ocaml -rectypes), then the reasoning about the type equation having no solution because a type can't contain itself breaks down, and indeed both $$\lambda y. y y$$ and the original term are well-typed in this system. For example, the most general type of $$\lambda y. y y$$ is $$\forall \alpha \beta [\alpha = \alpha \to \beta]. \alpha$$.

• If you add a rule that allows intersection types: $$\dfrac{\Gamma \vdash M : \tau_1 \qquad \Gamma \vdash M : \tau_2} {\Gamma \vdash M : \tau_1 \wedge \tau_2}$$ then the reasoning above breaks down because the presentation of the type system is not type-directed. The intersection rule can be used with any language construct. With this type system, $$y : \alpha \wedge (\alpha \to \beta) \vdash_{\wedge} y : \alpha$$ and $$y : \alpha \wedge (\alpha \to \beta) \vdash_{\wedge} y : \alpha \to \beta$$ and so $$\lambda y. y y$$ has the type $$\forall \alpha \beta. (\alpha \wedge (\alpha \to \beta)) \to \beta$$. The original term is also well-typed. With a rule that departs so radically from being syntax-directed, you might think that it's difficult to prove that a term is not typable, and you'd be right: the intersection rule is so strong that it causes all strongly normalizing terms to be well-typed. Conversely, intersection types with base types (but without quantifiers or a top type) only allow strong normalizing terms, so to prove that a term is not typable in that system, it's sufficient to prove that a term is not strongly normalizing. See Does there exist a Turing complete typed lambda calculus?) for more information about intersection types.

No, that term can not be typed in Hindley Milner, or any other "standard" type system. Here's a rough sketch of a proof.

Suppose by contradiction it had a type. Since type is preserved under beta reduction (by the subject reduction theorem) we would get that all these terms also have the same type

$$\begin{array}{l} (λx.λy.y(x\ y))(λz.z) \\ (λy.y((λz.z)\ y) \\ (λy.y\ y) \\ \end{array}$$

The last term is however not typeable, since $$y$$ should have a function type $$\tau_1 \to \tau_2$$ because it is applied as a function, but since $$y$$ itself is the argument we should also have that $$y$$ has type $$\tau_1$$. Since $$\tau_1 = \tau_1\to\tau_2$$ is impossible, we obtain a contradiction.

Another way to see the same fact is running the type inference algorithm: doing so at a certain point would require to solve the equation $$\tau_1 = \tau_1\to\tau_2$$, triggering the failure of type inference.

Let me add that applying a function to itself, directly or indirectly (as done above), is the archetypal way to produce a term having no type in typed lambda calculi.