patternMinor
Check if a lambda constructor is well-typed
Viewed 0 times
typedconstructorwellchecklambda
Problem
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)$$
when can we say that we cannot give a type to a lambda constructor?
For example
$$(λx.λy.y(x\ y))(λz.z)$$
Solution
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
-
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
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
Context
StackExchange Computer Science Q#105948, answer score: 8
Revisions (0)
No revisions yet.