What to do with half-finished "CL 101"?

Remember when I announced a "101" on Combinatory Logic in https://github.com/busterjs/buster/issues/339 ([1] here)?

I have a draft lying around half-finished which I wasn't pleased with because it's already quite lengthy. I found myself striking out ever farther... and just stopped at some point. But then I thought it'd be a pity if it were just thrown away.

We do have a bit of confusion of terms re combinators: what are the things that are being combined vs those that do the combining (the real combinators in my view)? So that was the main motivation to write it. Not sure if it's helpful though, or rather creates more confusion...

Anyways, don't wanna just throw it away. So at least it's here. Perhaps put it into git, docs/ or so?

Here's what I got, with a lot of "TODO"s:

λ & CL 101

Intro

"Lambda calculus" - at least as a term or name - is probably known to everyone, and so is Alonzo Church, who devised the thing in 1930. Not so well-known is, on the other hand, "Combinatory Logic" (CL) which was invented in 1920, by a Ukrainian named Moses Schönfinkel. It turned out later that both systems have precisely the same power of expressiveness. Schönfinkel, however, didn't publish a lot^[1] and died in 1942. It took another American to re-invent combinators in 1927 (who had not seen Schönfinkel's paper then): Haskell Curry. You definitely have heard of "Haskell" and most probably you know what "currying"^[2] is, don't you?

λ syntax

The syntax of the lambda calculus ("λ calculus" or even just "λ" for short) is nothing but an extremely compact way of writing down functions. It's even so compact that no function ever gets a name, pretty much like anonymous function expressions in JS. So eg. function (x) { return x; } (the identity function) would translate to λ as \x.x. Formally, there are only three basic entities in λ's syntax:

λ or alternatively \ (for I don't know how to get λ inside backticks here)
variables^[3], for which we'll use lower-case latin letters a, b, c, ..., x, y, z
the dot .

That's it :) Well ok, the basic entities as such are not what really makes up the language of λ. Rather, a formal language - such as λ - is nothing but a set, and the elements are called terms. These, in turn, are composed of the basic entities. For λ it goes like this:

atoms: every variable is a term
application: if X and Y^[4] are terms, then so is (X Y). Think of it as "call function X with argument Y" or "apply function X to argument Y". We shall adopt the convention of left-associativity for this in order to save some parentheses. For instance: X Y Z abbreviates ((X Y) Z) - as opposed to (X (Y Z)).
abstraction: if X is a variable (NOT an arbitrary term!) and Y is any term, then so is \X.Y. This is the facility to build functions, as seen before with \x.x.

Examples: neither \ alone nor \x are valid λ terms, whereas x alone or x x or \x.x are.

We can (and will) of course use abbreviations in order to reduce clutter. For example we might say I ≡ \x.x once and for all, and thereafter only use the one character I in place of the previous four. We'll reserve upper-case latin letters for such abbreviations^[5].

[TODO: I in JS]

Currying

Abstraction from above only gives rise to unary (one-argument) functions, so what about binary (2-arg), ternary (3-arg), ...? Well, due to the magic of "currying"/"schönfinkeling" \x y.T (binary) can be viewed as a mere abbreviation for \x.(\y.T), and similarly \x y z.T (ternary) for \x.(\y.(\z.T)), and so on... Why that is safe (ie always works) is beyond scope here - but it does. Really :)

[TODO: no variadic fns in lambda, not a good idea to mix currying and variadic fns]

Scope and free vs bound variables

[TODO: define "scope", "binding" and "bound"]

In lambda, a combinator is simply a closed term (one where all variables are bound). The "postpone-the-actual" operation that defert

[TODO: no such thing as `defert` anymore!]

does^[1] is such a combinator: \x y z.x z y where \ stands for the greek letter lambda λ. It is known as the combinator C. In JS it is

function defert (assertion expected) {
    return function (actual) {
        return assertion.apply(null, actual, expected);
    };
}

and in Haskell it would read

defert :: (a -> e -> Bool) -> e -> (a -> Bool)
defert assertion expected = \actual -> assertion actual expected

(the parens around a -> Bool in the type decl aren't necessary) Note that I chose the type Bool instead of a type variable, in order to emphasize the decision-making character of an assertion. Such a (systematic) specialization is not possible in JS, nor in pure λ.

[TODO: Scala example]

Some more combinators with standard names:

I ≡ \x.x identity
K ≡ \x y.x which makes constant unary functions, e.g. K x produces the function that always yields x, no matter what y you apply it to.
B ≡ \f g x.f (g x) which is function composition. Note the difference to C - it's due to the parentheses.
S ≡ \f g x.f x (g x), a "stronger" composition
CL syntax

Now, in CL you have nothing but combinators! And yet it is equivalent to lambda calculus.

[TODO: rephrase]

Of course we can't use λ (nor .) for definitions since it's simply not part of the language. Rather it goes like this:

S, K and I are CL terms
if x and y are CL terms then so is (x y) (adopting the usual convention of left-associativity enables us to omit a good deal of parentheses)

...and that's all for the syntax of CL.

busterjs / referee-combinators