Blog: 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.

Lambda calculus is a theoretic framework used to define the meaning of computation in languages like Haskell, Agda, Idris, and others. In this article, we introduce you to lambda calculus by exploring its untyped variant.