What's a good resource to learn about the simply typed lambda calculus? I've read An Introduction to Functional Programming Through Lambda Calculus by  Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to learn about the typed versions of the Lambda Calculus as well, since to my understanding they seem to form the basic for most statically typed functional programming languages like Haskell. Unfortunately, all of the resources I've found online don't explain the syntax of any of the typed versions of the Lambda Calculus very well, and needless to say, this makes it very hard to learn. Does anyone know of any good resources out there to learn either the simply typed, or any other of the typed versions of the Lambda Calculus? Free, online resources are preferable, but a decently priced book on the subject would be fine as well. I'm looking for a gentle introduction, not a rigorous textbook. 
 A: You might try Introduction to lambda calculus by Barendregt and Barendsen, starting in chapter 5 (“Type assignment”).  Chapter 5 is only 8 pages long, so you will know quickly if it's not what you're looking for $\ddot\smile$.
You might be puzzled because you are looking for an additional syntax for types, but there is not necessarily any new syntax. The types might be assigned to terms implicitly or explicitly.  The former case is called "in the style of Curry" and the latter "in the style of Church".  In the Curry style of typed lambda calculus, the syntax is exactly the same as in the untyped calculus. The difference between Curry style typed calculus and untyped calculus is that terms have types associated with them, not as part of the syntax of the language, but implicitly, and you are not allowed to compose two terms $S$ and $T$ unless the types match correctly.
A: Types and Programming Languages by Benjamin C. Pierce is the standard introductory textbook for this subject. It is not cheap, and it is rigorous, but you can read it pretty easily without worrying overly much about the rigor, and it is very good.
A: Lambda Cube Unboxed by Theo Reto probably gives the gentlest free online introduction to Simply Typed Lambda Calculus and its extensions via polymorphism, type operators, and (briefly) dependent types.
A: I have CS background and was very happy to read "Lambda-Calculus and Combinators: An Introduction" by Roger Hindley. It is very good book for self learning because it has many exercises with solutions. After reading it I was able to skim over "An Introduction to Functional Programming Through Lambda Calculus" very quickly so I think this book is good. It introduced untyped as well as two sorts of typed lambda calculus. It also describes combinatory logic which is even more minimalistic than lambda calculus.
