解釋 FP 中的 Functor 與範疇論中的 Functor 關聯

[FizzyElt]

我需要一些建議，目前我有個草稿，不知道該怎麼接續程式中的 Functor laws

草稿

即便我們看了範疇論跟 FP 語言中的 Functor 定義，但在概念的銜接上仍然有困難，如果你看了 Functor(functional programming) wiki 會發現他是受範疇論啟發的 design pattern。而到底引用了哪些概念，以及與語言能做到什麼程度，並沒有很好的說明。

如果以「Functor 是兩個範疇之間的映射」這個觀點來看程式中的 Functor 似乎感覺有些奇怪，通常我們看到的範例都是舉兩個不同範疇 $C,D$，如果某一程式語言是一個範疇 $C$ 的話，那範疇　　 $D$ 就會是另一個語言，但現實我們幾乎不會想這樣做。所以這裡唯一的可能是指「 $C$ 與 $C$ 之間的映射」，也就是 Endofunctor 。你可以在 Haskell wiki 以及 fp-ts 作者所寫的 Introduction to Functional Programming 中找到相關說明。

Technically, these laws make f and fmap together an endofunctor on Hask, the category of Haskell types (ignoring ⊥, which is a party pooper). See Wikibook: Category theory.

Even though a map between two different programming languages is a fascinating idea, we're more interested in a map where C and D are the same (the TS category). In that case we're talking about endofunctors (from the greek "endo" meaning "inside", "internal").

[dannypsnl]

我覺得最大的問題是 Haskell 的 functor 甚至都沒有要求 functor law，所以技術上來說你甚至可以寫出不是 functor 的 "functor"。而且，這並不表示 "functor" 是無用的定義，反而有些很實用的定義是 "functor"。

所以 functional programming 裡面 type class 的定位蠻微妙的

[dannypsnl]

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α :=
    Function.comp map (Function.const _)

註：下面忽視任何宇宙問題

直接把程式挖過來看，所以其實只是說有個 f : Type → Type 可以把各種 α → β 變成 f α → f β
所以下面這個程式也是不會被抱怨啦xd

[dannypsnl]

假設限定 F 必須是 inductive 那我們知道因為 F 肯定能被拆解，所以還會好一點

但是 inductive 顯然也不必然需要有儲存其參數，舉例：

inductive F (α : Type) where
  | c : F α → F α

這時候同樣，map 根本就拿不到 α

[dannypsnl]

可見 functor 定義至少需要 F 至少

1. 能被拆解
2. 拆開之後真的有 α 能用

沒有 1 就無從談論定義，缺少 2 就不可能用到給定的函數 f : α → β

[dannypsnl]

滿足兩條件之後，直接來看要是我們要如何不滿足 id law

inductive F (α : Type) where
  | c : α → α → F α

def curmap (f : α → β) (self : F α) : F β :=
  match self with
  | .c x y => .c (f y) (f x)
instance : Functor F where
  map := curmap

這裡只要執行

#eval (curmap id (.c 1 2) : F3 Nat)
#eval (id (.c 1 2) : F3 Nat)

就能證明這確實不是 functor（違反 id law）但 lean 也是沒有抱怨

[dannypsnl]

而要保持 id 的正確性，顯然需要保持結構，因此 functor 至少要不對結構進行變動

[dannypsnl]

#eval (curmap (Nat.succ ∘ Nat.succ) (.c 1 2) : F3 Nat)
#eval (((curmap Nat.succ) ∘ (curmap Nat.succ)) (.c 1 2) : F3 Nat)

這兩個執行則是顯示 curmap 非常有趣的控制了翻轉幾次，它們出現幾次就會有多少翻轉

當然也直接給出了這不是 functor 的反例。

[dannypsnl]

要給出數學上的理解的話，應該可以用 universal algebra

[FizzyElt]

我去多找一些資源來整理一下可以怎麼闡述

• https://en.wikibooks.org/wiki/Haskell/Category_theory
• https://lean-lang.org/functional_programming_in_lean/type-classes/standard-classes.html#functors
• https://nikgrozev.com/2016/03/14/functional-programming-and-category-theory-part-1-categories-and-functors/

[dannypsnl]

1, 2 應該都沒有更深入

3 的說法我們在 issue 就說過了

[dannypsnl]

我覺得多少取決於你要論述多深，要是我們認定所有 type 肯定只能是

1. eval
2. product
3. coproduct

