Re: [心得] 今天收到的挑戰，也上來問問大家

看板PLT (程式語言與理論)作者xcycl (XOO)時間14年前 (2010/08/12 02:05)推噓1(1推 0噓 2→)

留言3則, 3人參與討論串2/2 (看更多)

試著不精確地講講看 ... 首先是 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