※ 引述《jaiyalas (ZZZ)》之铭言： : 据说,这个版的版主之前有尝试过以这样的方式来实做 : 也许可以请版主大人稍微讲一下实做的心得 = =+ 嗯，我是证人。 因为看不懂所以很快放弃了... XD : Haskell(GHC-6.6.1) : 最一开始使用的语言 : 不过因为他对於dependent type的支援不是很好 : ( 虽说好像有GADT,但是我不太知道那是什麽 : 也许哪个高手可以帮我补充一下,囧> ) : 没试几次以後就转向其他语言了 GADT 是 Generalized Algebraic Datatype. 不过要解释 generalized XYZ, 就得要先解释 XYZ... 所以... 等到有 观众要求再说好了... Haskell 其实还是没有要做 dependent type 的意思。 有人说 Haskell 近几年（包括加入 GADT、日後可能有的type family 等等）的一连串扩充尝试是往 dependent type 靠近 的过程。但对於跨出这最後几步，Haskell 似乎还是蛮迟疑的。 毕竟大家对该怎麽做 dependent type 还是没个共识，而且 有了它之後，程式的风貌可能改很多，这也是大家所陌生的。 Dependent type 听说倒是在 proof assistants 之中常用到。 GADT 好像就是学来的。 : Omega http://web.cecs.pdx.edu/~sheard/Omega/index.html : 没有试过,只有看过程式码 : 感觉语法和Haskell很像 : Epigram http://www.e-pig.org/ : 据说有比较完整的dependent type : 也是我试最久却最让人动怒的东西.. : 编辑上,实在是不太好用 : 与其说是个editor,还不如说是一个"填空软体" 哈哈哈... 其实如果 implement 得好，这是设计者 Conor McBride 心目中理想的 程式环境。你由定义 datatype 开始，然後 IDE 帮你找那个 datatype 的 induction 规则是什麽，程式会长什麽样子，同时也确保程式会终止。 你就填空就可以了。 （但我的感觉是，这跟 structure editor 不好用的原因一样。它假设 programmer 写程式都很有条理、很有结构。但我写程式都是涂涂抹抹的。） 不过 epigram 只有他自己一个人在写。听说是关在房间里面几个月什麽 别的事情都不怎麽做... 因为只有一个人所以他选用他比较容易做出原型 的方式：写成 emacs mode. 所以就变成这副模样了。 现在他正从 epigram 得到的许多经验去构思 epigram 2. 听说人手比较 多了，希望可以有人帮忙把这个界面的使用者经验弄得好一点... : 语言本身,实在是.. : 难以形容的诡异.. 嗯，这是一个有二度空间语法的语言. 用 - 和 | 等等符号画格子。 我很难想像它的 parser 怎麽写的。 : 他另外有一个compiler : 但是难用程度不下於那个editor 好像真的很怒.. 辛苦啦.. : Agda2 http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php : 现在才要开始尝试的东西 : 希望会比Epigram好用很多 Orz 我想至少是会比较习惯啦... BTW, Agda 本来也是在 proof assistant 里面用的语言。 * * * 另外，还可以提一下越来越红的 proof assistant: Coq. http://coq.inria.fr/ 基本概念上 Coq 也是用 Curry-Howard isomorphism 帮你做证明： 一个 type 就是一个 proposition, 如果找得到一个有这种 type 的 term, 就是找到了一个该 proposition 的证明。为了描述更多 想描述的 proposition, 使用 dependent type 就是蛮自然的事情。 Coq 等等 proof assistant 的使用经验是使用者一直去和系统对话。 当写好一个证明（写出一个 term）之後，Coq 可以 extract 出一个 OCaml 程式给你。（Coq 本身也是用 OCaml 写的。Agda 则是 Haskell. 设计者的偏好也反应在这两个语言的语法上... ） Agda 的 Emacs mode 也有一点对话的感觉，但已经比较像程式设计 而不是定理证明。Epigram 是这种互动程式设计的新尝试。 像 Omega 的做法则是老 programmer 对新 tool 的抗拒 -- 回到 老方法去，死也不改。 :) : 有哪位高手可以提供一点锻链自己逻辑能力的方法.. : 最近觉得自己逻辑没有学好 : 很多证明的东西常常没法很快转过来 欸... 很多 computer scientist (指自己) 其实只会一种证明方法: 归纳法。大概多看多做就会了吧....? --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 140.109.20.217