Project 2: Church Encodings - Numbers, Booleans, and Data from Nothing

Project 2: Church Encodings - Numbers, Booleans, and Data from Nothing

Metadata

Attribute	Value
Title	Church Encodings: Numbers, Booleans, and Data from Nothing
Difficulty	Advanced
Main Language	Haskell
Alternative Languages	Racket, OCaml, JavaScript (for comparison)
Prerequisites	Project 1 (Lambda Calculus Interpreter), understanding of higher-order functions
Estimated Time	1-2 weeks
Knowledge Area	Lambda Calculus / Church Encodings
Main Book	“Learn You a Haskell for Great Good!” by Miran Lipovaca

---

Learning Objectives

By completing this project, you will be able to:

1. Explain how pure lambda calculus represents data as behavior - understanding that numbers, booleans, and data structures are patterns of function application rather than primitive values.

2. Implement Church numerals and perform arithmetic - encoding natural numbers as functions and deriving addition, multiplication, and exponentiation from first principles.

3. Solve the predecessor problem using Kleene’s trick - understanding why subtraction is fundamentally harder than addition in Church encoding.

4. Build Church booleans and conditional logic - encoding true, false, and if-then-else as pure functions.

5. Construct Church pairs and lists - encoding compound data structures as functions that accept selectors.

6. Implement recursion without names using the Y combinator - understanding fixed points and how anonymous recursion is possible.

7. Connect Church encodings to practical programming - recognizing these patterns in continuation-passing style, visitor patterns, and functional abstractions.

---

Conceptual Foundation

The Magic Trick: Data from Functions

Here is one of the most profound ideas in computer science:

You do not need primitive data types. Functions alone can represent any data.

This is not just a theoretical curiosity - it is a deep insight into the nature of computation. When you understand Church encodings, you understand that “data” is really just “behavior waiting to happen.”

What Is an Encoding?

An encoding is a way of representing one thing as another. We encode text as binary (ASCII, UTF-8). We encode images as pixels. We encode sound as waveforms.

Church encodings represent data as functions. But what makes a function “represent” a number? The answer: behavior.

A Church numeral does not contain a number - it behaves like a number. Specifically, the Church numeral for N is a function that applies its first argument N times to its second argument.

Church Numerals: Numbers as Iteration

The Big Idea: The number N is represented as “apply a function N times.”

0 = lambda f. lambda x. x                    -- Apply f zero times to x
1 = lambda f. lambda x. f x                  -- Apply f once to x
2 = lambda f. lambda x. f (f x)              -- Apply f twice to x
3 = lambda f. lambda x. f (f (f x))          -- Apply f three times to x
n = lambda f. lambda x. f (f (... (f x)...)) -- Apply f n times to x

Think of it this way: if you give me a function f and a starting value x, I will tell you what happens after applying f exactly N times. That IS what the number N means in this context.

Why This Works

Consider what we actually DO with numbers:

• Count iterations: “do this N times”
• Index positions: “the Nth element”
• Measure quantities: “N units”

All of these are about repeated application of an operation. Church numerals capture this essence directly.

Converting to Regular Numbers

To convert a Church numeral back to a regular integer, give it the increment function and zero:

unchurch :: Church -> Int
unchurch n = n (+1) 0

-- Example: unchurch 3
-- = 3 (+1) 0
-- = (+1) ((+1) ((+1) 0))
-- = (+1) ((+1) 1)
-- = (+1) 2
-- = 3

Converting from Regular Numbers

church :: Int -> Church
church 0 = \f x -> x
church n = \f x -> f (church (n-1) f x)

Arithmetic: Derived from Structure

The beautiful thing about Church numerals is that arithmetic operations emerge naturally from their structure.

Successor (Add One)

Adding one means “apply f one more time”:

succ n = lambda f. lambda x. f (n f x)

Given n (which applies f n times), apply f once more.

succ 2
= lambda f. lambda x. f (2 f x)
= lambda f. lambda x. f (f (f x))
= 3

Addition

Adding M and N means “apply f M+N times.” We can achieve this by applying f M times, then N more times:

add m n = lambda f. lambda x. m f (n f x)

First apply f N times (starting from x), then apply f M more times to that result.

Alternatively, observe that addition is just repeated successor:

add m n = m succ n

Apply the successor function M times to N.

Multiplication

Multiplying M and N means “apply f M*N times.” Apply f N times, and do that M times:

