Metaphysics
Distinction between True and False statements “partition” the “universe of discurse”.
A predicate (or an assertion) could “land” on either side - could be either True or False.
So it is a “fork” which sorts into two distinct, non-overlapping “buckets”.
\[\{ x \in S | P(x) \}\]
Or, to be more precise, to a single partition (a subset) of Truth in the sea of bullshit.
not True = False -- a dump
So, it seems that we have partitions and forks between them.
The vertical bar
The logical OR is syntactically expressed as |. It is literally
everywhere and it captures the universal notion of availability of
different forms (as inputs to or outcomes of a process), which the mind
of an external observer captures and expresses as branching.
Partitioning
When we partition members of a Set as distinct possible forms (alternative valid inputs or outcomes) we have the notion of an alphabet (or a finite dictionary of a language or even some infinite set ofnumbers).
And this is the core of pattern-matching (on all possible valid inputs), which is how the captured notion of branching is expressed formally.
Regular expressions, such as
[A-Z]
is an abbreviation for
{A | B | C | ... | X | Y | Z}
Notice that the choices of symbols (which corresponds to distinct sounds) are arbitrary.
Grammars
This is why the BNF of a grammar syntax is full of | (ORs).
It captures the universal notion (a universal pattern). We can write a grammar for DNA sequences and for Lambda Calculus, end each one will be a set of possible inputs or forms.
type Letter = A | C | G | T
Whole number systems
The set \(Z\) (of all Integers) is really
{ ... | -3 | -2 | -1 | 0 | 1 | 2 | 3 | ... }
And if we ask how different these are, we will arrive at the notion of a successor function.
Algebraic types
There is no wonder that we have evolved similar syntax for Algebraic Sum types.
type Letter = A | C | G | T
Of course, GADTs are also based on the fundamental notion of |.
And pattern matching on these types is “natural” branching.
Arrows
A single linked list in a box-and-pointed diagram (oldfags knew) is just a bunch of connected arrows with donts in between.
So is a composition of several functions at a type-level.
Both of these abstract structures could be seen as nested.
A list is a bunch of nested conses, a composition is a bunch of nested lambdas.
This is not a coincidence.
Both explicitly define a particualar order for a Set of values (in the case of a composition - how a value is being transformed by each function in a pipeline).
A list is a serialization at the data level. A function composition is serialization at the function level.