Today I learned something new! At first it was startling, but in hindsight it makes perfect sense: The Simply Typed Lambda Calculus is not Turing complete. Any well-typed program will eventually terminate, and the intuition here is that your program can only have a finite number of arrow types, and evaluation will always reduce the number of arrow-typed things that you have around. The Untyped Lambda Calculus, however, allows programs that never terminiate. I guess the Y-combinator is a pretty good example here. I once learned that the Untyped Lambda Calculus can be embedded inside the Typed Lambda Calculus by having essentially one type, the everything type. So I guess this makes sense, since there are no arrow types that can decrease monotonically...
Now I have more questions:
Does this mean the untyped lambda calculus is Turing complete?
How does the encoding of the untyped lambda calculus into the lambda calculus work? I mean, don't functions always have to have function type? Or is the everything type some kind of function type?