Oll*_*edt 7 ocaml types coq metaocaml
在OCaml邮件列表上窃听人们之前,我想我可能会在这里发布我的问题.我刚发现这个美女(链接到Concoqtion网站).Concoqtion是MetaOCaml的扩展,它允许索引类型(可能还有更多).有了它,很容易创建列表,其中包括列表的长度:
type ('n:'(nat),'a) listl =
| Nil : ('(0),'a) listl
| Cons of let 'm:'(nat) in 'a * ('(m),'a) listl : ('(m+1),'a) listl
这(m+1)是在类型级别完成的.井井有条.
但是,最后一个版本是2007年(OCaml 3.08).有谁知道为什么这个项目被取消,或者今天OCaml有类似的东西？
gas*_*che 14
在计算机科学研究期间编写的大多数软件都是一个原型,它没有比制作文章的科学观点所需要的更多,验证了你的方法.一些例外最终会被维持很长一段时间并过着复杂的生活,成为人们所依赖的东西(OCaml就是这样一个例子),但这既是一种祝福,也是一种诅咒.
我从未想过Concoqtion是为了立即采用,而是作为一个概念证明,你可以整合编程并证明"现在!".从"采用"的角度来看,MetaOcaml已经是在OCaml上添加的一个很少使用的补丁,在混合中加入Coq(不是轻量级的,也不是用于嵌入)会给你一个相当脆弱的系统的合理承诺.地狱要坚持很久.
我不会说Concoqtion被"放弃",而不是教给我们一个教训,但并不意味着实际使用.研究人员一直在该领域工作,许多系统可以被描述为这项工作的后代(或至少重用一些想法),例如VeriML.
当然,我说这是一个局外人.很难猜出作者的意图是什么.此外,研究界的原型/产品往往存在模糊关系:你通常认为没有人会采用你的实验软件,但也许,某些人实际上可能会有一点希望.作者本身对于他们是否打算将其开发作为一个抛弃原型,或者积极期望用户参与而言通常是相当矛盾的(你通常不会写"我们故意偷工减料并且黑客攻击丑陋以使其在"在您的论文或您的网页上"的论文的几个例子.有些人设计的是非常可靠的软件,但是从未被采用过(对Alice ML来说),有些人会开发出被其他人使用的片状原型(没有例子),你永远不会知道.