Lambda calculus, invented by Alonzo Church in the 1930s, is the theoretical foundation of functional programming. It has only three constructs: variables, abstraction \( \lambda x.\text{body} \), and application \( f\,x \), yet it is Turing complete. Alpha equivalence states that bound variable names do not matter, so \( \lambda x.\,x \) and \( \lambda y.\,y \) are the same function. Beta reduction is the evaluation rule for function application, replacing \( (\lambda x.\,\text{body})\,\text{arg} \) with the body in which \( x \) is replaced by arg. Eta reduction removes redundant parameter passing when a function merely forwards its argument, while eta expansion is the inverse, wrapping a function to make its type check or delay its evaluation. The Church-Rosser theorem guarantees confluence: any two reduction sequences can be extended to meet at a common result, so a term's normal form is unique when it exists. A term is in weak head normal form when its outermost structure is not a redex, even if subexpressions remain unevaluated.
Lambda calculus can be reformulated without variables using combinators. The K combinator returns its first argument and ignores the second; the S combinator implements generalized application as \( S\,x\,y\,z = x\,z\,(y\,z) \); together with the identity combinator I, they form SKI calculus, a Turing-complete basis. A combinator is a function whose only free variables are its arguments, making combinator-heavy code highly portable and easy to test. Fixed-point combinators enable anonymous recursion: the Y combinator \( Y\,f = f\,(Y\,f) \) computes the least fixed point of \( f \) and works in lazy languages, while the Z combinator adapts the same idea for strict languages by wrapping recursive calls in thunks. Church encoding represents data as higher-order functions — Church Booleans and Church numerals are constructed purely from lambdas — while the Scott encoding represents data as functions that case-analyze themselves, supporting strict pattern matching in strict languages. Recursion schemes generalize these patterns: a catamorphism tears down a structure according to its type's shape, an anamorphism builds a structure from a seed by unfolding, and a hylomorphism fuses an unfold and a fold without materializing the intermediate structure, enabling streaming divide-and-conquer algorithms.
Category theory provides further structure. A natural transformation is a mapping between functors that commutes with fmap; the Yoneda lemma says \( \forall b.\, (a \to b) \to f\,b \) is isomorphic to \( f\,a \), meaning a functor is determined entirely by its action on morphisms, and the dual Coyoneda lemma gives a free construction that makes any functor a Functor automatically. A comonad is the categorical dual of a monad, providing extract and duplicate operations, and the zipper data structure — pairing a focused element with its surrounding context for O(1) navigation in an otherwise immutable structure — is a comonad satisfying left and right identity laws. The cofree comonad of a functor represents a value with a branching tree of future values, dual to the free monad, and underpins functional reactive programming. Profunctors are contravariant in one argument and covariant in the other, and they form the foundation of optics: lenses for read/write focus on substructures, prisms for focusing on a single constructor of a sum type, traversals for zero-or-more elements, isos for bijective type conversions, and getters and setters as their read- and write-only specializations. The Bifunctor class captures functors of two arguments, the Contravariant class applies functions in the opposite direction, and the natural number object with morphisms \( 1 \to N \) and \( N \to N \) embodies the Peano axioms category-theoretically.