四连发 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