Overview
In the previous part, we developed lambda-calculus-based languages and studied evaluation through reduction. In this part, we move to the simply typed lambda calculus (STLC) and use types to enforce stronger guarantees about programs. We will implement typing and call-by-value dynamics, and extend the core language with several practical data types.
This part is organized as follows:
-
Types Provide Confidence motivates static typing, introduces typing contexts and hypothetical typing, and presents the typing rules of STLC.
-
STLC Implementation translates the STLC typing and reduction rules into Rust code and builds a working type checker and evaluator.
-
The Natural Numbers Type extends STLC with
Nat, case analysis, and primitive recursion under call-by-value semantics. -
Big Integer Optimization replaces Peano-style naturals with efficient big-integer-backed naturals and adapts typing and dynamics accordingly.
-
Pairs and The Product Type adds product types, projections (
fst,snd), and introduces theUnittype. -
The Sum Type introduces injections (
inl,inr) and sum case analysis (scase) with corresponding typing and reduction rules. -
The List Type adds parametric lists (
nil,cons), list case analysis (lcase), and list recursion (lrec).
By the end of this part, you will have a substantially richer typed calculus and a concrete implementation that supports functions, booleans, naturals, products, sums, and lists. Finally, the chapter Recap and Feedback summarizes the part and asks for your feedback on the materials.
The materials in this part are inspired by Programming Language Foundations: STLC chapter and Types and Programming Languages by Benjamin Pierce et al.