mult m n = lambda f. m (n f)

The function n f applies f N times. Apply that function M times.

Exponentiation

M to the power N means “multiply by M, N times”:

power m n = n m

Wait, that is suspiciously simple! But it works. The Church numeral N is “apply a function N times.” Apply the function M to get multiplication, N times.

power 2 3 = 3 2
         = 2 (2 (2 id))   -- conceptually: multiply by 2 three times
         = 8

The Predecessor Problem: Kleene’s Insight

Addition, multiplication, and exponentiation all have elegant one-line definitions. But what about subtraction?

Subtraction requires computing the predecessor (N - 1). And here is the shocking fact: predecessor is HARD.

Alonzo Church himself could not figure out how to compute the predecessor. His student Stephen Kleene discovered the solution while at the dentist (reportedly after nitrous oxide was administered, which may or may not have helped).

Why Predecessor Is Hard

With Church numerals, you can only go “forward” - apply f one more time. But to compute predecessor, you need to somehow go “backward.”

The problem: n f x applies f N times. How do you apply f only N-1 times?

Kleene’s Trick: Paired State

The insight is to carry extra information through the iteration. Instead of just tracking the current value, track a pair: (previous value, current value).

Start: (0, 0) After step 1: (0, 1) After step 2: (1, 2) After step 3: (2, 3) … After step n: (n-1, n)

At the end, extract the first element to get n-1.

pred n = lambda f. lambda x.
  fst (n (lambda p. pair (snd p) (f (snd p))) (pair x x))

Where:

• pair a b = lambda sel. sel a b (Church pair)
• fst p = p (lambda a b. a)
• snd p = p (lambda a b. b)

Step by step for pred 3:

Start: (x, x)
Step 1: (snd(x,x), f(snd(x,x))) = (x, f x)
Step 2: (snd(x,f x), f(snd(x,f x))) = (f x, f (f x))
Step 3: (snd(f x, f(f x)), f(snd(f x, f(f x)))) = (f (f x), f (f (f x)))
Result: fst = f (f x) = 2 applications = predecessor of 3

Subtraction

Once you have predecessor, subtraction is just repeated predecessor:

sub m n = n pred m

Apply predecessor N times to M.

Church Booleans: Conditionals as Selection

The Big Idea: A boolean is a choice between two options.

True selects the first option. False selects the second.

true  = lambda t. lambda f. t
false = lambda t. lambda f. f

Given two arguments, true returns the first, false returns the second.

If-Then-Else

The if function applies a boolean to the two branches:

if b then else = b then else

No need for special syntax - the boolean itself IS the conditional.

if true  "yes" "no" = true  "yes" "no" = "yes"
if false "yes" "no" = false "yes" "no" = "no"

Boolean Operations

and = lambda a. lambda b. a b false
or  = lambda a. lambda b. a true b
not = lambda b. lambda t. lambda f. b f t

Let us trace and true false:

and true false
= true false false
= false              -- true returns its first argument

And or false true:

or false true
= false true true
= true               -- false returns its second argument

Church Pairs: Structures as Closures

The Big Idea: A pair is a function that has captured two values and applies a selector to them.

pair = lambda a. lambda b. lambda sel. sel a b

A pair is “give me a selector function, and I will apply it to my two elements.”

Selectors

fst = lambda p. p (lambda a. lambda b. a)
snd = lambda p. p (lambda a. lambda b. b)

fst passes a selector that returns the first element. snd passes one that returns the second.

fst (pair 1 2)
= (pair 1 2) (lambda a b. a)
= (lambda sel. sel 1 2) (lambda a b. a)
= (lambda a b. a) 1 2
= 1

Church Lists: Recursive Data from Pairs

With pairs, we can build lists. A list is either:

• Empty (nil)
• A head followed by a tail (cons)

Encoding

nil  = lambda c. lambda n. n
cons = lambda h. lambda t. lambda c. lambda n. c h (t c n)

This is a right fold. A list [1, 2, 3] becomes:

cons 1 (cons 2 (cons 3 nil))
= lambda c n. c 1 (c 2 (c 3 n))

Given a combining function c and a nil-case n, fold the list.

List Operations

isNil = lambda l. l (lambda h. lambda t. false) true
head  = lambda l. l (lambda h. lambda t. h) ???
tail  = -- Similar trick to predecessor, requires pairs

Sum of a List

sum = lambda l. l add 0

Given add as the combiner and 0 as the base, fold the list.

