Church encoding in Scheme: Desugaring numbers, lists, booleans, conditionals and recursion into lambda.

A compiler will often desugar complex language constructs into simpler yet equivalent language constructs. This desugaring reduces the number of cases to consider when translating into an intermediate representation. For example, a C compiler might translate for loops into while loops. In languages which contain the λ-calculus as their core, the desugaring process, taken to its limit, will desguar every program into a language with only three expression types: variable references, single-argument anonymous functions and function calls. In other words, the following subset of Scheme is sufficient for universal computation:

 <exp> ::= <var>
        |  (lambda (<var>) <exp>)
        |  (<exp> <exp>)

For my advanced compilers class, I cooked up a demonstration of Church encodings [commented code below], which shows how these techniques work.

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.