试着不精确地讲讲看 ... 首先是 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 ※ 编辑: xcycl 来自: 82.36.219.50 (08/12 06:57)