sum [1, 2, 3]
= [1,2,3] add 0
= add 1 (add 2 (add 3 0))
= add 1 (add 2 3)
= add 1 5
= 6

The Y Combinator: Recursion Without Names

How do you write a recursive function when functions do not have names?

In normal programming:

factorial n = if n == 0 then 1 else n * factorial (n-1)
                                          ^^^^^^^^^
                                          Refers to itself by name

In lambda calculus, there are no names (only bound variables). How can a function call itself?

The Fixed Point Insight

A fixed point of a function f is a value x such that f(x) = x.

For recursion, we want the fixed point of a “pre-recursive” function. Consider:

preFactorial = lambda self. lambda n.
  if (isZero n) 1 (mult n (self (pred n)))

If we could find a self such that preFactorial self = self, then self would be the factorial function.

The Y Combinator

The Y combinator finds fixed points:

Y = lambda f. (lambda x. f (x x)) (lambda x. f (x x))

For any f, Y f is a fixed point of f:

Y f = (lambda x. f (x x)) (lambda x. f (x x))
    = f ((lambda x. f (x x)) (lambda x. f (x x)))
    = f (Y f)

So Y f = f (Y f). That is exactly what we need for recursion!

Factorial with Y

factorial = Y preFactorial

factorial 3
= Y preFactorial 3
= preFactorial (Y preFactorial) 3
= if (isZero 3) 1 (mult 3 ((Y preFactorial) (pred 3)))
= mult 3 (factorial 2)
= mult 3 (mult 2 (mult 1 1))
= 6

Why It Works

The Y combinator achieves self-reference through self-application. The term (lambda x. f (x x)) receives itself as an argument, so x x is the function applying itself to itself - generating unbounded recursion.

Strict Languages: The Z Combinator

In strict (eager) languages, Y diverges immediately because it tries to evaluate Y f before it’s needed. The Z combinator adds a wrapper:

Z = lambda f. (lambda x. f (lambda v. x x v)) (lambda x. f (lambda v. x x v))

The extra lambda v delays evaluation until needed.

The Philosophical Depth

Church encodings reveal something profound: data and behavior are the same thing.

A number is not “stored” - it is a pattern of application. A boolean is not a flag - it is a decision procedure. A list is not memory - it is an iterator.

This perspective is central to:

• Object-oriented programming: “ask objects to do things, don’t examine their data”
• Algebraic effects: represent actions as first-class values
• Denotational semantics: define meaning through mathematical functions

Type Issues in Haskell

Pure Church encodings have a problem in Haskell: polymorphism.

The Church numeral type is:

type Church = forall a. (a -> a) -> a -> a

This requires RankNTypes or Rank2Types. Without it, Haskell’s type inference cannot handle Church numerals directly.

Newtype Wrapper

A common solution:

newtype Church = Church { unChurch :: forall a. (a -> a) -> a -> a }

This can still cause type issues with operations. For learning purposes, using raw polymorphic types with explicit type annotations often works better.

Connection to Category Theory

Church encodings are related to initial algebras in category theory.

An F-algebra is a functor F together with a morphism F A -> A. The initial F-algebra has a unique morphism to any other F-algebra.

Natural numbers are the initial algebra for the functor F(X) = 1 + X. Lists of A are the initial algebra for F(X) = 1 + A * X.

Church encodings express these initial algebras as functions - the “fold” over the structure.

---

Project Specification

Core Requirements

Build a Haskell library implementing Church encodings, plus integration with your lambda calculus interpreter from Project 1.

1. Church Numerals Module

Implement:

• zero, one, two, … - Church numeral constants
• succ' - successor function
• church :: Int -> Church - convert from Int
• unchurch :: Church -> Int - convert to Int
• add :: Church -> Church -> Church - addition
• mult :: Church -> Church -> Church - multiplication
• power :: Church -> Church -> Church - exponentiation
• pred' :: Church -> Church - predecessor (Kleene’s trick)
• sub :: Church -> Church -> Church - subtraction
• isZero :: Church -> ChurchBool - test for zero

2. Church Booleans Module

Implement:

• true, false - Church booleans
• if' :: ChurchBool -> a -> a -> a - conditional
• and' :: ChurchBool -> ChurchBool -> ChurchBool
• or' :: ChurchBool -> ChurchBool -> ChurchBool
• not' :: ChurchBool -> ChurchBool
• toBool :: ChurchBool -> Bool - convert to Bool
• fromBool :: Bool -> ChurchBool - convert from Bool

