Applicative

[FizzyElt]

Applicative Laws

1. identity : pure id <*> v = v
2. function composition : pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)
3. homomorphism : pure f <*> pure x = pure (f x)
4. interchange : u <*> pure x = pure (fun f => f x) <*> u

取自 Lean Applicative, Haskell Applicative

如果容器內部為一個純值是無法做 <*> ,seq 的，即 f a 但我們可以將 f a 改寫成 f (Unit → a)

[FizzyElt]

目前不知道要用怎麼樣的方式呈現這四個定律，單純這樣寫出來沒人看得懂 🙃

• 用各語言 ( JS, Lean, Haskell 等等) 實作一個 Container 去驗證
• 用分析的方式把整個函式拆解開來做執行

[dannypsnl]

Lax monoidal functor

但我覺得更根本的問題是代數語義跟代數語法本來就有差

在大部分的程式語言裡面根本沒辦法解釋這件事，畢竟型別在這裡只約束語法的部分

而實現律是源自語義

[dannypsnl]

Monoidal category

當一個範疇 $\mathcal{C}$

1. 配上一個形如 $\otimes : \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ 的 bifunctor
2. 有一個 $\mathcal{C}$ 物件 $I$ 令 $I \otimes A \cong A$ 跟 $A \otimes I \cong A$ 對所有 $\mathcal{C}$ 物件 $A$ 成立
3. 對任意 $\mathcal{C}$ 物件 $A, B, C$，有 $(A \otimes B) \otimes C$ 跟 $A \otimes (B \otimes C)$ 成立

Monoidal functor

對兩個 monoidal category $\mathcal{C}, \mathcal{D}$ 保持 monoid 結構映射的 functor

所以

1. $I\mathcal{C}$ 投射到 $I\mathcal{D}$
2. $\otimes\mathcal{C} : \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ 投射到 $\otimes\mathcal{D} : \mathcal{D} \times \mathcal{D} \to \mathcal{D}$

Lax monoidal functor 更寬鬆的部分是指用 $\bullet$ 取代 $\otimes_\mathcal{D}$，也就是說結構依然保留，但是 $\bullet$ 只需要是一個 bifunctor，不需要滿足 monoid category 的其他條件

[dannypsnl]

1. https://stackoverflow.com/a/35047673/6789898
2. https://stackoverflow.com/a/62959880/6789898

[dannypsnl]

我已經深切體會到這個有多進階了，需要仔細考慮 2-cat, enriched 跟 monoidal cat 之後再想吧，暫時可以放棄