Why will the Hindley-Milner algorithm never yield a type like t1 -> t2? - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-09-18T13:39:31Z https://cs.stackexchange.com/feeds/question/19430 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/19430 14 Why will the Hindley-Milner algorithm never yield a type like t1 -> t2? Juan https://cs.stackexchange.com/users/10401 2014-01-01T03:28:39Z 2015-01-03T04:12:58Z <p>I'm reading about <a href="http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system" rel="nofollow noreferrer">the Hindley-Milner typing algorithm</a> while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the arguments will determine the final type, such as <code>t1 -&gt; t1</code> or <code>(t1 -&gt; t2) -&gt; (t1 -&gt; t2)</code> where <code>t1</code> and <code>t2</code> are type variables.</p> <p>I cannot think of a way you'd get something like <code>t1 -&gt; t2</code> or simply <code>t1</code>, which I understand would mean the algorithm is broken since there would be no way to determine the actual type of the expression. How do you know you'll never get a type such as these "broken" ones as long as every variable is bound?</p> <p>I know the algorithm yields types with variables, but these are always resolved once you pass the arguments to the function, which wouldn't be the case in a function with type <code>t1 -&gt; t2</code>. This is why I want to know how we know for sure the algorithm will never yield such types. </p> <p>(It seems that <a href="https://cs.stackexchange.com/a/304">you can get these "broken" types in ML</a>, but I'm asking about lambda calculus.)</p> https://cs.stackexchange.com/questions/19430/why-will-the-hindley-milner-algorithm-never-yield-a-type-like-t1-t2/19431#19431 16 Answer by Gilles for Why will the Hindley-Milner algorithm never yield a type like t1 -> t2? Gilles https://cs.stackexchange.com/users/39 2014-01-01T04:32:28Z 2014-01-01T04:32:28Z <p>In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$, but there is a term of type $\forall \alpha.\; \alpha\mathbin\rightarrow\alpha$ (the identity function $\lambda x.x$).</p> <p>Intuitively, a term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$ requires being able to build an expression of type $\beta$ from thin air. It is easy to see that there is no <strong>value</strong> which has such a type. More precisely, if the type variable $\beta$ does not appear in the type of any term variable in the environment, then there is no term of type $\beta$ which is in head normal form. You can prove this by structural induction on the term: either the variable at the head would have to have the type $\beta$, or one of the arguments would have to have a principal type involving $\beta$, i.e. there would be a smaller suitable term.</p> <p>Just because there is no value of a certain type doesn't mean that there is no term of that type: there could be a term with no value, i.e. a non-terminating term (precisely speaking, a term with no normal form). The reason why there is no lambda term with such types is that all well-typed HM terms are strongly normalizing. This is a generalization of the result that states that simply typed lambda calculus is strongly normalizing. It is a consequence of the fact that <a href="http://en.wikipedia.org/wiki/System_F" rel="nofollow noreferrer">System F</a> is strongly normalizing: System F is like HM, but allows type quantifiers everywhere in types, not just at the toplevel. For example, in System F, $\Delta = \lambda x. x \, x$ has the type $(\forall \alpha. \alpha) \rightarrow (\forall \alpha. \alpha)$ — but $\Delta\,\Delta$ is not well-typed.</p> <p>HM and System F are examples of type systems that have a <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow noreferrer">Curry-Howard correspondence</a>: well-typed terms correspond to proofs in a certain logic, and types correspond to formula. If a type system corresponds to a consistent theory, then that theory does not allow proving theorems such as $\forall A, \forall B, A \Rightarrow B$; therefore there is no term of the corresponding type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$. The type system allows one to deduce “<a href="http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps.gz" rel="nofollow noreferrer">theorems for free</a>” about functions over data structures.</p> <p>This result breaks down as soon as you add certain constants to the calculus. For example, if you allow a general <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator" rel="nofollow noreferrer">fixpoint combinator</a> such as $Y$, it is possible to build terms of arbitrary type: $Y (\lambda x.x)$ has the type $\forall \alpha. \alpha$. The equivalent of a general fixpoint combinator in the Curry-Howard correspondence is an axiom that states $\forall A, \forall B, A \Rightarrow B$, which makes the logic obviously unsound.</p> <p>Finding the fine line between type systems that ensure strong normalization and type systems that don't is a difficult and interesting problem. It is an important problem because it determines which logics are sound, in other words which programs embody proofs of theorems. You can go a lot further than System F, but the rules become more complex. For example, the <a href="http://en.wikipedia.org/wiki/Calculus_of_inductive_constructions" rel="nofollow noreferrer">calculus of inductive constructions</a> which is the basis of the <a href="http://en.wikipedia.org/wiki/Coq" rel="nofollow noreferrer">Coq proof assistant</a>, is strongly normalizing yet is capable of describing common inductive data structures and algorithms over them, and more.</p> <p>As soon as you get to real programming languages, the correspondence breaks down. Real programming languages have features such as <a href="https://cs.stackexchange.com/questions/302/ml-function-of-type-a-b">general recursive functions</a> (which may not terminate), exceptions (an expression that always raises an exception never returns a value and hence can have any type in most type systems), recursive types (which allow non-termination to sneak in), etc.</p>