Why S and K are enough.
The word “implies” and corresponding arrows are grossly overloaded and have more than one subtle but distinct meanings.
We will read and interpret the “arrows” (and the word “implies”) from different formalisms differently (as an implication in terms of necessity and sufficiency and as a single discrete step of causality).
We will put the universal notion of an environment (and the corresponding Γ abstraction) from obscurity to the center.
We will threat “arrows” as paths of a /single step, and composition of functions (via nesting) as composition of arrows, or steps in longer paths (of causality).
The notion of currying corresponds to joins (when multiple arrows come together).
The notion of abstraction by parameterization (B. Liskov) is implicit in the notion of currying. We (and molecular biology) parameterize with whole discrete steps (arrows).
So, the world “implies” and the notion of an arrow is convoluted and overloaded, which causes a mess and a profound confusion. Once we sort the arrows out everything will “click”.
Indeed, stating what causes what (necessary and sufficient for a “reaction” or a “transition”) in general is subtly different from describing (stating) individual steps of causality, at least for us - programmers, who are concerned with representations and implementations.
The “arrows” looks (are) the same in various related formalisms - different perspectives (views) of the same reality (mountain). They are trying to capture (aspects of) the same universal notions, after all.
Some arrows out there are due to currying, which is implemented as (is) nesting and thus having an implicit particular ordering “under the hood”.
Causality (the processes) are ordered, of course. The previous “results” or “stable intermediate forms” (including what is necessary and sufficient) has to be already present “out there” in the environment – in Γ or in the same locality.
Composition as nesting captures another universal notion of a partitioned compartment - of a closure - of an enzyme or a whole cell.
Closure is a more general notion, which includes a statement of fact while all the references to the elements of Γ has been “captured” (the meaning is set immutable). The biological parallels are also obvious.
The notion of an environment is required (necessary), just as Γ is required for any system of logic (which tries to capture the universal notions of What Is).
So, some arrows corresponds to the “mappings” or “transitions” of pure functions - nested “single steps” of causality, while others denote various meanings of an “implication”.
First of all
The “famous” (which makes me sick) “False implies anything” of the purists has only and only one meaning:
The false result (statement) does not affect the whole environment (the contents of Γ) or What Is. So the word implies has this (and only this) meaning in this context.
Lets settle this once and for all.
S and K combinators (which are closed forms or closures)
This is what we have
s : ((A → (B → C)) → ((A → B) → (A → C))
This reads (in classic logic): A implies B implies C, implies A implies B, implies A implies C.
The another (denotatonal) reading is this: give me a function from a to b, and by already having a function from b to c, we will have a function from a to c.
This, is, of course, exactly corresponds to a partial application of curried functions, which is, again, a couple of universal notions being captured together.
Partial application, obviously, corresponds to the universal notion of when not all what is necessary and sufficient is present in the particular locality - a partially filled enzyme, not meet required conditions of a reaction.
So, in the notation above we got the currying itself backwards – a function composition via nesting which is what currying is (how it is actually implemented, and this is the only possible way).
And the “forward” reading is this: a presence of A implies presence of (B -> C) (nested in a curried form) implies that, if there is a path (A -> B), there is (already, always) a path from (A -> C).
The“if” there is not just an artifact of the English language usage, it hints on necessity (and sufficiency) and of that everything must be present in the environment (in the same locality).
Conclusion on this one? We have captured the same universal notion within different formalisms, more than once at different levels (abstraction by parameterization).
k : A → (B → A)
This is a left-identity (for a curried function of arity 2 - a join of two arrows), so will eventually have a Monoid – the why S and K are enough.
The notion of a Simigroup captures jet another universal pattern (two arrows coming together and resulting in a “starting point of a the next arrow of the same kind”), and no, there is no identity elements or functions in What Is, but a lot of concatenations and “coming togethe”.
Kleisli arrows, by the way, are another proper “capturing” of the notion of “crossing an abstraction barrier” or just a single step with a structurally kind of a result. Anyway.
S
Lets do familiar (less confusing) renaming of the type-variables and the terms first
s :: (a -> b -> c) -> (a -> b) -> a -> c s = \f -> \g -> \h -> f h (g h)
We have removed the optional parenthesis due to the associativeness.
What we see is a function composition of terms of different arity, which themselves (f) may be curried. So, yes, currying at different levels, or currying of currying.
f :: a -> b -> c f = \a -> \b -> undefined
g
g :: a -> b g = \a -> undefined
h is of arity zero, which corresponds to a binding, so it should be named x
h :: a h = undefined
One more time - what we have there is a function composition. Not just that, but parameterized by a necessary “step”.
To see everything clearly we just have to partially apply s and examine the types. Eventually we will have just a -> c, which everything already “present” (captured withing a closure).
This is a universal form. Enzymes are like that. Or mathematical or logical statements (intermediate results).
K
A curried function of arity 2.
k :: a -> b -> a k = \a -> \_ -> a
which discards its second argument and is an identity on the first (the left-identity)
An identity function is the most general in principle, so it takes functions (of any arity) as its arguments.
Identity could be seen as a constant term, which is the name k misleadingly suggests.
The usual reading of A → (B → A) in logic is:
A implies [there is some] (B → A) [which justified it].
We could also read:
[the presence of] A implies [there was some] (B \rightarrow A) [which caused it].
Sometimes “implies” may have the meaning “causes”, which is subtly NOT the same as “necessary and sufficient”.
The “universal law” (which different formalisms are trying to capture) is that necessary and sufficient requirements must be present in the environment, in the same locality (or in Γ), so the Causality may advance another step (the Universe as a “runtime” evaluate another form).
This is the universal notion properly captured in logic. The Modus Ponens is another universal notion (of a single step of Causality).
Here, however, the implementation of k, which discards b has very different meaning and reading.
First, the type should be written as k :: a -> (_ -> a) and the meaning is:
anything implies (or causes) a.
Looks very much like the False implies everything purist’s bullshit.
Another, proper reading is: a is just there, or a just is (there is a) [regardless of ~b~].
So the arrow there is from (of) currying, not of an implication or of a single step (mapping).
And the final reading is:
given an a and also [any] b there is (still) an a (and b is /unrelated).
The notion of being unrelated is, of course, the most fundamental and “the most” universal. Most of events are unrelated (they all, of course, are related only in the unwinding of the causality - being the sub-processes of the same single Universe).
In short, the shape of the Universe is a directed /acyclic graph, and the joins are not the cyles (due to one direction “traffic”).
Forks are just abstract notions - they do not exist, only as hyipothetic potentialities - every “step” takes only one path and other “possibilities” do not exist, except for the mind of an external observer.
This is exactly why no conditionals are required. Just nesting of steps is enough.
Now why is this particular form?
Well, g is nested in f, which is the same notion as g is curried within f or that f is implicitly parameterized by g.
On the other hand, partial application reveals more general properties.
Just as partially applied fmap yields a function on a containers, partially applied s (to a binary combinaror) first yields a function on an unary combinator, and then, partially applied again, yields a function on a value.
k, of course, has to be partially applied to s.
Notice that any partially applied combinator (a closure) yields another closure (so the whole thing is a Semigroup), which is “as good as s and k themselves”. The arities, of course, has to match up.
These stable intermediate forms are present in the local context (of the environment) and can be used freely. So s and k are not the only ones out there. This is why the Lambda Calculus has binding and the implicit environment, just as any formal system of logic.
So, the form of s is as it is because it can be partially applied (saturated) to yield intermediate results, which can be used freely.
When s is partially applied to k, which a justification of k’s its existence, the resulting form is a special case – it acts as an left-identity inside of s, discarding the (g h). So, there is a Monoid lurking within.
Now the whole thing has the same properties as the Natural Numbers under addition and all the other Monoids. What is the operation? The composition of individual steps (of arrows) via nesting, of course.
Now try to realize what exactly we (actually the guys who have discovered the sufficiency of S and K) have just captured.