Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

I'm reading about this algorithm 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 t1 -> t1 or (t1 -> t2) -> (t1 -> t2).

I cannot think of a way you'd get something like t1 -> t2 or simply t1, 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?

EDIT Seems that you can get these "broken" types in ML, but I'm asking about lambda calculus.

share|improve this question
    
What do you mean by “broken type”? What are t1 and t2: type variables? HM is a typing algorithm for ML, so it does often yield types with variables, for any term that's polymorphic. Is this a source of confusion? –  Gilles Jan 1 at 3:31
    
Yes, t1 and t2 are type variables. I know it yields types with variables, but these are always always resolved once you pass the arguments to the function, which wouldn't be the case in a function with type t1 -> t2. This is why I want to know how do we know for sure the algorithm will never yield such type. –  Juan Luis Soldi Jan 1 at 3:34
    
Oh, I understand the question now. You can get such “broken” types in ML. (Hint: there is no value that has the type $\forall \alpha, \alpha$. So the type has to be on an expression that has no value.) –  Gilles Jan 1 at 3:47
    
Can you give an actual example in lambda calculus of such an expression (sorry I don't know ML)? –  Juan Luis Soldi Jan 1 at 3:55
2  
Take a non-terminating term, such as $Y (\lambda f. \lambda x. f x)$. There's a brief explanation in Stéphane's answer. If you need more explanations, edit your question to state what language you're working in (pure lambda calculus? with constants?) and what part you need explanations about, and we can reopen this question. –  Gilles Jan 1 at 4:03

1 Answer 1

up vote 10 down vote accepted

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

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 value 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.

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 System F 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.

HM and System F are examples of type systems that have a Curry-Howard correspondence: 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 “theorems for free” about functions over data structures.

This result breaks down as soon as you add certain constants to the calculus. For example, if you allow a general fixpoint combinator 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.

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 calculus of inductive constructions which is the basis of the Coq proof assistant, is strongly normalizing yet is capable of describing common inductive data structures and algorithms over them, and more.

As soon as you get to real programming languages, the correspondence breaks down. Real programming languages have features such as general recursive functions (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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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