Since April 2019 until I re-visit this Youtube video on 12 August 2019, I can now totally understand his speech after a pause of 4 months by viewing other related Youtube (below prerequisite) videos on Category Theory, Type Theory, Homotopy Type Theory.

That is the technique of self-study:

First go through the whole video,

Don’t understand? view other related simpler videos.

While Mathematicians like to talk non-sensical abstract idea, Informaticians want to know how to apply the idea concretely:

Mathematical Parlance:

Monad = Monoid +Endofunctor

Monoid = Identity + Associative

Endo-functor = functor between 2 same categories

IT Parlance:

Monad is a ‘function’ to wrap the ‘side effects’ (exception errors, I/O,… ) so that function composition in ‘pipeline‘ chained operation sequence is still possible in pureFP (Functional Programming, which forbids side-effects).

Some common Monads: ‘Maybe’, ‘List’, ‘Reader’… This allows monads to simplify a wide range of problems, like handling potentialundefined values(with theMaybemonad), or keeping values within a flexible, well-formedlist(using theListmonad). With a monad, a programmer can turn a complicated sequence of functions into a succinctpipelinethat abstracts away additional data management,control flow, orside-effects.^{[2][3]}

AsTikhon Jelvisexplained in his response, functions map sets to sets, and functions themselves form sets. This is the essence of the untyped lambda calculus. Unfortunately, untyped lambda calculus suffers from theKleene–Rosser paradox(later simplified toCurry’s paradox).

This paradox can be removed by introducing types, as in the typed lambda calculus. Simple types are equivalent to sets, but in order to pass a function as an argument to another function (or return one), we have to give this function a type. To really understand what a function type is, you need to look into category theory.

The categorical model for the typed lambda calculus is a category in which objects are types and morphism are functions. So if you want to have higher order functions, you have to be able to represent morphisms as objects — in other words, create a type for functions. This is possible only if the category is cartesian closed. In such a category you can define product types and exponential types. The latter correspond to function types.

So that’s a mathematical explanation for higher order.

Category Theory (CT) is like Design Pattern, only difference is CT is a better mathematical pattern which you can prove, also it has no “SIDE-EFFECT” and with strong Typing.

The examples use Haskell to explain the basic category theory : product, sum, isomorphism, fusion, cancellation, functor…

Note: We just look at the Category “Types Set” from external Macroview, “forget ” what it contains, we only know the “composition” (Arrows) between the Category “Type Set”, also “forget” what these Arrows (sin,cosin, tgt, etc) actually are, we only study these arrows’ behavior (Associativity).