# 函数概念并不难，理解“函”字是关键——函数概念如何理解】

The unique 1 single output of a function becomes very important for subsequent development in Math & IT:
functions are composable, associative, identify function，etc (distributive,… ) => it can be treated like vector => structure of a Vector Space “Vect”

Extended to..

“Vect” is a bigger structure “Category” in which “function of functions” is a
Functor” （函子）F：F(f)

Example : F(f) = fmap (in Haskell)

fmap (+1) {2,7,6,3}

=> {3,8,7,4}

here F = fmap, f = +1

The Math branch in the study of functions is called “functional” 泛函。

IT : Functional Programming in Lisp, Haskell, Scala, ensure safety of guaranteed output by math function property. Any unexpected exception (side effects: IO, errors) is handled by a special function called “Monad” (endo-Functor).

(想看更多合你口味的内容，马上下载 今日头条)

# A Functional Programmer’s Guide to Homotopy Type Theory (HoTT)

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:

1. First go through the whole video,
2. Don’t understand? view other related simpler videos.
3. Repeat 1.

Prerequisite knowledge:

1. Homotopy
2. Type Theory
3. Homotopy Type Theory
4. Bijection = Isomorphism
5. Functional Programming in Category Theory Concept: Monad & Applicative

Two Key Takeaway Points:

1. In the Homotopy “Space” : Programs are points in the space, Paths are Types.
2. “Univalence Axiom” : Paths Induce Bijection, vice versa.

# Knowing Monads Through The Category Theory

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

Mathematical Parlance:

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 pure FP (Functional Programming, which forbids side-effects).

This allows monads to simplify a wide range of problems, like handling potential undefined values (with the Maybe monad), or keeping values within a flexible, well-formed list (using the List monad). With a monad, a programmer can turn a complicated sequence of functions into a succinct pipeline that abstracts away additional data management, control flow, or side-effects.[2][3]

# Quora: Functional Programming / Side Effect / Monads

Introduction:

• The curse of Immutability in Functional Programming – no “Looping” (recursion ok), no Date, no Random, …no I/O …

Monads ~ “Design Pattern” in Functional Programming

Examples: “Option”, “Some”,…

Dr. Eugenia Cheng ‘s Lectures on Category Theory (2007)

The name “monad” came from “monoid” and “triad”, which indicated that it is a triple (1 functor + 2 trasformations), monoidic algebraic structure.

Monad = Monoid (restricted to endofunctors)

Note: She was annoyed nobody had corrected her mistake in (red) Tμ . (I discovered it only on 2nd revision view few years later).

Monad for Small Categories (= Set)

Ref:

What is the difference between Monoid and Monad? (Bartosz Milewski )

Functor: 函子

# Program = Category

2017 : (PhD Math made simple for IT programmers)

Keywords:

• Category
• Monad = Monoid + Endofunctor
• Lewvere Theory

Category Theory is replacing Set Theory as the foundation of Math. Nowadays, few Advanced Math papers are written without using Category to explain, and this trend is spreading to IT through Functional Programming languages (Google’s Kotlin, Haskell, Clojure…) – the latest paradigm to replace Object-Oriented languages like Java, C++, etc, as a safer “Strong Typed” languages for AI, BIG DATA…

$\boxed {\text {Type = Category }}$

Examples of “Types” in IT:

• Integers
• Real
• Double
• Boolean
• String
• etc

T-program defined in the following 6 examples:

• list (X), eg. {2, 5 , 3, 7, 1 }
• partial (X), eg: +1 (error msg)
• side-effect, eg: update a record
• continuation (X),
• non-det (X),
• prob-dist (X)

A Monad : a T-program which turns an arrow to a “Category” (ie + 2 properties: Identity & Associative).

Proof: List Computation is a Category

Proof: Partial operation is a Category

$\boxed {\text {Monad = Lawvere Theory }}$

Monad is for only one Category. Lawvere Theory is more general.

Ref:

Ref:

A well-said, perhaps the briefest ever answer is: monad is just a monoid in the category of endofunctors.

monoid is defined as an algebraic structure (generally, a set) M with a binary operation (multiplication) • : M × M → M and an identity element (unit) η : 1 → M, following two axioms:

i. Associativity
∀ a, b, c ∈ M, (a • b) • c = a • (b • c)

ii. Identity
∃ e ∈ M ∀ a ∈ M, e • a = a • e = a

When specifying an endofunctor T : X → X (which is a functor that maps a category to itself) as the set M, the Cartesian product of two sets is just the composition of two endofunctors; what you get from here is a monad, with these two natural transformations:

1. The binary operation is just a functor composition μ : T × T → T
2. The identity element is just an identity endofunctor η : I → T

Satisfied the monoid axioms (i. & ii.), a monad can be seen as a monoid which is an endofunctor together with two natural transformations.

The name “monad” came from “monoid” and “triad”, which indicated that it is a triple (1 functor + 2 trasformations), monoidic algebraic structure.

In other words, monoid is a more general, abstract term. When applying it to the category of endofunctors, we have a monad.

Brian Beckman:

You can understand Monad without too much Category Theory.

Functional Programming = using functions to compose from small functions to very complex software (eg. Nuclear system, driverless car software…).

• Strong Types Safety: detect bugs at compile time.
• Data Protection thru Immutability: Share data safely in Concurrent / Parallel processing.
• Software ‘Componentisation’ ie Modularity : Each function always returns the same result, ease of software reliability testing.

Each “small” function is a Monoid.
f : a -> a (from input of type ‘a‘ , returns type ‘a’)
g: a -> a

compose h from f & g : (strong TYPING !!)
h = f。g : a -> a

[Note] : Object in Category, usually called Type in Haskell, eg. ‘a’ = Integer)

You already know a Monoid (or Category in general) : eg Clock

1. Objects: 1 2 3 …12 (hours)
2. Arrow (Morphism): rule “+”:

7 + 10 = 17 mod 12 = 5

• Law of Associativity:
x + (y + z) = (x + y) + z
• Identity (or “Unit”): (“12”):
x + 12 = 12 + x = x

More general than Monoid is a “Monoidal” Category where: (instead of only single object ‘a’, now more “a b c…”)
f : a -> b
g: b -> c
h = f。g : a -> c

Function under composition Associative rule and with an Identity => Monoid

Monad (M): a way to manage the side-effects (I/O, exception , SQL Database, etc) within the Functional Programming way like monoidal categories: ie associative composition, identity.

Remark: For the last 60 years in Software, there have been 2 camps:

1. Bottom-Up Design: from hardware foundation, build performance-based languages: Fortran, C, C++, C#, Java…
2. Top-Down Design: from Mathematics foundation, build functional languages (Lambda-Calculus, Lisp, Algo, Smalltalk, Haskell…).
3. F# (Microsoft) is the middle-ground between 1 & 2.

Ref: What is a Monad ?

Monad = chaining operations with binding “>>=”

• Possible use: allows to write mini-language, parser…

《知乎》https://zhuanlan.zhihu.com/p/29542641?from=timeline

# BM Category Theory 10: Monad & Monoid

Analogy

Function : compose “.“, Id