Zoom

To be any good as a programmer (not a coder or a webshitter - a person who does webshit) one has to be able to zoom through layers upon layers of abstractions (grounded in What Is) and being able to comprehend and understand all the details (or at least the fundamental underlying principles) at each level.

Attention to details is not optional at representation and implementation levels, and this is what largely constitutes Japanesse (or any other) art-forms.

Principles, by the way, are correct (closest to What Is) but informal descriptions of what causes an observable (by an external observer) behavior (or a particualar pattern) at each level.

Precise, formal describtions of proven properties of a particular abstraction (such as Natural Numbers) could also be called principles.

Understanding of principles frees one from memorizing all the particular details.

A sequence of steps

It is not an arbitrary coincedence that we see connected arrows almost everywhere as we are trying to model (using mathematics as a language of precision) aspects of the reality.

Mathematics, by the way, is a formal study of patterns which arise in What Is. It expands by generalizing and defining pure abstractions (abstract entities) and studying their properties and relations among them.

Mathematics, thus, is the most general language for talking about common patterns and well-defined (in terms of their properties and structure only) abstractions.

When we see connected arrows we usually mean a sequence of discrete steps.

A single arrows denotes a transition (or a transformation) - a single step, which may, in turn, be abstracted out as an application of a function or a binary operator.

At a higher level (of types) an arrow also denotes a composition of funtions - a single step at the level of pure functions - one level higher than that of values.

Notice that these are just arrows at the type level

(.) :: (b -> c) -> (a -> b) -> a -> c
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c

(>>) :: m a -> m b -> m b
(>>=) :: m a -> (a -> m b) -> m b

Arrows could denote not just steps but also relations between values.

ANDs

There are actually two ANDs, which are always confused and sometimes not even distinguished

AND ALSO, which corresponds to a logical conjunction or \(\land\)
AND THEN, which corresponds to an arrow of composition or \(\circ\)

This is the result that took long time for me to arrive at.

Notice that the first AND is declarative, and is a generalization of AND IS ALSO TRUE, and (wow!) 2 AND ALSO 2 while the second AND is also declarative but defines a single STEP in a particular direction.

Guess why a single-step evaluator (or mechanical reducer of logical expressions) is the way it is?

The Category Theory

Other people study functions and their compositions in terms of dots and arrows.

The only usefulness of the Category Theory is that it formalizes what common patterns - common arrangements of arrows - are there and what properties such arrangements have. In particular, it is imortant to realize when considering a pattern that such and such arrows are all that is there (the only possible ones).

When we constrain ourself to the patterns of arrows which does not have “forks”, but “joins” are possible (which corresponds to collapcing of a structure or to application a “multi-argument” or curried functions), we would arrive at a most general structure of almost everything What Is, as a generalized abstract visual model, of course.

This is the obvious connection between TLA+ and the Category Theory, and this connection is, of course, through What Is.

A sequence of discrete steps, which may be denoted as a set of connected arrows in a linear structure (or in a structure which can be traversed into a linear path, such as a finite tree) is a universal abstraction.

Not surprisingly, currying, function composition, and a transition from the current state to the next form such sequences of steps or pathes, which always imply a direction, which, in turn, captures causality and unfolding of a process (by causality) in abstract “time”.

Notice, that the only use for abstract theories such as the Set Theory or The Category Theory is that some universal patterns are precisely defined and thus well understood.

When we reduce some part of a problem to something which is well-understood we can use all the related formal knowledge - theorems, lemmas, “laws”.

Functional Programming

This, by the way, is the reason behind (and a connection to) the functional programming paradigm. There are well-understood pattens, and even “laws” in pure functional code which defines and implements sequential, tree-like and table-like data structures and related Abstract Data Types.

Notice that programming could be reduced to just 3 visual patterns - a sequence (again), a loop (which can be unfold into a sequence) and a “branch” which corresponds to a conditional expression, which, in turn, describes alternative possibilities (and this is what “forks” are).

Notice also, that “forks” never arise in reality, only in abstract models of some aspects of it.

An actual sequence of “events” always goes through one branch OR another and an alternative branch DOES NOT EXIST in What Is (it is a super-imposed abstraction by an external observer).

So, it seems that everything is reducible to a sequence of discrete steps (or a sequrnce of events), which can be represented as connected arrows - paths without forks or loops.

This is where you zoom to.

Discrete Math

The good thing is that we need just the very essence of Discrete Math - the Set Theory, the Category Theory, the core of the Number Theory (that numbers are a generalized abstraction and could be viewed as having an abstract structure - being a sum or a product or a weighed sum of other numbers) and the Graph Theory (which captures and abstracts out pattens which arise in What Is, while most of the pure theoretical fancy bullshit (about possible categories of categories, for example) could be safely discarded (or pruned out).

And this “locus” of universal pattens is what a good programmer should study.

The reasoning above partially explains why pure functions and a list structure considered as the core of functional programming - almost everything could be reduced to them.

Remember that a table is just an a list of ordered pairs (or a set of binary relations) and a tree is a list with more than one tails, and that a list itself is just a bunch nested pairs, and “conses” could be implemented as lambdas.

All you need is Lambda is another great fundamental result (by Alonzo Church), which confirms that everything is reducible to nesting of lambdas, which is the only implementation for sequencing (connected arrows!) in a Normal Order language.

And this is the beg picture one has to have in one’s mind.

This, by the way, implies that all these gigabytes of frameworks are, probably, unnecessay, redundant abstractions made by ignorant virtue-signalling idiots to bullshit their bosses and other people.