OCaml中的依赖类型

Question

关于Haskell和Scala中的依赖类型有很多信息.对于OCaml,没有那么多.是否有足够的技术人员提供有关如何在OCaml中实现此目的的编码示例(如果可能的话)？当然(废弃的)Dependent ML,但似乎不可能将这些东西合并到"常规"OCaml代码中.

基本上,我想要做的是删除代码assert(n > 0),并在编译时检查它.

编辑

作为旁注,值得一提的是OCaml 混合合同检查分支,它可以满足依赖类型系统的一些需求.而不是assert(n > 0)你会写一份合同:

contract f = {x : x > 0} -> int
let f x = x + 1
let dummy_variable = f (-1) (* Won't compile *)

编辑2:对于读这篇文章的人来说,我认为F*是一种有趣的ML类语言,具有依赖类型.

Answer 1

参考链接是Oleg的轻量级依赖类型页面,其中包含ML语言中使用的依赖类技术的示例(在OCaml中或您可以转换为OCaml).他在2007年与Chung-chieh Shan 撰写的关于轻量级静态能力(PDF)的论文尤为重要.

编辑:从版本4.00(在上面的文档编写之后发布),OCaml有GADT,它允许精简一些技术以获得精细的静态信息(以前依赖于幻像类型技术),特别是Omega中演示的"单例类型"模式.已经证明,它们对于获得强大的类型编程并不是必不可少的,但它们仍然可以被野外发现的各种例子所使用.