Emulate Church encoding?

[71104]

Church-encoded booleans are:

• true ≡ λ x, y . x
• false ≡ λ x, y . y

At type-checking, the bool type can be retained and made a subtype of those lambdas, i.e.:

bool ≤ ∀ α . α → (α → α)

At evaluation, BooleanValue can be made a subclass of Closure.

[71104]

It gets more complicated with natural numbers because the natural type would become a subtype of both integer and the Church-encoded lambdas. The order relationship on types is partial, so there is no problem in doing this from a mathematical standpoint; but the JavaScript implementation needs attention.

Church encoding for natural numbers:

• 0 ≡ λ x, y . y
• 1 ≡ λ x, y . x y
• 2 ≡ λ x, y . x (x y)
• 3 ≡ λ x, y . x (x (x y))
• …

Typing:

natural ≤ integer
natural ≤ ∀ α . (α → α) → (α → α)

[71104]

With proper definitions of operators, this might allow to drop the Polish notation.

For example, with a proper definition of +, this feature might allow for:

2 + 3

which would actually yield 5. This could also be done for booleans, but the implementation for real and complex numbers would be a problem because there is no Church encoding for them.

Optimizing this would be a completely different story, but it could also provide a way to fix it for real and complex numbers.

The only problem with this view is that standard operator precedence would not be respected because left associativity of application would still hold, i.e.:

1 + 2 * 3

would be resolved as:

(((1 +) 2) *) 3

and it would yield 9 instead of 7.

[71104]

Also, the idea doesn't cover unary operators.

The not operator doesn't actually need any change. The unary - operator would still need to be written as a binary operation between 0 and another number, i.e. 0 - 5 instead of -5.

[71104]

If this infix notation is implemented, it would be a good idea to introduce explicit operator types (as subtypes of appropriate lambdas) to improve the typing of operations so that numbers can be applied to operators only instead of any suitable lambda.

[71104]

Nice side effect: partial applications still yield functions that operate on the second operand.

That is:

• old style: + 2 yields a function that adds 2 to whatever argument;
• new style: 2 + yields the same.

Nice example use case: doubling all the numbers in an array.

Old style: {1, 2, 3, 4, 5}.map (* 2).

New style: {1, 2, 3, 4, 5}.map (2 *).

Unfortunately neither style works well with non-commutative operations. Example use case: squaring all the numbers in an array; both styles have to explicit a lambda:

• old style: {1, 2, 3, 4, 5}.map fn x -> ** x 2;
• new style: {1, 2, 3, 4, 5}.map fn x -> x ** 2.

[71104]

The new style actually opens new possibilities to satisfy the latter use case (squaring all the numbers of an array or otherwise apply a non-commutative operator).

Operators can be defined such that when applied to the right-hand operand they return something that the left-hand operand can be applied to, to return the final value.

That is:

• 3 ** returns a function that raises 3 to the specified power;
• ** 2 returns a function that squares the specified argument;
• 3 ** 2 equals (3 **) 2 and returns 3 to the power of 2, i.e. 9.

What 3 (** 2) returns can be easily inferred. Given that:

• 3 ≡ λ x, y . x (x (x y))
• ** 2 ≡ function that squares the argument

3 (** 2) must return a function that squares the argument 3 times. That is, 3 (** 2) raises the argument to the power of 8.

In this way the use case of squaring all numbers in an array becomes as nice as the other cases with commutative operations:

{1, 2, 3, 4, 5}.map (** 2)

[71104]

The design of the infix notation turns out to be incompatible with the Church encoding.

Given 3 ≡ λ x, y . x (x (x y)), in order to achieve 3 + 2 = 5, + must be a function that, when applied 3 times to 2, yields 5. So + must be the successor function, also known as succ. The successor function applied to any natural number n returns n+1.

We have:

3 + 2 =
(3 +) 2 =
(3 succ) 2 =
succ (succ (succ 2)) = 5

This works well with any pair of operands, but it's incompatible with the above design of + 2 returning a function that adds 2. If + is the successor function, + 2 simply returns 3.

There are other incompatibilities, the sum operation seems to be the one that works best. We need to choose between implementing Church encoding and keeping the Polish notation or implementing the infix notation and dropping Church encoding.

[71104]

Pros of Church encoding:

• Very standard in the academic community.
• There are standard definitions for booleans, naturals, and tuples/lists. The latter can be extended to arrays and strings. Complex numbers can also be encoded as pairs.

Cons:

• Nobody in the industry knows it.
• Incompatible with infix notation.
• It lacks a definition for integer numbers and floating point numbers.
  • Real numbers can actually be Church-encoded but the resulting strategy is incompatible (or very difficult to be made compatible) with floating point arithmetic implemented by most of today's machines. Since we want to exploit floating point arithmetic implemented in the hardware, we won't encode reals like that.

[71104]

Given that the cons outweigh the pros, Church encoding will be dropped in favor of #92.