推 ogamenewbie:用五句話講完看來很難很難 08/12 02:39
※ 編輯: xcycl 來自: 82.36.219.50 (08/12 06:57)
→ xcycl:如果只單純實務上怎麼用，到沒什麼問題 08/12 09:55
→ jellyice:咦？不是五句話嗎？怎麼看起來好長… 11/11 23:06
試著不精確地講講看 ...
首先是 cateogry 上對照 type theory 是什麼呢？[2]
對 category 上每個 object A 考慮作 type A, 那麼
可以將 morphism f : A -> B 寫成
x : A |- f(x) : B
其中把 x 當作是 free variable of type A
在 category 下不是每個 object 都是 set, morphism 也不一定是 function,
例子是考慮 preorder 本身當作一個 category, a <= b 視作 a -> b。
（這個例子也很重要，因為 category 本身可看作 preorder 的範疇化結構[1][3]，
很多概念例如 colimit 跟 limit 可以看作是 sup 跟 inf，adjoint functor
可以看作 Galois correspondence，另一個是 homotopy category, 以
topological space 作為 object，連續函數的 homotopy classes 作為 morphisms,
被 Peter Freyd 證明不是 concrete category）
但是呢，我們還是可以把 x : A 看作是 A 的廣義元素，或是任何到 A 的 morphism。
這個概念來自於在 Set 底下，A 的元素可以看成跟 1 -> A 的morphism，其中
1 是只有一個元素的集合 {*}。
那麼 x : A |- f(x) : B 的意思，就變成說若有一個廣義元素 y : U -> A
函數的套上去之後，有 f o y : U -> A -> B = f(y) : U - B 。
那麼來到 morphism 的 composition, f : A -> B, g : B -> C 得到 A -> C呢？
寫作
x : A |- f(x) : B y : B |- g(y) : C
---------------------------------------------
x : A |- g o f (x) : C
單位元素則是講
-----------------
x : A |- x : A
我現在講的結構是最一般化的 category，他對應的 type theory 也相對簡單，
如果考慮 Cartesian closed category (CCC) ，對應的則會是 simple type theory。
則也是為甚麼如果只考慮 simple type theory ，我們可以用 Set 來給定語意，
因為 Set 是 CCC 。
其他的 type theory 跟 category theory 的關係可以看看 Bart Jacobs 的
Categorical Logic and Type Theory，雖然我只看了序章而已。
好了，以上這些都沒扯到 monad 只講到 category 跟 type theory
或說計算的 categorical model 而已。
那考慮 monad 進來是什麼呢？給定一個 monad <T, \eta, \mu>
我們先看 functor T ，照 E. Moggi 的話講 [4]，
既然 x : A 其中 x 看作是 type A, 那麼我們把
TA 看作是對 A 的概念上的計算或操作，例子在 Haskell 上很多，跳過不講。
若我們有 f : A -> B 從 type A 到 type B 的函數，
我們可以將 f 延伸至 TA 到 -> TB 上的函數，也就是 Tf。
呼，好長，我要拖稿，還是看誰來接力吧 ...
[1] http://unapologetic.wordpress.com/2007/06/27/categorification/
[2] http://ncatlab.org/nlab/show/type+theory
[3] http://ncatlab.org/nlab/show/categorification+-+contents
[4] E. Moggi, Notions of computation and monads, 1991
（咦？我沒用 Tex 就不會寫引用文獻了）
※ 引述《SansWord (是妳)》之銘言：
: 今天午餐有幸跟一群在中研院工作的人吃飯....
: 大多數人第一次見面，自我介紹是免不了的....
: 不過這樣的自我介紹可能不能介紹興趣喜好之類的東西....
: 要介紹我正在研究的東西....
: 然後，我就被challenge了:
: "請5句話解釋什麼是monad"
: 大家有什麼Idea嗎?
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 147.188.193.87