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

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:

1
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.

1
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.

1
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:

1
Item1 (CreateTuple x y)
2
≡ Item1 (λf.f x y)
3
≡ (λt.t (λx.λy.x)) (λf.f x y)
4
≡ (λf.f x y) (λx.λy.x)
5
≡ (λx.λy.x) x y
6
≡ (λy.x) y
7
≡ x

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

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

And just like Item1:

1
Item2 (CreateTuple x y)
2
≡ Item2 (λf.f x y)
3
≡ (λt.t (λx.λy.y)) (λf.f x y)
4
≡ (λf.f x y) (λx.λy.y)
5
≡ (λx.λy.y) x y
6
≡ (λy.y) y
7
≡ y

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

1
// Tuple = f => f(item1)(item1)
2
public delegate object Tuple<out T1, out T2>(Func<T1, Func<T2, object>> f);
3
// Tuple is an alias of Func<Func<T1, Func<T2, object>>, object>
4

5
public static class ChurchTuple
6
{
7
    // CreateTuple = item1 => item2 => f => f(item1)(item2)
8
    public static Func<T2, Tuple<T1, T2>> Create<T1, T2>
9
        (T1 item1) => item2 => f => f(item1)(item2);
10

11
    // Item1 => tuple => tuple(x => y => x)
12
    public static T1 Item1<T1, T2>
13
        (this Tuple<T1, T2> tuple) => (T1)tuple(x => y => x);
14

15
    // Item2 => tuple => tuple(x => y => y)
16
    public static T2 Item2<T1, T2>
17
        (this Tuple<T1, T2> tuple) => (T2)tuple(x => y => y);
18
}

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:

1
Item1 := λt.t (λx.λy.x)
2
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:

1
Item1 := λt.t True
2
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.

1
// Curried from: object Boolean(TTrue @true, TFalse @TFalse)
2
public delegate Func<TFalse, object> Boolean<in TTrue, in TFalse>(TTrue @true);
3
// Boolean is alias of Func<TTrue, Func<TFalse, object>>
4

5
public static partial class ChurchBoolean
6
{
7
    // True = @true => @false => @true
8
    public static Func<TFalse, object> True<TTrue, TFalse>
9
        (TTrue @true) => @false => @true;
10

11
    // False = @true => @false => @false
12
    public static Func<TFalse, object> False<TTrue, TFalse>
13
        (TTrue @true) => @false => @false;
14
}

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

1
public delegate object Tuple<out T1, out T2>(Boolean<T1, T2> f);
2

3
public static partial class ChurchTuple
4
{
5
    // CreateTuple = item1 => item2 => f => f(item1)(item2)
6
    public static Func<T2, Tuple<T1, T2>> Create<T1, T2>
7
        (T1 item1) => item2 => f => f(item1)(item2);
8

9
    // Item1 = tuple => tuple(x => y => x)
10
    public static T1 Item1<T1, T2>
11
        (this Tuple<T1, T2> tuple) => (T1)tuple(ChurchBoolean.True<T1, T2>);
12

13
    // Item2 = tuple => tuple(x => y => y)
14
    public static T2 Item2<T1, T2>
15
        (this Tuple<T1, T2> tuple) => (T2)tuple(ChurchBoolean.False<T1, T2>);
16
}

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:

1
public static partial class ChurchBoolean
2
{
3
    // And = a => b => a(b)(False)
4
    public static Boolean<TTrue, TFalse> And<TTrue, TFalse>
5
        (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> a, Boolean<TTrue, TFalse> b) =>
6
            (Boolean<TTrue, TFalse>)a(b)(False<TTrue, TFalse>);
7

8
    // Or = a => b => a(True)(b)
9
    public static Boolean<TTrue, TFalse> Or<TTrue, TFalse>
10
        (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> a, Boolean<TTrue, TFalse> b) =>
11
            (Boolean<TTrue, TFalse>)a(True<TTrue, TFalse>)(b);
12

13
    // Not = boolean => boolean(False)(True)
14
    public static Boolean<TTrue, TFalse> Not<TTrue, TFalse>
15
        (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> boolean) =>
16
            (Boolean<TTrue, TFalse>)boolean(False<TTrue, TFalse>)(True<TTrue, TFalse>);
17

18
    // Xor = a => b => a(b(False)(True))(b(True)(False))
19
    public static Boolean<TTrue, TFalse> Xor<TTrue, TFalse>
20
        (this Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> a, Boolean<Boolean<TTrue, TFalse>, Boolean<TTrue, TFalse>> b) =>
21
            (Boolean<TTrue, TFalse>)a((Boolean<TTrue, TFalse>)b(False<TTrue, TFalse>)(True<TTrue, TFalse>))((Boolean<TTrue, TFalse>)b(True<TTrue, TFalse>)(False<TTrue, TFalse>));
22
}

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:

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

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

1
// Swap = tuple => Create(tuple.Item2())(tuple.Item1())
2
public static Tuple<T2, T1> Swap<T1, T2>
3
    (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:

1
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:

1
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:

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

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

1
ChurchTuple._Create(1, "a");

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

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

https://dixin.github.io/posts/lambda-calculus-via-c-sharp-13-encoding-church-pairs-2-tuples-and-generic-church-booleans/

Author

Dixin

Published at

2018-11-13

License

CC BY-NC-SA 4.0

Lambda Calculus via C# (14) Church Pair (2-Tuple) and Church Numeral Decrease

Lambda Calculus via C# (12) Church Numeral Comparison Operators

1

[LINQ via C# series]

2

[Lambda Calculus via C# series]

3

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

4

Church pair (2-tuple)

5

Generic Church Booleans

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

6

Currying and type inference