Lets talk about some targets no one else sees.

I am a prod student of Brian Harvey, the great. I used to watch his CS61A recordings like other people watch stupid TV serials. For me it was something like watching X-Files or Twin-Peaks, which are only non-stupid ones.

The problem was, however, that even if I understand every word and almost every concept mentioned, I didn’t know which are the most fundamental ones and which are just accidental notions or just preserved in a shared culture social constructions.

It took a lot of time and Reading classic CS and Math textbooks to sort out what is fundamental and even Universal, and what are just nice memes.

The fundamental and universal notions are the “penetrable partitions, sort of a biological cell membranes with their “portals” and “pumps”, from which our abstract interfaces has been intuitively generalized”.

In the old times they used way better vocabulary, and called thing by its proper names. So they said a “type-signature” which describe a procedural abstraction (which should implement a pure function) in classic languages.

A set of such type-signatures is a partially-defined abstract interface. Partially, because just a set is not enough, we also need a specification – the rules, the “laws” and “invariants”.

The universal notion is of an actual Abstraction Barriers (our membranes between partitions) and how such abstraction barriers can be implemented using Abstract Data Types.

These notions can be traced back to something very general (abstract) and nevertheless actual and profound. Lets have some excursion to the realms of very general abstractions.

When we are trying to understand what an Abstract Data Type actually is, we would notice that there are two distinct kinds of procedures in its public interface – so-called constructors and selectors. Constructors return actual data values, while selectors are used to actually use a value, at so-called “use-site”. The oversuse of the word “use” is intentional. The other “site” is, well, a “construction site”.

There is a seemingly unrelated notion from Gerhads Gentzen’s formalism of Natural Deduction – the rules come in pairs – an Introduction rule and an Elimination rule. The rules are being “constructed” and then somewhere else they are being “used”.

Consider Algebraic Data Types (at a higher level). Conceptually, a sum-type is a set partitioned into possible alternative no-overlapping outcomes. Technically, it is a set of all possible (alternative) data-constructors. Only one alternative will be used at a “creation site”, and this particular single value will be passed around. At the “use-site” the value will be pattern-matched against all possible “tags” (data-constructors) and then the only one (“branch”) will be selected. It is also called an “either-of” of “one-of” type.

A Product Type is at the “creation site” fills all its “slots” either explicitly with the parameters or implicitly within a data-constructor using some default values. The structured value will be passed around as a whole, which is the main point. At the “use-site”, however, a single “slot” would be selected at a time (using some individual selector or a generalized operation which selects “by name”).

Some people would claim that these types thus are isomorphic to each other when we consider their respective “dots-and-arrows (arrows-between-dot)” diagrams. At the minimum of two alternatives and two slots both a sum and a product type would look like \(<\),with the arrows pointing “in” for a sum and “out” for a product. From many data-constructors one value, from a single data-constructor multiple slots.

What exactly does this isomorphism capture? “Forks” and “joins” are isomorphic to each other too. A fork is (sort of) an “introduction” and a corresponding join is an “elimination”.

Now consider that at each fork of a flow a single water molecule takes only one branch, each particle takes only one of all possible paths (whatever this means), and that any function of arity more than one (a Curried function) is a “join”.

Did I already said that the Algebraic Data Types can be nested and are enough for everything?. And that “forks” exist only as “potentialities”, alternative paths on an algorithm-charting diagram? That all the algorithm-charting patterns can be decomposed to just sequences, forks as conditionals, joins as functions, and recursion for loops?

Another seemingly unrelated notion is of message-passing from Biology. Messages (actual particular molecular structures) are being created by enzymes (mechanical procedures) at one “site” and then, after traveling freely some distances, being “used” somewhere (presumably by another enzyme). Notice that there is no notions of time nor a particular odering involved

The “target” is to realize that “what we need” is just a very few Universal notions, properly generalized, upon which everything has been built (by biological process) or could be build and these notions reccur (re-emerge) at all levels, including the most abstract (but non-bullshit) ones.

We have seen this a lot without understanding. The notion of an ADT is the basic building block, similar to some specialized locality (a subprocess) within a cell. An individual procedure is, of course, an enzyme, and suddenly, the totally abstract notion of a Curried function is just abstract notion of a “partially filled” enzyme .

Abstract Interfaces, are actual implementations of conceptual abstraction barriers. To actually work the abstraction has to be “non-leaking” (proper closures) and interfaces has to be “abstract”, meaning that nothing but the type-signatures of the “pumps” and “portals” have been exposed on the membrane (an abstraction barrier).

These are the very foundations. As it will turn out, the universal notions behind logic, math, CS and the part of biology which aurally do information processing (at the molecular level) are the same, and there are just a handful of them.

Non-bullshit mathematics (which studied a properly captured notions, abstracted out as mathematical objects) has already been captured all of them. We just didn’t sort them out.

So, lets list dome of them to have a fell of it.

  • a symmetry (different point of view on the same process)
  • commutative and distributive “laws” which just generalization of symmetries.
  • associativity as concatenation
  • a Monoid (an operation which produces the same kind of values)
  • all the set-theoretic notion
  • the function theory (the part which reach isomorphisms and homomorphisms)
  • a mathematical closure (over an operation)
  • a logical closure (over all the “free” and bound symbols)
  • the composition of functions (and the related part of the Category theory)

This is the locus, an entangled essence. The Curry-Howard Isomorphism clearly shows that this is so. The same few properly captured notions everywhere, at all levels

There re some other, which almost always being neglected.

  • the generalization that Sets can be defined by a set of operations (not just a predicate on a common property).
  • the notion of a binding
  • the \(\Gamma\) as the set of all previously known results
  • an environment, which has binding for all symbols
  • how every word in a spoken human language has to be a binding to its meaning
  • how cells are always within their particular locality (biological environment)

And a few more “captured principles”

  • the notion of counting and therefore of an abstract time does not exist at the level of molecular or cell biology.
  • the fundamental mathematical notions can be clearly separated (partitioned) into “properly captured” (existent) and “socially constructed” (non-existent).

Once done, this will show (unveil) What actually Is and the “basic building blocks” could be clearly seen.

They are already visible (at least to some) who asked the questions like “Why The Nartueal Deduction or the Lambda Calculus or the Set Theiry or the Functions or the aspects of the Category theory are “enough for everything”, or “why a system of logic is what it is”.

The problem with current understanding is that we mix and match implementation aspects within abstract notions, and they should be separated and well-typed (sorted out). The type-classes and duck-typing in general is the way to go..