Re: [心得] Dependent Type "簡"介

看板PLT (程式語言與理論)作者godfat (godfat 真常)時間17年前 (2007/10/01 21:08)推噓0(0推 0噓 0→)

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

四連發 XD ※ 引述《noctem (noctem)》之銘言： : 嗯，我是證人。 : 因為看不懂所以很快放棄了... XD 其實我覺得比起證明這真是簡單多了|||b 不過由於 template 本來就不是設計來那樣玩的，所以有些地方寫起來會滿令人覺得彆扭又詭異... C++0x 這部份應該會有很大的補強，像是 template alias 就能減少很多複雜度 * : GADT 是 Generalized Algebraic Datatype. 不過要解釋 : generalized XYZ, 就得要先解釋 XYZ... 所以... 等到有 : 觀眾要求再說好了... 我也不太懂這是什麼 XDXD 不過不知道 template haskell 是什麼？有機會時試試看好了 * : （但我的感覺是，這跟 structure editor 不好用的原因一樣。它假設 : programmer 寫程式都很有條理、很有結構。但我寫程式都是塗塗抹抹的。）我也是，由結果去推過程，實在很方便啊 XD : 嗯，這是一個有二度空間語法的語言. 用 - 和 | 等等符號畫格子。 : 我很難想像它的 parser 怎麼寫的。既然他是自己一個人悶頭寫的，為什麼會選擇那麼恐怖的語法？光要處理那個介面應該就很花時間了吧...? 還是 emacs 本身有提供這種畫格子的 feature? XD * : 另外，還可以提一下越來越紅的 proof assistant: Coq. godfat ~ 3.2$ port info coq coq 8.1, lang/coq (Variants: universal) http://coq.inria.fr/ Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp4. For more information, see <http://coq.inria.fr/>. Build Dependencies: ocaml Maintainers: reilles@loria.fr 有時候（其實已經不是有時候了 XD）會覺得，macports 裡沒有的東西我不想灌 :D : 一個 type 就是一個 proposition, 如果找得到一個有這種 type : 的 term, 就是找到了一個該 proposition 的證明。為了描述更多 : 想描述的 proposition, 使用 dependent type 就是蠻自然的事情。證明對我來說真是個難以理解的步驟，本來用 type 去看能夠理解的事，如果用證明的說法來描述的話，我就常常要想很久也不見得能看出什麼。不知道是單純不習慣呢，還是這本來就是迥異的兩種思維方向...? : 像 Omega 的做法則是老 programmer 對新 tool 的抗拒 -- 回到 : 老方法去，死也不改。 :) 這還是我的習慣 XDXD 不喜歡寫的東西 dependent on 某個工具。越方便寫在紙上（or even speak perhaps XD）的我越喜歡 :p -- Hear me exalted spirits. Hear me, be you gods or devils, ye who hold dominion here: I am a wizard without a home. I am a wonderer seeking refuge. Sacrifice -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 220.135.28.18