# Lambda Calculus via C# (13) Encoding Church Pairs (2-Tuples) and Generic Church Booleans

# [LINQ via C# series]

# [Lambda Calculus via C# series]

**Latest version: https://weblogs.asp.net/dixin/lambda-calculus-via-csharp-4-tuple-and-signed-numeral**

Church pair is the Church encoding of the pair type, aka 2-tuple. Unlike the Tuple<T1, T2> class in .NET, in lambda calculus Church pair will be represented by lambda expression. To avoid 2 naming systems, here in all the code, Church pair will be called tuple.

# Church pair (2-tuple)

A Church pair can be constructed with 2 values x y:

`CreateTuple := λx.λy.λf.f x y`

And it return a tuple - another lambda expression (λf.f x y). So tuple is a higher order function that takes a function and apply it with x and y.

`Tuple := λf.f x y`

Notice:

- tuple is a closure of x and y
- f is supposed to be in the format of λx.λy.E

So, to get the first item x, a f like λx.λy.x can be applied to a tuple.

`Item1 := λt.t (λx.λy.x)`

Item1 takes a tuple as parameter, applies it with a (λx.λy.x), and returns the first item x. This is how Item1 works:

```
Item1 (CreateTuple x y)
≡ Item1 (λf.f x y)
≡ (λt.t (λx.λy.x)) (λf.f x y)
≡ (λf.f x y) (λx.λy.x)
≡ (λx.λy.x) x y
≡ (λy.x) y
≡ x
```

So to get the second item y, a tuple can be applied with a f of λx.λy.y:

```
Item2 := λt.t (λx.λy.y)
```

And just like Item1:

```
Item2 (CreateTuple x y)
≡ Item2 (λf.f x y)
≡ (λt.t (λx.λy.y)) (λf.f x y)
≡ (λf.f x y) (λx.λy.y)
≡ (λx.λy.y) x y
≡ (λy.y) y
≡ y
```

Based on above definitions, here is the C# implementation:

// Tuple = f => f(item1)(item1) public delegate object Tuple<out T1, out T2>(Func<T1, Func<T2, object>> f); // Tuple is an alias of Func<Func<T1, Func<T2, object>>, object> public static class ChurchTuple { // CreateTuple = item1 => item2 => f => f(item1)(item2) public static Func<T2, Tuple<T1, T2>> Create<T1, T2> (T1 item1) => item2 => f => f(item1)(item2); // Item1 => tuple => tuple(x => y => x) public static T1 Item1<T1, T2> (this Tuple<T1, T2> tuple) => (T1)tuple(x => y => x); // Item2 => tuple => tuple(x => y => y) public static T2 Item2<T1, T2> (this Tuple<T1, T2> tuple) => (T2)tuple(x => y => y); }

Tuple’s Item1 is of type T1, Item2 is of type T2. And, f is λx.λy.E, so its type is Func<T1, Func<T2, object>>. Again, just like the object in Church Boolean Func<object, Func<object, object>>, object here does not mean System.Object is introduced. It just mean λx.λy.E can return any type. For example:

- in function Item1, f is λx.λy.x or x => y => x, so f returns a T1
- in function Item2, f is λx.λy.y or x => y => y, so f returns a T2

# Generic Church Booleans

If observing above definition:

```
Item1 := λt.t (λx.λy.x)
Item2 := λt.t (λx.λy.y)
```

In Item1 f is actually True, and in Item2 f becomes False. So above definition can be simplified to:

```
Item1 := λt.t True
Item2 := λt.t False
```

In C# more work need to be done for this substitution. As fore mentioned, f is Func<T1, Func<T2, object>> but currently implemented Church Boolean is Func<object, Func<object, object>>. So a more specific Church Boolean is needed.

