Church encoding by Mark Seemann
Church encoding is a unified way to model data and functions. An introduction for object-oriented developers.
This article series is part of an even larger series of articles about the relationship between design patterns and category theory.
When asked why I like functional programming so much, I often emphasise the superior modelling ability that I get from algebraic data types. Particularly, languages like F# and Haskell have sum types in addition to the product types that most statically typed languages seem to have.
In short, a sum type gives you the ability to declare, as part of the type system, that a particular data type must be exactly one of a finite list of mutually exclusive options. This differs from common object-oriented sub-typing because class inheritance or interface implementation offers conceptually infinite extensibility. Sometimes, unconstrained extensibility is exactly what you need, but in other cases, the ability to define a closed set of cases can be an effective modelling tool. If you need an easy-to-read introduction to algebraic data types, I recommend Tomas Petricek's fine article Power of mathematics: Reasoning about functional types.
Interestingly, TypeScript has sum types, so they don't have to belong exclusively in the realm of functional programming. In this article series, you'll see an alternative way to represent sum types in C# using Church encoding.
Lambda calculus #
In the 1930s, several mathematicians were investigating the foundations of mathematics. One of them, Alonzo Church, developed lambda calculus as a universal model of computation. In a sense, you can think of lambda calculus as a sort of hypothetical programming language, although it was never designed to be a practical programming language. Even so, you can learn a lot from it.
In the untyped lambda calculus, the only primitive data type is a function. There are no primitive numbers, Boolean values, branching instructions, loops, or anything else you'd normally consider as parts of a programming language. Instead, there's only functions, written as lambda expressions:
λf.λx.f x
This looks opaque and mathematical, but most modern programmers should be familiar with lambda (λ) expressions. The above expression is an anonymous function that takes a single argument: f. The body of the function is the return value; here, another lambda expression: λx.f x. This lambda expression also takes a single argument: x.
In the untyped lambda calculus, everything is a function, so that includes f and x. The return value of the entire expression is f x, which means that the function f is applied to the value (in fact: function) x. The entire expression is therefore a higher-order function.
In C#, the corresponding lambda expression would be:
f => x => f(x)
This is a lambda expression that returns another lambda expression, which again returns the result of calling the function f with the value x.
In F#, it would be:
fun f -> fun x -> f x
and in Haskell, it would be:
\f -> \x -> f x
In both Haskell and F#, functions are already curried, so you can shorten that Haskell lambda expression to:
\f x -> f x
and the F# lambda expression to:
fun f x -> f x
This looks more like a function that takes two arguments, so alternatively, via uncurry isomorphisms, you can also write the C# representation like this:
(f, x) => f(x)
Those six lambda expressions, however, are statically typed, even though they're generic (or, as Haskellers would put it, parametric polymorphic). This means that they're not entirely equal to λf.λx.f x, but it should give you a sense of what a lambda expression is.
It turns out that using nothing but lambda expressions, one can express any computation; lambda calculus is Turing-complete.
Church encoding #
Since languages like C#, F#, Haskell, and others, include lambda expressions, you can reproduce as much of the lambda calculus as you'd like. In this article series, I'll mainly use it to show you how to represent sum types in C#. Later, you'll see how it relates to design patterns.
- Church-encoded Boolean values
- Church-encoded natural numbers
- Church-encoded Maybe
- Church-encoded Either
- Church-encoded payment types
- Church-encoded rose tree
These articles give you examples in C#. For Haskell examples, I found Travis Whitaker's article Scrap Your Constructors: Church Encoding Algebraic Types useful.
All C# code for these articles is available on GitHub.
Summary #
You can use lambda expressions to define all sorts of data types and computations. Because lambda calculus is a universal model of computation, you can learn about fundamental representations of computation. Particularly, lambda calculus offers a model of logical branching, which again teaches us how to model sum types.
Comments
James