What You Will Learn in This Article

– Typed lambda calculus

Introduction

Having completed learning about lambda calculus in *Introduction to Functional Programming 3*, you’re now ready to study typed lambda calculus. Let’s dive into an explanation of typed lambda calculus.

(For information on lambda calculus, check here↓)

Introduction to Functional Programming 3 (Lambda Calculus)

Typed Lambda Calculus

Typed lambda calculus involves assigning types to lambda terms for computation. Types can be either basic types or function types in the form \( A \to B \), using types \( A \) and \( B \). Basic types include examples like the integer type \( i \) or the boolean type \( o \). Each variable is associated with a specific type. For instance, variable \( z \) could have type \( o \), and \( f \) could have type \( i \to i \). If \( f \) has type \( i \to i \) and \( a \) has type \( i \), the type of \( fa \) would be \( i \).

Recall that lambda terms are constructed from variables using abstraction and application. By defining rules for types in abstraction and application, types can be assigned to lambda terms. For abstraction \( \lambda a.M \), if \( a \) has type \( A \) and \( M \) has type \( B \), the type of \( \lambda a.M \) is \( A \to B \). For application \( MN \), if \( M \) has type \( A \to B \) and \( N \) has type \( A \), the resulting type is \( B \). If \( M \) does not have type \( A \to B \) or \( N \) does not have type \( A \), the application \( MN \) is invalid and does not have a type.

Types and Reduction

In the lambda calculus section, we studied \( \beta \)-reduction. A key question is whether \( \beta \)-reduction preserves types. For example, consider the lambda term \( (\lambda x.\lambda y.x)w \) where \( x \), \( y \), and \( w \) all have type \( i \). The type of \( \lambda x.\lambda y.x \) is \( i \to i \to i \), and since \( w \) has type \( i \), the application \( (\lambda x.\lambda y.x)w \) has type \( i \to i \). After \( \beta \)-reduction, \( (\lambda x.\lambda y.x)w \) reduces to \( \lambda y.w \), which also has type \( i \to i \). Thus, the type remains the same before and after \( \beta \)-reduction.

This type preservation during \( \beta \)-reduction is due to the well-defined rules for abstraction and application. Incidentally, the normalization theorem proves the termination of \( \beta \)-reduction, meaning it always halts after a finite number of steps.

Conclusion

In this article, we explained typed lambda calculus. We hope this content helps you write better functional programs. Typed lambda calculus also includes the Curry-Howard correspondence, a fascinating concept that connects proofs with programs and contributes to improving program quality. This is a hot topic and will be introduced in the future. Until next time!
² indicates independent content and should remain unchanged.[/efn_note]

2. Text enclosed in ¹