# Alternative encodings

There are 3 well-known approaches for data representation in the pure λ-calculus (without complex extensions such as ADTs), viz. the Church, Scott and Parigot encoding.

## Church Encoding

The Church Encoding represents data structures as folds. For example, the natural number 3 is represented via the function obtained from folding the successor tree times onto a zero function:

```
zero = \a b -> b
succ = \n f x -> f (n f x)

-- by successive appl. of succ to zero we get ℕ
c1 = \s z -> s z
c2 = \s z -> s (s z)
c3 = \s z -> s (s (s z))
```

The Church Encoding embeds iteration and it is typeable in System F, which mean it can be used in a total language. Algorithms on Church-encoded data are *strongly normalizing*; writing a folding function for Nat type is trivial, but its major issue is that the pattern matching takes linear time, and so does the predecessor function, which isn't trivial to write (has several version).

```
-- not recursive (good)
foldNat = \s z n -> n s z

-- one of pred variants, O(n). Also, WTF.
pred = \n (\g h -> (h (g succ))) (const zero) id
```

## Scott Encoding

`O(N)` pred is considered bad, and solved by the Scott Encoding, which represents data structures as their pattern-match. Here is 3 again:

```
0 s0 = (f x -> x)
1 s1 = (f x -> (f (f x -> x)))
2 s2 = (f x -> (f (f x -> (f (f x -> x)))))
3 s3 = (f x -> (f (f x -> (f (f x -> (f (f x -> x)))))))
```

With this representation, we get constant-time pattern-matching, but we need general recursion to implement foldr. That means we can't implement `foldNat` in a total language, and no implementation of `foldNat` for Scott-encoded structures has a beta normal form.

```
-- O(1). Good.
pred    = (nat -> (nat (pred -> pred) _))

-- Recursive. Also, WTF.
foldNat = (s z nat -> (nat (pred -> (s (foldNat s z pred))) z))
```

## Parigot Encoding

To solve even this issue, the Parigot encoding is sometimes used. It works like a combination of the Church and Scott encodings:

```
0 p0 = (f x -> x)
1 p1 = (f x -> (f (f x -> (f x)) (f x -> x)))
2 p2 = (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))
3 p3 = (f x -> (f (f x -> (f (f (f x)))) (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))))
```

We can make it easier to read using church-number literals:

```
0 p0 = (f x -> x)
1 p1 = (f x -> (f c1 (f x -> x)))
2 p2 = (f x -> (f c2 (f c -> (f c1 (f x -> x)))))
3 p3 = (f x -> (f c3 (f x -> (f c2 (f x -> (f c1 (f x -> x)))))))
```

This allows us to see that it is just the Scott encoding with Church-numbers stored inbetween - or, if you prefer, a Scott-encoded list of Church-encoded naturals. This allows us to get `pred` in constant time (just take the tail of the list), and `foldr` without recursion (just take the head of the list).

```
-- O(1). Good.
pred    = (nat -> (nat (_ pred -> pred) _))

-- Non-recursive. Good.
foldNat = (nat -> (nat (fold _ -> fold) _))
```

But the Parigot Encoding has its own problem: terms take quadratic amount of space.

## Alternative Encoding

There is another encoding which combines all good properties from the previous, but I've never seen on literature. This is it:

```
0 a0 = (f x -> x)
1 a1 = (f x -> (f (c -> (c f x)) (f x -> x)))
2 a2 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))
3 a3 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))))
```

Like Parigot encoding, this uses a Scott-list. Instead of Church-numbers, we store continuators, `(c -> (c f x))`. Each continuator gives us fuel to fold to the next pred - all the way to zero, where there isn't fuel anymore, so the term has to halt. Pred is still just tail `(O(1))`, and there is a non-recursive implementation of foldNat with a beta normal form.

```
-- Non-recursive. Good.
foldNat = (s z nat -> (nat (cont pred -> (s (cont pred))) z))

-- O(1). Good.
pred    = (nat -> (nat (_ pred -> pred) _))
```

It can easily be extended to arbitrary data-types and, differently from the Parigot encoding, terms take linear space. That looks like a decent solution. (Was this proposed? Is there any merit on that kind of encoding?)


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus-encodings/encodings/encoding-alternatives.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.