expand_less
I've been rocking and rolling with friends in social media about monads. All the possible meanings as possibly related, but coming from an information systems background, my primary model comes from theoretical and applied mathematics. Category Theory (CT) in general and Type Theory (TT) in formal systems and computational theory are already well established as the rising trend. Those doing it and learning is know that this what functional programming (FP) is all about and why its currency is also on the rise. I want to start from something a little bit formal, but quickly branch and twist towards essoteric grounds in Leibntz and his monad and other metaphoric and ancient sources on the monad conceptually.
First, the entirety of the formalism. Though the expression and diagrams are the same for CT, TT and metaphorically, we find the language is all changed. But the whole point of this theory is that it isn't the names but the structure, therefore when you translate the names, the same work becomes meaningful in another domain. Here it is:
All M : M(A) -> A
Reads more or less: For all categories (types) M as in method in TT, functor in CT, of the type (category) Method for any type A to itself.
Then if you just notice that this is essentially recursive because M is a type (category) and can be also in the place of A. In other words, methods (functors) of methods to methods of the same type signature.
The Monad:
{{Monad Image| type: Image}}
This is metaphorically The One of Greek thought, the generalization and sum of all mathematical/logicial possibility spaces. In Pierce, this is the general rule that is necessarily of a class of incomplete infinities like the ones we find in Godel, Church and Turing. Projecting Leibniz through a little Kantian language, the thing in itself is monadic. Existential monads come and go in our consensual realities, but the miriads of relationships and synchronicities that make monads significant just are.
Not to sidetrack this topic, but I want to be clear what this doesn't entail. This isn't existance from the infinities of Platonic forms in their eternal completeness. We want to consider and be consistent with putting the real of consensual realities we can affirm before any eternal abstractions. Abstractions are not necessary to Be, that comes later in time. What is marvelous is that it does turn out to be as comprehensible as it is. You can't postulate a gounding in laws of logic and math for existential foundations. You'll come up with less than air, nothing.
That said, we now have the emerging spaces created by monadic coverage even if completeness is a fool's errand. In other words, when I write code (FP) and it works with other monads, I can then compose my monad with other monads and get more monads. This is so straightforward that the bots can do it. They can also write the formal proofs the security and financial policies require for critical infrastructure. With all the right wiz-bang tooling on the front and the back, this become drag and drop high level programming. Domain experts draw the relationships with a tool, and presto, code.
First, the entirety of the formalism. Though the expression and diagrams are the same for CT, TT and metaphorically, we find the language is all changed. But the whole point of this theory is that it isn't the names but the structure, therefore when you translate the names, the same work becomes meaningful in another domain. Here it is:
All M : M(A) -> A
Reads more or less: For all categories (types) M as in method in TT, functor in CT, of the type (category) Method for any type A to itself.
Then if you just notice that this is essentially recursive because M is a type (category) and can be also in the place of A. In other words, methods (functors) of methods to methods of the same type signature.
The Monad:
{{Monad Image| type: Image}}
This is metaphorically The One of Greek thought, the generalization and sum of all mathematical/logicial possibility spaces. In Pierce, this is the general rule that is necessarily of a class of incomplete infinities like the ones we find in Godel, Church and Turing. Projecting Leibniz through a little Kantian language, the thing in itself is monadic. Existential monads come and go in our consensual realities, but the miriads of relationships and synchronicities that make monads significant just are.
Not to sidetrack this topic, but I want to be clear what this doesn't entail. This isn't existance from the infinities of Platonic forms in their eternal completeness. We want to consider and be consistent with putting the real of consensual realities we can affirm before any eternal abstractions. Abstractions are not necessary to Be, that comes later in time. What is marvelous is that it does turn out to be as comprehensible as it is. You can't postulate a gounding in laws of logic and math for existential foundations. You'll come up with less than air, nothing.
That said, we now have the emerging spaces created by monadic coverage even if completeness is a fool's errand. In other words, when I write code (FP) and it works with other monads, I can then compose my monad with other monads and get more monads. This is so straightforward that the bots can do it. They can also write the formal proofs the security and financial policies require for critical infrastructure. With all the right wiz-bang tooling on the front and the back, this become drag and drop high level programming. Domain experts draw the relationships with a tool, and presto, code.