3. Church Pairs Module

Implement:

• pair :: a -> b -> ChurchPair a b - construct pair
• fst' :: ChurchPair a b -> a - first projection
• snd' :: ChurchPair a b -> b - second projection

4. Church Lists Module

Implement:

• nil - empty list
• cons :: a -> ChurchList a -> ChurchList a - prepend
• isNil :: ChurchList a -> ChurchBool - test for empty
• head' :: ChurchList a -> a - first element
• tail' :: ChurchList a -> ChurchList a - rest of list
• foldr' :: (a -> b -> b) -> b -> ChurchList a -> b - fold
• length' :: ChurchList Church -> Church - length
• map' :: (a -> b) -> ChurchList a -> ChurchList b - map
• append :: ChurchList a -> ChurchList a -> ChurchList a - concatenate

5. Y Combinator and Recursion

Implement:

• y :: ((a -> b) -> a -> b) -> a -> b - Y combinator (or Z for strict eval)
• factorial :: Church -> Church - using Y combinator
• fibonacci :: Church -> Church - using Y combinator

6. Lambda Calculus Integration

Extend your interpreter from Project 1 to:

• Preload Church encoding definitions
• Allow :church n to show Church numeral representation
• Allow :eval expr to evaluate Church-encoded expressions

Expected Output

-- In GHCi:

> let three = church 3
> let five = church 5

> unchurch (add three five)
8

> unchurch (mult three five)
15

> unchurch (power (church 2) (church 10))
1024

