When prototyping a new language or a new static analysis, Church encodings become practical. Since any language construct may be desugared into a pile of lambdas, a researcher can bring the language down to the interpreter/analysis, rather than the interpreter/analysis to the language.
The Church encoding philosophy also allows practicing programmers to extend a language with new features from with the language itself, so long as that language contains anonymous functions.
More Church-encoding resources:
- Types and Programming Languages is the modern resource on the λ-calculus and advanced topics in programming language theory. It covers more Church-encoding schemes, including special Church-encodings that work only in lazy languages like Haskell.
Related blog posts:
- Compiling Scheme to C with closure conversion.
- Compiling Scheme to Java with closure conversion.