註：polymorphism 來自 index 所以可以跳過

那 universal algebra 就能回答問題了，也就是什麼條件下這尚且還保持 functor 的定義。另外要無視 lazy semantic 的情形。

但要是真的要連同各種 modal 考慮那我也不清楚會是什麼情況。

[FizzyElt]

感覺水很深，目前想法是把 Typeclass 的概念說清楚即可，這樣後續的 Applicative 跟 Monad 比較好接續

[dannypsnl]

對沒錯，甚至多少算是 open question (in my poor knowledge)

[FizzyElt]

目前暫定這個 Section 只幫讀者破除迷思，未來有更多想法可以再補充上去
幫我再過目一下有哪部分敘述不夠精確的地方

草稿

即便我們看了範疇論跟 FP 語言中的 Functor 定義，但在概念的銜接上仍然有困難，如果你看了 Functor(functional programming) wiki 會發現他是受範疇論啟發的 design pattern。而到底引用了哪些概念，以及與語言能做到什麼程度，並沒有很好的說明。

如果以「Functor 是兩個範疇之間的映射」這個觀點來看程式中的 Functor 似乎感覺有些奇怪，通常我們看到的範例都是舉兩個不同範疇 $C,D$，如果某一程式語言是一個範疇 $C$ 的話，那範疇 $D$ 就會是另一個語言，但現實我們幾乎不會想這樣做。所以這裡唯一的可能是指「 $C$ 與 $C$ 之間的映射」，也就是 Endofunctor 。你可以在 Haskell wiki 以及 fp-ts 作者所寫的 Introduction to Functional Programming 中找到相關說明。

Technically, these laws make f and fmap together an endofunctor on Hask, the category of Haskell types (ignoring ⊥, which is a party pooper). See Wikibook: Category theory.

Even though a map between two different programming languages is a fascinating idea, we're more interested in a map where C and D are the same (the TS category). In that case we're talking about endofunctors (from the greek "endo" meaning "inside", "internal").

即使我們將範疇論內的概念與程式做對比，依然不能將範疇論的 Functor 以及語言中定義的 Functor 劃上等號。範疇論有的語言不一定能做到，語言裡有的範疇論不一定有，我們能做的就是將兩者之間重疊的部份做連結。而 Haskell 是透過 Typeclass 來做約束，所以一般正常情況下我們所談論的 Functor 是 Typeclass 內的 Functor class。另外，我們常說「Maybe 是一個 Functor」 指的是 Maybe 是 Functor class 的一個實例 (Maybe 可替換任何其他 Functor class 實例)。

其他 FP 語言雖然不一定都使用 Typeclass 這個詞，但大多 Functor 的定義都差不多。

Haskell

class Functor f where
  fmap :: (a -> b) -> f a -> f b

  (<$) :: a        -> f b -> f a
  (<$) = fmap . const 

Scala

trait Functor[F[_]] {
  def map[A,B](a: F[A])(f: A => B): F[B]
}

Lean

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α :=
    Function.comp map (Function.const _)

Functor laws

光有 Functor class 其實還不夠，因為只要 fmap 的實作通過語言的檢查，都能視為 Functor，而這些實例總有些例外，所以還必須遵守 Functor laws 才能成為真正意義上的 Functor。

$$ fmap\ id = id $$

$$ fmap\ (g\circ f) = fmap\ g \circ fmap\ f $$

[dannypsnl]

「範疇論有的語言不一定能做到，語言裡有的範疇論不一定有」
~>
「大部分的語言並不可能寫出命題，所以範疇論的限制語言裡不一定有加上，這之間的一些漏洞就會產生對使用者來說可能很奇怪的結果」

[dannypsnl]

「一般正常情況下我們所談論的 Functor 是 Typeclass 內的 Functor class」
「在程式語言的語境下所說的 functor 是指 type class 的定義」

[dannypsnl]

「光有 Functor class 其實還不夠，因為只要 fmap 的實作通過語言的檢查，都能視為 Functor，而這些實例總有些例外，所以還必須遵守 Functor laws 才能成為真正意義上的 Functor。」

「Functor class 的實例通過語言的檢查，都被視為語言中的 Functor，然而因為不能施加限制的關係，這些實例並不總是範疇論中的 functor，所以必須檢查 Functor laws 才會是範疇論中的 Functor。」

[dannypsnl]

我覺得很重要的一點是為什麼範疇論裡面的 functor 很重要，主因是因為這樣才會有預期中具備結構保持特性的可組合性。