> unchurch (pred' (church 7))
6

> unchurch (sub five three)
2

> toBool (isZero zero)
True

> toBool (and' true false)
False

> unchurch (fst' (pair three five))
3

> let myList = cons (church 1) (cons (church 2) (cons (church 3) nil))
> unchurch (length' myList)
3

> unchurch (foldr' add zero myList)  -- sum
6

> unchurch (factorial (church 5))
120

> unchurch (fibonacci (church 10))
55

In the lambda calculus interpreter:

Lambda> :church 3
\f. \x. f (f (f x))

Lambda> :eval (add (church 2) (church 3))
Church numeral: 5

Lambda> :let true = \t. \f. t
Lambda> :let false = \t. \f. f
Lambda> :let and = \a. \b. a b false
Lambda> and true false
\t. \f. f

---

Solution Architecture

Type Definitions

{-# LANGUAGE RankNTypes #-}

-- Church numeral: applies f to x, n times
type Church = forall a. (a -> a) -> a -> a

-- Church boolean: selects between two options
type ChurchBool = forall a. a -> a -> a

-- Church pair: holds two values, applies selector
type ChurchPair a b = forall c. (a -> b -> c) -> c

-- Church list: right fold
type ChurchList a = forall b. (a -> b -> b) -> b -> b

Module Organization

src/
  Church/
    Numeral.hs      -- Church numerals and arithmetic
    Boolean.hs      -- Church booleans
    Pair.hs         -- Church pairs
    List.hs         -- Church lists
    Combinator.hs   -- Y combinator, recursion helpers
    Integration.hs  -- Lambda interpreter extensions
  Main.hs           -- Demo / tests

Key Implementation Insights

Church Numerals - The Core Insight

-- The key: n represents "apply f n times"
zero :: Church
zero = \f x -> x

succ' :: Church -> Church
succ' n = \f x -> f (n f x)

-- Addition: apply f (m+n) times
add :: Church -> Church -> Church
add m n = \f x -> m f (n f x)
-- OR: add m n = m succ' n

-- Multiplication: apply f (m*n) times
-- Apply (n f) m times
mult :: Church -> Church -> Church
mult m n = \f -> m (n f)
-- OR: mult m n = \f x -> m (n f) x

The Predecessor Pattern

-- The hard one! Kleene's trick with pairs
pred' :: Church -> Church
pred' n = \f x ->
  fst' (n (\p -> pair (snd' p) (f (snd' p))) (pair x x))

-- Helper: pair for the predecessor trick
predPair :: ChurchPair a a -> (a -> a) -> ChurchPair a a
predPair p f = pair (snd' p) (f (snd' p))

Church Booleans - Selection as Truth

true :: ChurchBool
true = \t f -> t

false :: ChurchBool
false = \t f -> f

-- if' is trivial: apply the boolean to branches
if' :: ChurchBool -> a -> a -> a
if' b t f = b t f

-- Boolean operations
and' :: ChurchBool -> ChurchBool -> ChurchBool
and' a b = a b false

or' :: ChurchBool -> ChurchBool -> ChurchBool
or' a b = a true b

Church Lists - Right Fold Structure

nil :: ChurchList a
nil = \c n -> n

cons :: a -> ChurchList a -> ChurchList a
cons h t = \c n -> c h (t c n)

-- The list [1,2,3] is: \c n -> c 1 (c 2 (c 3 n))
-- Which is exactly a right fold!

foldr' :: (a -> b -> b) -> b -> ChurchList a -> b
foldr' f z l = l f z

Y Combinator - Self-Reference

-- The Y combinator (for lazy evaluation)
-- Y f = f (Y f)
y :: ((a -> b) -> a -> b) -> a -> b
y f = f (y f)
-- Note: In Haskell, this works due to laziness!

-- For explicit fixed points:
fix :: (a -> a) -> a
fix f = let x = f x in x

-- Factorial using Y
factorial :: Church -> Church
factorial = y factorialPre
  where
    factorialPre self n =
      if' (isZero n)
          one
          (mult n (self (pred' n)))

---

Implementation Guide

Phase 1: Church Numerals Basics (Days 1-3)

Milestone: Implement Church numerals with addition and multiplication.

1. Create Numeral.hs with Church type
2. Implement zero and succ'
3. Implement church and unchurch conversion
4. Implement add and mult
5. Test arithmetic operations

Hint Layer 1: Start without type signatures; let GHC infer types, then add RankNTypes Hint Layer 2: For add, think: “m applies f m times, n applies f n times” Hint Layer 3: mult m n f should apply f m*n times; that is, apply (n f) m times Hint Layer 4: Test: unchurch (mult (church 3) (church 4)) should be 12

Phase 2: Predecessor and Subtraction (Days 4-5)

Milestone: Implement predecessor using Kleene’s trick.

1. Implement pair, fst', snd' (you will need these)
2. Implement pred' using the pair-stepping technique
3. Implement sub as repeated predecessor
4. Test edge cases (pred of 0, sub when m < n)

Hint Layer 1: Build the pair operations first and test them independently Hint Layer 2: pred' n iterates n times, each time shifting (prev, curr) to (curr, f curr) Hint Layer 3: Start with (x, x), not (0, 0), because x is the “zero” in Church encoding context Hint Layer 4: pred' zero should equal zero (or you can leave it undefined)

Phase 3: Church Booleans (Day 6)

Milestone: Implement booleans and conditionals.

1. Create Boolean.hs with ChurchBool type
2. Implement true, false
3. Implement and', or', not'
4. Implement if' and isZero
5. Implement conversions to/from Bool

Hint Layer 1: true t f = t and false t f = f - selection is the essence Hint Layer 2: For isZero, think: what does zero do? It ignores f entirely. Hint Layer 3: isZero n = n (const false) true - if f is applied even once, return false Hint Layer 4: Be careful with types; you may need explicit annotations

Phase 4: Church Lists (Days 7-8)

Milestone: Implement lists as right folds.

1. Create List.hs with ChurchList type
2. Implement nil and cons
3. Implement foldr' (trivially)
4. Implement length', map', append
5. Implement head' and tail' (harder!)

Hint Layer 1: A list IS its fold: [1,2,3] c n = c 1 (c 2 (c 3 n)) Hint Layer 2: length' l = l (const succ') zero - count how many times c is called Hint Layer 3: tail' requires the same pair trick as predecessor Hint Layer 4: append l1 l2 = l1 cons l2 - fold l1 with cons, starting from l2

Phase 5: Y Combinator (Days 9-10)

Milestone: Implement recursion using fixed points.

1. Create Combinator.hs
2. Implement fix or y
3. Implement factorial using Y
4. Implement fibonacci using Y
5. Test recursive functions with Church numerals

Hint Layer 1: In Haskell, fix f = let x = f x in x works due to laziness Hint Layer 2: The “pre-recursive” function takes self as first argument Hint Layer 3: factorialPre self n = if n==0 then 1 else n * self (n-1) Hint Layer 4: Be careful with strictness; use seq or the Z combinator if needed

Phase 6: Integration and Polish (Days 11-14)

Milestone: Integrate with lambda interpreter, add demos.

1. Add Church definitions to interpreter prelude
2. Create evaluation mode for Church expressions
3. Build a comprehensive demo module
4. Write property-based tests
5. Add documentation

---

Testing Strategy

Unit Tests

Numeral Tests:

testChurchRoundTrip = unchurch (church n) == n  -- for n in [0..100]
testAddition = unchurch (add (church 3) (church 5)) == 8
testMultiplication = unchurch (mult (church 4) (church 7)) == 28
testPower = unchurch (power (church 2) (church 10)) == 1024
testPredecessor = unchurch (pred' (church 5)) == 4
testPredZero = unchurch (pred' zero) == 0
testSubtraction = unchurch (sub (church 10) (church 3)) == 7

Boolean Tests:

testTrue = toBool (true)
testFalse = not (toBool false)
testAnd = toBool (and' true true) && not (toBool (and' true false))
testOr = toBool (or' false true) && not (toBool (or' false false))
testNot = toBool (not' false) && not (toBool (not' true))
testIsZero = toBool (isZero zero) && not (toBool (isZero one))

List Tests:

testLength = unchurch (length' (cons one (cons two nil))) == 2
testSum = unchurch (foldr' add zero (cons one (cons two (cons three nil)))) == 6
testMap = -- map succ' over list, verify elements increased
testAppend = -- append two lists, verify combined length

Recursion Tests:

testFactorial5 = unchurch (factorial (church 5)) == 120
testFactorial0 = unchurch (factorial zero) == 1
testFibonacci10 = unchurch (fibonacci (church 10)) == 55

Property-Based Tests

-- Addition is commutative
prop_addCommutative m n =
  unchurch (add (church m) (church n)) == unchurch (add (church n) (church m))

-- Multiplication distributes over addition
prop_multDistributive a b c =
  unchurch (mult (church a) (add (church b) (church c))) ==
  unchurch (add (mult (church a) (church b)) (mult (church a) (church c)))

-- Church round-trip
prop_churchRoundTrip n = n >= 0 ==> unchurch (church n) == n

-- Predecessor-successor inverse
prop_predSucc n = n > 0 ==> unchurch (pred' (succ' (church n))) == n

-- List length
prop_consLength l = length' (cons x l) == succ' (length' l)

Integration Tests

Test with lambda interpreter:

testInterpreter = do
  result <- eval "add (church 2) (church 3)"
  unchurchResult result `shouldBe` 5

testDivergenceDetection = do
  result <- eval "(\\x. x x) (\\x. x x)"
  result `shouldBe` Diverges

---

Common Pitfalls

1. Type Errors with RankN Types

Symptom: “Cannot match type a with type b” even when code looks correct

Cause: Haskell’s type inference struggles with higher-rank types.

Fix: Add explicit type annotations or use newtype wrappers:

newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }

2. Predecessor Returns Wrong Value

Symptom: pred' (church 5) gives 5 instead of 4

Cause: The pair stepping is incorrect; often starting with wrong initial pair.

Fix: Start with (x, x), not (zero, zero). Each step: (prev, curr) -> (curr, f curr).

3. Subtraction Underflows

Symptom: sub (church 3) (church 5) gives weird results

Cause: Natural numbers do not have negative values.

Fix: Define sub m n to return 0 when n > m:

sub m n = n pred' m  -- Applying pred' to 0 returns 0

4. Y Combinator Diverges Immediately

Symptom: Using Y causes infinite loop before any useful computation

Cause: Strict evaluation of Y f = f (Y f)

Fix: Use the Z combinator or rely on Haskell’s laziness:

-- Lazy version (works in Haskell):
fix f = let x = f x in x

-- Strict version (Z combinator):
z f = (\x -> f (\v -> x x v)) (\x -> f (\v -> x x v))

5. Church Lists Missing Elements

Symptom: head' or tail' return wrong values

Cause: Incorrect understanding of list representation.

Fix: Remember: a Church list is a right fold. [1,2,3] c n = c 1 (c 2 (c 3 n)).

6. isZero Gives Wrong Results

Symptom: isZero one returns true

Cause: Incorrect implementation; not testing whether f is applied.

Fix:

isZero n = n (\_ -> false) true
-- If n > 0, f is applied at least once, returning false
-- If n = 0, f is never applied, returning true

---

Extensions and Challenges

Extension 1: Church Numerals for Integers

Extend Church numerals to handle negative numbers using pairs:

integer (sign, magnitude) where sign is a Church boolean

Implement addition, subtraction, and multiplication for integers.

Extension 2: Scott Encodings

Implement Scott encodings as an alternative to Church encodings:

zero = lambda z. lambda s. z
succ n = lambda z. lambda s. s n

Compare expressiveness and efficiency with Church encodings.

Extension 3: Continuation-Passing Style

Convert Church operations to continuation-passing style and back. Understand the connection between CPS and Church encodings.

Extension 4: Peano Axioms Verification

Prove (informally or formally) that Church numerals satisfy the Peano axioms:

1. 0 is a natural number
2. For every natural n, S(n) is a natural number
3. S(n) != 0 for all n
4. S(m) = S(n) implies m = n
5. Induction principle

Extension 5: Division and Modulo

Implement division and modulo for Church numerals. This requires recursion (Y combinator) and comparison operations.

Extension 6: Binary Representations

Implement a more efficient binary representation of numbers using Church encodings. Compare performance with standard Church numerals.

---

Real-World Connections

Continuation-Passing Style

Church encodings are closely related to CPS, which is used in:

• Compiler intermediate representations: Many compilers transform code to CPS
• Async programming: Callbacks are continuations
• Control flow: Call/cc in Scheme

Visitor Pattern

The Church encoding of a data type is essentially the visitor pattern:

interface List<T> {
  <R> R accept(ListVisitor<T, R> visitor);
}

interface ListVisitor<T, R> {
  R visitNil();
  R visitCons(T head, R tailResult);
}

This IS a Church list.

Fold/Reduce in Functional Programming

Church lists reveal why foldr is the fundamental list operation:

-- A Church list IS its foldr
churchList :: ChurchList a -> (a -> b -> b) -> b -> b
churchList l = l

Every other list operation can be expressed via fold.

Free Monads and Interpreters

Church encodings connect to free monads, which represent programs as data:

• The encoding captures “what operations are available”
• The evaluator provides “how to execute them”

Type Theory and Dependent Types

Church encodings extend to dependent type theory:

• Dependent Church numerals: forall (P : Nat -> Type), P 0 -> (forall n, P n -> P (S n)) -> forall n, P n
• This is the induction principle for natural numbers

---

Interview Questions

After completing this project, you should be able to answer:

1. What is a Church numeral, and how does it represent the number 5?

2. Why is the predecessor function harder to implement than successor for Church numerals? Explain Kleene’s trick.

3. How do Church booleans implement conditional logic without if-statements?

4. What is the Y combinator, and why is it needed for recursion in lambda calculus?

5. Explain the connection between Church-encoded lists and the foldr function.

6. What are the type challenges when implementing Church encodings in Haskell? How do you work around them?

7. How does the visitor pattern relate to Church encodings?

---

Self-Assessment Checklist

You have mastered this project when you can:

• Write Church numeral definitions from memory
• Perform arithmetic (add, mult, power) mentally on small Church numerals
• Implement predecessor step-by-step, explaining why each part is necessary
• Write Church booleans and boolean operations without references
• Construct a Church list from regular values and verify it works
• Explain the Y combinator’s mechanism and write a recursive function using it
• Translate between Church encodings and regular Haskell values fluently
• Identify Church encoding patterns in other contexts (visitor pattern, CPS)
• Debug type errors related to RankN types
• Extend Church encodings to new data types independently

---

Resources

Primary References

Resource	Use For	Specific Chapters
“Types and Programming Languages” by Pierce	Church encodings, Y combinator	Chapter 5
“Learn You a Haskell” by Lipovaca	Higher-order functions in Haskell	Chapters 5-6
“Lambda Calculus and Combinators” by Hindley & Seldin	Comprehensive encoding theory	Chapters 2-4

Papers and Tutorials

Resource	Description
A Tutorial Introduction to the Lambda Calculus	Church encodings section
Programming with Lambda Calculus	Interactive Y combinator tutorial
Learn X in Y Minutes - Lambda Calculus	Quick reference

Online Tools

Tool	Use For
Lambda Calculator	Test Church encodings
Lambda Viewer	Visualize Church numeral reductions

Videos

Video	Platform
“Y Combinator in JavaScript” by Computerphile	YouTube
“Lambda Calculus” playlist by NICTA	YouTube
“Church Encodings” by Bartosz Milewski	YouTube

---

“The lambda calculus… shows that the concept of number emerges naturally from the concept of function.” - Alonzo Church