// Curried from: object Boolean(TTrue @true, TFalse @TFalse) public delegate Func<TFalse, object> Boolean<in TTrue, in TFalse>(TTrue @true); // Boolean is alias of Func<TTrue, Func<TFalse, object>> public static partial class ChurchBoolean { // True = @true => @false => @true public static Func<TFalse, object> True<TTrue, TFalse> (TTrue @true) => @false => @true; // False = @true => @false => @false public static Func<TFalse, object> False<TTrue, TFalse> (TTrue @true) => @false => @false; }

With this generic version of Church Booleans, above Church tuple can be re-implemented:

public delegate object Tuple<out T1, out T2>(Boolean<T1, T2> f); public static partial class ChurchTuple { // CreateTuple = item1 => item2 => f => f(item1)(item2) public static Func<T2, Tuple<T1, T2>> Create<T1, T2> (T1 item1) => item2 => f => f(item1)(item2); // Item1 = tuple => tuple(x => y => x) public static T1 Item1<T1, T2> (this Tuple<T1, T2> tuple) => (T1)tuple(ChurchBoolean.True<T1, T2>); // Item2 = tuple => tuple(x => y => y) public static T2 Item2<T1, T2> (this Tuple<T1, T2> tuple) => (T2)tuple(ChurchBoolean.False<T1, T2>); }

## Back to Church Boolean - why not using generic Church Booleans from the beginning?

If the Boolean logic is implemented with this generic version of Church Booleans, then:

public static partial class ChurchBoolean { // And = a => b => a(b)(False) public static Boolean<TTrue, TFalse> And<TTrue, TFalse> (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> a, Boolean<TTrue, TFalse> b) => (Boolean<TTrue, TFalse>)a(b)(False<TTrue, TFalse>); // Or = a => b => a(True)(b) public static Boolean<TTrue, TFalse> Or<TTrue, TFalse> (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> a, Boolean<TTrue, TFalse> b) => (Boolean<TTrue, TFalse>)a(True<TTrue, TFalse>)(b); // Not = boolean => boolean(False)(True) public static Boolean<TTrue, TFalse> Not<TTrue, TFalse> (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> boolean) => (Boolean<TTrue, TFalse>)boolean(False<TTrue, TFalse>)(True<TTrue, TFalse>); // Xor = a => b => a(b(False)(True))(b(True)(False)) public static Boolean<TTrue, TFalse> Xor<TTrue, TFalse> (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> a, Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> b) => (Boolean<TTrue, TFalse>)a((Boolean<TTrue, TFalse>)b(False<TTrue, TFalse>)(True<TTrue, TFalse>))((Boolean<TTrue, TFalse>)b(True<TTrue, TFalse>)(False<TTrue, TFalse>)); }

The type parameter becomes too noisy. It is difficult to read or use these functions.

# Currying and type inference

The part of currying mentioned currying may cause some noise for type inference in C#. Here is an example:

`Swap = λt.CreateTuple (Item2 t) (Item1 t)`

C# logic is simple, but the type information has to be given so it is noisy:

// Swap = tuple => Create(tuple.Item2())(tuple.Item1()) public static Tuple<T2, T1> Swap<T1, T2> (this Tuple<T1, T2> tuple) => Create<T2, T1>(tuple.Item2())(tuple.Item1());

When invoking the curried Create function, the type arguments cannot be omitted. This is signature of Create:

Func<T2, Tuple<T1,T2>> Create<T1,T2>(T1 item1)

After currying, T2’s appearances are all relocated to Create’s returned type. So during the 2 applications of Create(item1)(item2), C# compiler does not even know how to compile first application Create(item1). It cannot infer what return type is wanted. The application code will always end up as:

ChurchTuple.Create<int, string>(1)("a");

So, only for convenience of C# coding and less noise for readability, this uncurried helper method can be created:

public static Tuple<T1, T2> _Create<T1, T2> (T1 item1, T2 item2) => Create<T1, T2>(item1)(item2);

Now T2 is relocated back to parameter, so type arguments are not mandatory:

ChurchTuple._Create(1, "a");

Much less noise. _Create is also tagged with underscore since its uncurrying is for adapting C# type inference feature.