四連發 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: [email protected]
有時候（其實已經不是有時候了 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