程式中的 Polymorphism 與範疇論 morphism

[FizzyElt]

主要希望釐清兩者之間的不同與關係

https://cs.stackexchange.com/questions/120216/why-are-all-polymorphic-functions-between-functors-natural-transformations
https://bartoszmilewski.com/2015/04/07/natural-transformations

[dannypsnl]

差異太大好像沒什麼好比的欸？最多就多型是 B 範疇裡面的一個 morphism 吧？

這是假設 B 是型別的範疇而 B-indexed category 是整個語言的範疇的語義

[FizzyElt]

倒也不是想比較 😃 ，只是想知道 polymorphism 起到了什麼作用

[dannypsnl]

那就是這兩個概念沒辦法放在一起比較

polymorphism 你可以暫時想成「type level application」，反正原則上也不算錯

[dannypsnl]

這個主題講起來很複雜，要從 signature $\Sigma$ 開始，然後加上 classifying category (term model) $Cl(\Sigma)$

然後加上等式理論 $\mathcal{A}$ 得到 $Cl(\Sigma, \mathcal{A})$，是 $Cl(\Sigma)$ 滿足 $\mathcal{A}$ 的子範疇。加上 Model 是 $Cl(\Sigma) \to B$ 的 functor，接下來才是 polymorphism 需要的 $B$-indexed 概念

到這裡就差不多需要學 topos 了

接到 natural model 的部分我也還沒看

[dannypsnl]

簡單來說我覺得這需要拆成好幾個部分