Blog: Typed lambda calculus

In this piece, we focus on introducing types to lambda calculus. Typed lambda calculus extends the untyped lambda calculus by introducing a type system. It's important to note that, unlike untyped lambda calculus, there are multiple typed lambda calculi, each differentiated by the specific features of the type system used. The exact features of the type system can be chosen with considerable flexibility. In this article, we will explore some of the common choices.