Practical application of SKI calculus and BCKW

I can understand how to create and think about the SKI and BCKW calculus, but I am never able to find practical uses.开发者_运维问答 Maybe I am not looking deeply enough? That is, I wonder if (an example only please, I am not implying this is true) Java Servlets use S extensively and Python generators are an example of BCW and I am just unable to see through the forest of trees?

In Haskell, they're everywhere!

• B is <$>
• C is flip
• K is pure
• I is id
• S is <*>
• W is join

From a Haskell point of view, <$> means "do in a context".

• (+2) <$> (*3) means add two after multiplying by three.
• (+2) <$> [1,2,3] means add two to each element in the list.
• (+2) <$> (read . getLine) means add two to the number I just read.
• (+2) <$> someParser means add two to the number I just parsed.

Things that have a context are called functors. All your Java/Python/C++ iterators are just weird inside-out versions of functors.

Another connection: the S and K combinator together are Turing-complete. In Haskell, pure and <*> together form an applicative functor.

Of course, understanding how the other combinators fit in will require learning Haskell. But this example shows how combinators are so entrenched in the language.

Although lambda and SKI calculus don't reflect the input and output systems of most programming languages (such as graphics, network connections, or arguably even standard input and output), the way practical computer programming is structured corresponds to Lambda (and therefore SKI and BCKW), such as the idea of recursion and somewhat the way functions are called. A lot of these programming languages have lambda abstractions for use as functions.

It's all about control.

Maybe start at a lower level. An applicative system is just a system where objects can be applied to other objects. A simple example of an applicative system is bash. ls | more One might suppose they are in some environment, and that the above means do ls on the environment, then do more. In applicative notation this is more @ (ls @ environment) However, one could do more complicated things like ls | grep pattern | more So now in applicative notation this is more @ ( (grep @ pattern) @ (ls @ environment)). Notice grep @ pattern. Grep is applied to a pattern, which give back the program to match that pattern in the result of ls. This is the point of application, to apply a program to arguments, building up new programs from "atomic" (aka builtin) programs. However, we can't do too much programming with just the primitive application or builtins. We need a way to structure our input and the application of our primitives to our input.

This is where lambda comes in. Using lambda one can generalize the (grep @ pattern) To applying grep to any input, (grep @ X) However, we must have a way to get the input to grep. Thus we usually use functions. f(X) = grep @ X The above process is called abstracting out the argument. But there is no reason to think of the name f as being special, so we have a syntax for it: lambda X . grep @ X Then lambda X. grep @ X, can be applied to an input, and the input will be substituted into the body and evaluated. However, substituting can get messy, bound variables can be troublesome to implement on a machine. S-K-I (or B,C,K,W) gives a way to do lambda stuff without substitution, and instead just swapping around applications.

To recap, application is what it's all about. It is very convenient to reason at the level of applying a program to something (possibly another program). Lambda calculus gives a way to structure the input and application of programs to arguments. SKI gives a way to do lambda without having to explicitly substitute.

One should note that SKI reduction is inherently lazy, so some consideration may need to be made in a real world use of SKI to structure application. Indeed, the arguments might now have been fully evaluated, and may be a partial application as well. One can get around this with a type theory, and only evaluating a program on its input if the program is in the head position of the application. I.e., if one writes with closed lambda terms, translated to SKI, then if p @ arg1 @ .... It should be the case that if p is a primitive program, then the rewriting has completed, and so all it's arguments are 1) available, 2) fully evaluated. However, I haven't proved this, and it might not be true with a strong enough type theory...

The SKI and BCKW calculi stand apart from the Lambda calculus (which has well-known applications in functional programming concept) because they are in point-free form. See also tacit programming. They form the basis of understanding how to construct functional programs without named arguments.

We see applications of it in certain languages (e.g. Joy and Cat). I once posted on Lambda-the-Ultimate.org about the relationship of SK calculus to Cat and Joy.

For what its worth: BCKW and SKI (or SK) calculi are virtually identical, but the BCKW basis has fallen out of vogue.