在对 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 是否有类似的东西？
在计算机科学研究期间编写的大多数软件都是一个原型，没有比提出文章的科学观点所需的更进一步，验证你的方法。有些例外最终会维持很长时间，过着复杂的生活，成为人们依赖的东西（OCaml 就是这样一个例子），但这既是福也是祸。
我从不认为 Concoqtion 意味着立即采用，而是作为概念证明，您可以集成编程和“现在！”证明。从“采用”的角度来看，MetaOcaml 已经是 OCaml 之上的一个很少使用的补丁，在混合中添加 Coq（不是轻量级的，也不是为嵌入而设计的）给你一个相当脆弱的系统的合理承诺，它将是地狱维持了很长时间。
我不会说 Concoqtion 被“抛弃”，而不是它给我们上了一课，但并不打算实际使用。研究人员一直在该领域工作，许多系统可以被描述为这项工作的后代（或至少重用一些想法），例如VeriML。
当然，我是作为一个局外人这么说的。很难猜出作者的意图是什么。此外，在研究圈中，原型/产品常常存在一种模棱两可的关系：您通常假设没有人会采用您的实验软件，但也许，也许有些人实际这样做的希望很小。对于他们是否打算将他们的开发作为一次性原型，或者积极期望用户参与其中，作者自己通常相当矛盾（你通常不会写“我们故意偷工减料并砍掉丑陋的狗屎，使其在论文的几个例子”在你的论文或你的网页上）。有些人设计了真正可靠的软件，但从未被采用（向Alice ML 致敬），有些人开发了被其他人使用的片状原型（没有例子），你永远不知道。