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

[article index] [] [@mattmight] [+mattmight] [rss]

A compiler will often desugar complex language constructs into simpler yet equivalent language constructs.

For example, a C compiler might translate for loops into while loops.

Desugaring simplifies compilation by eliminating cases in functions that operate on syntax.

In languages which contain the λ-calculus as their core, the desugaring process, if 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 Turing-complete:

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

Unbeknownst to many, JavaScript also contains the lambda calculus, which means the following subset of JavaScript is also Turing-complete:

 <exp> ::= <var>
        |  function (<var>) { return <exp> ; }
        |  (<exp>)(<exp>)

Encodings of high-level constructs in the λ-calculus are Church encodings.

To see how Church encodings work, read and play around with the commented code below.

Church encodings

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 resources

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: