, | → ˆ () =

Have you seen the language I have designed in which the sum-types and product types are the most primitive primitives? (You) haven’t seen nothing.

Okay, let’s build some from the /First Principles, right from the ground up of Underlying Reality and Causality Itself.

What Is the most fundamental non-quantum physical notion? An Atom, which is an Energy being trapped or in a particular physical locality? Noo. Energy Itself, which cannot be created or destroyed, only transformed from any “form” to another (so we say it is being conserved within the Universe)? Yes. By the way, here we do not consider quantum “physics” as physics. It is a theoretical socially-constructed pseudo-science. Modern day Tantric teachings.

Before my good friends start to look at me suspiciously – there is Buddhism and Tantric “.Buddhism”, just like there are Physics and Quantum “physics”, Philosophy and Western “philosophy”.

So, we will use the second most physical notion, of a Locality, and the third – of an Observer or rather Observability [of what we usually call Events].

Observability is the key principle, from which everything follows. At least the abstract notions of a Product of a Coproduct, which are said to be duals of each other, but only by idiots.

Within a particular physical Locality we can observe Nothing, a single Something or more than one of Something. (the Natural Numbers 1 and 2 just have emerged by themselves, 2 being one more than 1). We will for now put Nothing and the corresponding symbol of 0 (usually defined as x - x) aside, as being special case, and will leave the inductive structure of Natural Numbers alone.

When we observe more than one of Something, we say we have a product. If we are more mathematicians than physicists, we will stay that 1 of Something is also a Product, or even that () is a Product of size 0 and that we observe Nothing.

Notice that in the Real World, when we observe two atoms, they are being bound together (by mutual forces), so, again, at least 2 and the bonds “define” and hold together the compound (an actual atomic structure).

What is a Coproduct then? Well, it is when we are observing exactly 1 of Something, which has 2 or more possible “forms” (shapes, variants, tags). If we are mathematicians, we will say that there is a Coproduct of only 1 possible form of Something, but this is bullshit.

Here is why. The number 2 is special (maybe this is why it is the only even Prime). When we have a partition – literally, a | – it has at least 2 sides, so the counting begins at 2. For a Product counting begins at 1.

This is the job pf a Natural Philosopher – to call [abstract] bullshit.

In the Category Theory they said that the \(∏{A}=A\) is a perfectly valid Product ,and \(∐{A}=A\) is the Coproduct of one object. We accept the former on the ground of 1 being the identity element for multiplication (as repeated addition), and reject the later,as mere non-existent socially constructed abstract bullshit. They also said that \(∏∅ = terminal object\), which is OK, since \(x * 0 = 0\), and a Product of an (or even “the”) Empty Set is the very same Empty Set (Nothing and Nothing). In general, any operation applied to Nothing or Absence of a Value, must produce strictly Nothing or Absence of a Value, just because this is an absurd.

Amazingly, Thermodynamics Itself agrees with this part – there is no such thing as zero energy, or total and absolute absence of anything, but if you want to masturbate, you better not to produce anything whatsoever out of Nothing, so either 0 or ~\(\empty\).

There is more of the why. The Set of Possibilities (possible forms, possible outcomes, possible observable events) has to be defined prior to definition of a Coproduct/. The cardinality of the Set of Possibilities has to be 2, because less than 2 does not constitute an alternative Possibility, so the whole notion collapses, and ceases to have a real .meaning (which is never a problem for mathematicians, who could easily have a Coproduct of just one possible alternative – an A | with Void on the other side of the partition).

Because we have to respect Mathematicians and because we do not know whether a second possible alternative exists or not, we can denote this | A construction (notice the reversed order of the symbols) and even pattern-match on it.

data A = A

Is perfectly valid type and we can define functions using pattern matching on values of this type, which will always be one and the same.

Ok, here is more. There is a reason why having a single “possible alternative” is bullshit. Your if statement will have no valid else clause – there is only one constructor and for the type and you have nothing to return in as a value of the same type in the else branch. As you may notice, a proper if expression, which required else clause and the constrain that the values for both branches has to be of the same type, is isomorphic to the fully saturated |, and the later comes prior to the former (and the set of possibilities comes prior to both).

This, by the way, is an illustration of the a priori principle at work – you first have [a set of] “atoms” and then you observe them [in different ways].

Tuples are how they represent Products.

There is another interesting observation – in Haskell they threat an “empty” tuple () as a distinct Unit type, does not allow a singleton tuples (1,) and have a distinct type for each possible size.

The () type is special, because it has only one value in principle – a singleton set of just a single element, which is also denoted as ().

type Unit :: *
data Unit = ()
   -- Defined in ‘GHC.Tuple’

The whole set of operations has been defined for just a single possible value (which always return just the same ().

instance Semigroup () -- Defined in ‘GHC.Internal.Base’
instance Monoid () -- Defined in ‘GHC.Internal.Base’
instance Bounded () -- Defined in ‘GHC.Internal.Enum’
instance Enum () -- Defined in ‘GHC.Internal.Enum’
instance Ord () -- Defined in ‘GHC.Classes’
instance Read () -- Defined in ‘GHC.Internal.Read’
instance Show () -- Defined in ‘GHC.Internal.Show’
instance Eq () -- Defined in ‘GHC.Classes’

Notice how they managed to define a Monoid, using the only value as an identity element. They also defined composition as constant but also returns the identity element (while identity is unary function and composition is a binary one). Equivalence relation re-states the Everything Is Equal To Itself axiom (which is only reflexivity), and the Total Order relation asserts that every Singleton set is Totally Ordered.

By the way, an equivalence relation requires three properties:Reflexivity,Symmetry and Transitivity, and Symmetry and Transitivity all hold trivially because there is only one element,

There is a catch – they forbid the existence of a Singleton tuples (containing only a single value) because they cannot be easily distinguished for “just” a value. If we just “tag” a value as a singleton tuple, then what is the point of having “untagged” values.

To be mathematically precise (and fancy) – the set of all values is isomorphic to the set of all values tagged as singleton tuples, and thus, by the axioms of the set theory, is the same set and thus is the same type (except the type-tags, which is how we conceptually mark the values and pattern-match against these tags).

This hair-splitting shit we do for a living.

type Tuple2 :: * -> * -> *
data Tuple2 a b = (,) a b
   -- Defined in ‘GHC.Tuple’
type Tuple3 :: * -> * -> * -> *
data Tuple3 a b c = (,,) a b c
   -- Defined in ‘GHC.Tuple’

and so on…

So, why don’t they forbid the singleton sum-types? Well, the tradition just says that every type of just one value (of a single data-constructor) is a Sum-type (or a Coproduct) and not a Product-type, which is, of course, wrong .

Both Products and Coproduct, (as Universal Constructions) structurally must have at least 2 arrows.

The * -> * “Construction” is for very different notion of a “step”.

type (->) :: * -> * -> *
type (->) = FUN Many :: * -> * -> *
  -- Defined in ‘GHC.Types’

Notice that the Tuple2 and -> have the same Kind * -> * -> *, which means the type-constructors, including the Order of arguments, are equivalent?

This is why a function defined on a finite domain can be represented as a set of Ordered Pairs or Tuples. The * -> * and (*, *) have exactly the same algebraic structure (an Ordered sequence) and carry or represent exactly the same information.

In general, a function on a finite domain A -> B is isomorphic to a Product of values \(B^∣A∣\) (a set o all individual a, b pairs, which is isomorphic to its graph \({(a,f(a))∣a∈A}\).

Notice also that (a, b), c and a, (b, c) are isomorphic to each other and carry the same information, more subtle, so are a -> (b -> c) and a -> b -> c , and also (a,b) -> c which is Currying.

Currying is universal because of a categorical isomorphism \(Hom(A×B,C)≅Hom(A,Hom(B,C))\) (the same set of “individual arrows”). That is the universal property of the exponential object.

All this comes from the facts that all different orderings (permutation) of a set carry exactly the same information, and that the order of writing (enumerating) has to become a representation invariant of a resulting sequence, and shall be the same as the order in which reading will eventually occur.

In other words, a product has no intrinsic positional order. Once we choose an encoding (by writing it down as an arbitrary ordered sequence), however, that order becomes fixed (a representation invariant). . Notice that a Curried function which is just a bunch nested lambdas, to be eventually evaluated in the only possible Causal order, so they are structurally equivalent to an arrangement of nested pairs, assuming all the returned values are already known.

The Causal Order is being established by nesting, so the returned value, taken as an input, structurally always appears before (prior) the result (output) of its application.

When you pass a function and its augment around (unapplied yet) it is the same as to pass an argument and the result, because the result is always the same for a given argument.

This is how fundamental (and how necessary) the Referential Transparency property is.

So, the Lambdas and their composition, the most fundamental (and the only – necessary and sufficient) building blocks.

All (You) need is Lambda!, long live, prof. Brian Harvey, the great!

There is a lot of hairs to split. A mathematical Function is a special type of binary relation between two sets. For a relation to be defined as a function, every element in the domain must map to exactly one unique element in the codomain. However, functions are not strictly one-to-one correspondence, since many “individual arrows” could end up on the same value of the co-domain.

A special kind of function called Injection or “one-to-one” when every distinct input maps to a unique output, meaning no two inputs /share the same output. A special kind of function which have strict one-to-one correspondence between the elements is called a Bijection, meaning that each element in the codomain also have a mapping to a unique element on the domain.

This means that each “individual arrow” between elements of domain and codomain have a corresponding inverse arrow “in the opposite direction”.

This is the proper basis to formally define (capture the notion of a) [structural] isomorphism, which just means “to have exactly the same structure (algebraic or not)”. For a set, which is, arguably, is the simplest compound structure, it is not just to have the same number of elands (which is sufficient – every set of the same cardinality is isomorphic – structurally the same – to each other) but to “show all the individual arrows in both directions”.

Showing “all the individual arrows” (also called “morphisms”) is the key.

So, a function, which we used to denote as a singe right arrow, is “actually” a “whole bunch of individual arrows” (at most one for each element of the domain).

When the domain has only single element, then there is only a single arrow, otherwise it is not a function. The codomain can be larger, the same or smaller set than the domain, and this is where the “jections” come from.

The only invariant for a function is that every element of the domain must have exact;y one outgoing arrow – not zero, not more than one. The “landing” of the arrows is “arbitrary”, as well as the size of the “range”.

We have to return one more time to Products.

A Product is an “object” \(A×B\), which has two possible representations as tuples. – (A, B) and (B, A) – which are “the same information” if you rotate them (or rotate yourself around them).

The CO molecule is the same no mater of rotation or location of an observer, it is our convention to write it as CO and not OC (no chemist will understand this). So is an abstract Product “object” \(A \times B\).

But once you say that (A, B) a set of coordinates (of individual ordered pairs (x, y)), let’s say, you cannot “rotate” the tuples anymore, since (x, y) \ne (y, x) – not the same information.

Where all this hair come from? The either 0 or 1 (Nothing or Something, Absence or Presence) is the fundamental dichotomy, while the qualitative distinction between \(x\) and \({x}\) is another one.

Now, since we are writing programs (and sometimes mathematics) we always have to remember that a tuple always has an implicit Order, while the underlying concept of a Product of two “objects” does not. A Product is an “abstract molecule”, existing independently of an Observer and may have more than one “written representations” (depending on where an Observer is located).

Also Currying is not about the syntax (not a merely syntactic trick), it is about having exactly same set of morphisms out of a Product of the domains and composed (nested) single-argument functions.

We have already discussed \(A \times 0 = 0\). What about the \(A + 0 = A\). It suggest that A | Void is a valid Coproduct.(no value of the type Void can ever be created in principle).

This is exactly where mathematical purity is going to far away from underlying Reality. Yes, adding nothing does not change anything. But choosing among possible alternatives is not the same notion at all.

Yes, with symbols and arrows drawn on a paper, There can be zero arrows, just one arrow and more than one arrows be drawn from any “object”. The paper is Okay with this.

So they claim that -> A (a single injection) and A -> (a single projection) are perfectly valid constructions. They also claim that these are dual of each other, again, on paper.

In the case of a Product of just one element everything seems trivial – A single element, single projection, a single unique function which produces the same “object” back. A tautology.

With Coproduct of an underlying singleton set, which, by definition, is isomorphic to the (), we are always getting the same observation, so it is just a constant function or pattern-matching against a constant. But an if expression is incomplete, while the pattern-matching is exhaustive. A function defined by clauses (with only a single clause) will be a total function (just as a pattern-matching expression exhaustive).

That incompleteness of the if expression – a fork with only one “branch/arm” is not a fork (it is a step!) is enough to reject the empirical validity of the single-object Coproduct.