4
$\begingroup$

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.

$\endgroup$

4 Answers 4

3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ While this link may answer the question, it is better to include the essential parts of the answer here and provide the link for reference. Link-only answers can become invalid if the linked page changes. - From Review $\endgroup$ Commented Feb 16, 2023 at 4:37
  • 2
    $\begingroup$ Added more info about the resource but as the question was what resources are helpful, the reference itself is the answer $\endgroup$ Commented Feb 16, 2023 at 4:53
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .