Check if a lambda constructor is well-typed - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-08-23T15:56:55Z https://cs.stackexchange.com/feeds/question/105948 http://www.creativecommons.org/licenses/by-sa/3.0/rdf https://cs.stackexchange.com/q/105948 4 Check if a lambda constructor is well-typed Gallaoui https://cs.stackexchange.com/users/66940 2019-03-23T14:35:40Z 2019-04-25T09:50:19Z <p>In basic type inference for 𝜆-calculus with parametric polymorphism &agrave; la Hindley&ndash;Milner, when can we say that we cannot give a type to a lambda constructor? For example <span class="math-container">$$(λx.λy.y(x\ y))(λz.z)$$</span></p> https://cs.stackexchange.com/questions/105948/-/105966#105966 6 Answer by chi for Check if a lambda constructor is well-typed chi https://cs.stackexchange.com/users/43599 2019-03-23T20:03:36Z 2019-03-23T20:09:25Z <p>No, that term can not be typed in Hindley Milner, or any other "standard" type system. Here's a rough sketch of a proof.</p> <p>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</p> <p><span class="math-container">$$\begin{array}{l} (λx.λy.y(x\ y))(λz.z) \\ (λy.y((λz.z)\ y) \\ (λy.y\ y) \\ \end{array}$$</span></p> <p>The last term is however not typeable, since <span class="math-container">$y$</span> should have a function type <span class="math-container">$\tau_1 \to \tau_2$</span> because it is applied as a function, but since <span class="math-container">$y$</span> itself is the argument we should also have that <span class="math-container">$y$</span> has type <span class="math-container">$\tau_1$</span>. Since <span class="math-container">$\tau_1 = \tau_1\to\tau_2$</span> is impossible, we obtain a contradiction.</p> <p>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 <span class="math-container">$\tau_1 = \tau_1\to\tau_2$</span>, triggering the failure of type inference.</p> <p>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. </p> https://cs.stackexchange.com/questions/105948/-/105973#105973 7 Answer by Gilles for Check if a lambda constructor is well-typed Gilles https://cs.stackexchange.com/users/39 2019-03-23T23:33:06Z 2019-04-25T09:50:19Z <p>A term <span class="math-container">$M$</span> is well-typed if and only if there is a type derivation that leads to a judgement of the form <span class="math-container">$\Gamma \vdash M : \tau$</span> for some context <span class="math-container">$\Gamma$</span> and some type <span class="math-container">$\tau$</span>. (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 <em>type scheme</em>.) 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.</p> <p>Hindley-Milner has a nice property in this respect: it's <em>syntax-directed</em>, 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 <a href="https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system" rel="nofollow noreferrer">classical syntax-directed presentation</a> which builds generalization into the let rule, rather than having a separate rule for generalization.)</p> <p>Another nice property (shared by almost every type system) is that unused variables can always be removed from the context. So for example, if <span class="math-container">$(\lambda x y.y (x y)) (\lambda z.z)$</span> 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: <span class="math-container">$$\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}$$</span></p> <p>You can of course make use of any theorem that you already know. In particular, the <em>principal typing</em> 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 <span class="math-container">$(\lambda z.z)$</span>'s possible types are all instances of <span class="math-container">$\forall \alpha. \alpha \to \alpha$</span>. Similarly, it's easy to see that the function <span class="math-container">$(\lambda x y.y (x y))$</span> has the most general type <span class="math-container">$\forall \beta \gamma. ((\beta \to \gamma) \to \beta) \to ((\beta \to \gamma) \to \gamma)$</span>.</p> <p>In order to find a type for <span class="math-container">$(\lambda x y.y (x y)) (\lambda z.z)$</span>, we saw above that we need to find types <span class="math-container">$\tau_0$</span> and <span class="math-container">$\tau_1$</span> such that <span class="math-container">$\tau_1 \to \tau_0$</span> is an instance of <span class="math-container">$\forall \beta \gamma. ((\beta \to \gamma) \to \beta) \to ((\beta \to \gamma) \to \gamma)$</span> and <span class="math-container">$\tau_1$</span> is an instance of <span class="math-container">$\forall \alpha. \alpha \to \alpha$</span>. This means that there must exist base types <span class="math-container">$T_1$</span>, <span class="math-container">$T_2$</span> and <span class="math-container">$T_3$</span> which satisfy the equations <span class="math-container">\begin{align} \tau_1 &amp;= \forall \alpha \beta \gamma. (T_2 \to T_3) \to T_2 \\ \tau_0 &amp;= \forall \alpha \beta \gamma. (T_2 \to T_3) \to T_3 \\ \tau_0 &amp;= \forall \alpha \beta \gamma. T_1 \to T_1 \\ \end{align}</span> Hence <span class="math-container">$T_3 = T_1 = (T_2 \to T_3)$</span>. 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 <span class="math-container">$(\lambda x y.y (x y)) (\lambda z.z)$</span> is not well-typed.</p> <p><a href="https://cs.stackexchange.com/a/105966">chi's answer</a> shows how to use another theorem about Hindley-Milner to shorten the proof: <em><a href="https://en.wikipedia.org/wiki/Subject_reduction" rel="nofollow noreferrer">subject reduction</a></em>, 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 <span class="math-container">$(\lambda x y.y (x y)) (\lambda z.z) \to_\beta^* \lambda y. y y$</span>, if the original term has a type then so does <span class="math-container">$\lambda y. y y$</span>. By contraposition, if <span class="math-container">$\lambda y. y y$</span> is not well-typed then neither is the original term. You can show that <span class="math-container">$\lambda y. y y$</span> 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 <span class="math-container">$T_1 \to T_1 = T_1$</span>, which has no solution for the same reason as before.</p> <p>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:</p> <ul> <li><p>If you extend the syntax of types to allow them to be recursive (as with <a href="https://caml.inria.fr/pub/docs/oreilly-book/html/book-ora209.html" rel="nofollow noreferrer"><code>ocaml -rectypes</code></a>), then the reasoning about the type equation having no solution because a type can't contain itself breaks down, and indeed both <span class="math-container">$\lambda y. y y$</span> and the original term are well-typed in this system. For example, the most general type of <span class="math-container">$\lambda y. y y$</span> is <span class="math-container">$\forall \alpha \beta [\alpha = \alpha \to \beta]. \alpha$</span>.</p></li> <li><p>If you add a rule that allows <em>intersection types</em>: <span class="math-container">$$\dfrac{\Gamma \vdash M : \tau_1 \qquad \Gamma \vdash M : \tau_2} {\Gamma \vdash M : \tau_1 \wedge \tau_2}$$</span> 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, <span class="math-container">$y : \alpha \wedge (\alpha \to \beta) \vdash_{\wedge} y : \alpha$</span> and <span class="math-container">$y : \alpha \wedge (\alpha \to \beta) \vdash_{\wedge} y : \alpha \to \beta$</span> and so <span class="math-container">$\lambda y. y y$</span> has the type <span class="math-container">$\forall \alpha \beta. (\alpha \wedge (\alpha \to \beta)) \to \beta$</span>. 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 <a href="https://cs.stackexchange.com/questions/2638/does-there-exist-a-turing-complete-typed-lambda-calculus/2639#2639">Does there exist a Turing complete typed lambda calculus?</a>) for more information about intersection types.</p></li> </ul>