但確實在程式開發上並不總是需要全部的可組合性，就像我上面給的定義

inductive F (α : Type) where
  | c : α → α → F α

def curmap (f : α → β) (self : F α) : F β :=
  match self with
  | .c x y => .c (f y) (f x)
instance : Functor F where
  map := curmap

交換順序雖然會不滿足 functor 的限制，但在程式上卻可能用到，比如說 c 可能是儲存兩支程式的調度器，這時候交換就有合理的語義。而且 functor class 在語言內部往往跟編譯器的自動展開混在一起，所以加上那些限制也不會更好用。

雖然我一直覺得正確的做法是這樣：

class SemiFunctor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α :=
    Function.comp map (Function.const _)

class Functor extends SemiFunctor where
  id_law : ...
  compose_law : ...

[dannypsnl]

啊，另外 Haskell Wiki 實在不是很好的參考

[FizzyElt]

Haskell wiki 已經算是較容易接觸到的資源了，對一般人比較不陌生 🥹
我自己也感覺好像什麼都沒說一樣

[FizzyElt]

感覺你這段可以弄一個新的 Section，當作額外補充想法之類的

[dannypsnl]

應該可以啊，就接在主文之後補充

[FizzyElt]

修改後，會把目前 Lean 定義那個區塊取消改成這個

初版

即便我們看了範疇論跟 FP 語言中的 Functor 定義，但在概念的銜接上仍然有困難，如果你看了 Functor(functional programming) wiki 會發現他是受範疇論啟發的 design pattern。而到底引用了哪些概念，以及與語言能做到什麼程度，並沒有很好的說明。

如果以「Functor 是兩個範疇之間的映射」這個觀點來看程式中的 Functor 似乎感覺有些奇怪，通常我們看到的範例都是舉兩個不同範疇 $C,D$，如果某一程式語言是一個範疇 $C$ 的話，那範疇 $D$ 就會是另一個語言，但現實我們幾乎不會想這樣做。所以這裡唯一的可能是指「 $C$ 與 $C$ 之間的映射」，也就是 Endofunctor 。你可以在 Haskell wiki 以及 fp-ts 作者所寫的 Introduction to Functional Programming 中找到相關說明。

Technically, these laws make f and fmap together an endofunctor on Hask, the category of Haskell types (ignoring ⊥, which is a party pooper). See Wikibook: Category theory.

Even though a map between two different programming languages is a fascinating idea, we're more interested in a map where C and D are the same (the TS category). In that case we're talking about endofunctors (from the greek "endo" meaning "inside", "internal").

即便我們將範疇論內的概念與程式做對比，依然不能將範疇論的 Functor 以及語言中定義的 Functor 劃上等號。範疇論有的語言不一定能做到，語言裡有的範疇論不一定有 (大部分的語言並不可能寫出命題，所以範疇論的限制語言裡不一定有加上，這之間的一些漏洞就會產生對使用者來說可能很奇怪的結果)，我們能做的就是將兩者之間重疊的部份做連結。而 Haskell 是透過 Typeclass 來做約束，所以在程式語言的語境下所說的 Functor 是指 type class 的定義。另外，我們常說「Maybe 是一個 Functor」 指的是 Maybe 是 Functor class 的一個實例 (Maybe 可替換任何其他 Functor class 實例)。

其他 FP 語言雖然不一定都使用 Typeclass 這個詞，但大多 Functor 的定義都差不多。

Haskell

class Functor f where
  fmap :: (a -> b) -> f a -> f b

  (<$) :: a        -> f b -> f a
  (<$) = fmap . const 

Scala

trait Functor[F[_]] {
  def map[A,B](a: F[A])(f: A => B): F[B]
}

Lean

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α :=
    Function.comp map (Function.const _)

Functor laws

Functor class 的實例通過語言的檢查，都被視為語言中的 Functor，然而因為不能施加限制的關係，這些實例並不總是範疇論中的 Functor，所以必須檢查 Functor laws 才會是範疇論中的 Functor。

$$ fmap\ id = id $$

$$ fmap\ (g\circ f) = fmap\ g \circ fmap\ f $$

[dannypsnl]

話說 haskell 跟 lean 的 mapConst 應該可以拿掉沒差，因為那個不需要也不應該被使用者蓋掉。

[dannypsnl]

應該可以先發個 PR 了

[dannypsnl]

merged