 # [Lambda Calculus via C# series]

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.