3
$\begingroup$

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

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.