types - 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 的语言，具有依赖类型。

score 12 · Accepted Answer

参考链接是 Oleg 的轻量级静态保证页面，其中包含 ML 语言中使用的类依赖技术的示例（在 OCaml 中或您可以翻译为 OCaml）。他在 2007 年与 Chung- jieh Shan 合作的关于轻量级静态能力 (PDF)的论文尤其具有相关性。

编辑：自 4.00 版（在编写上述文档后发布）以来，OCaml 具有 GADT，它允许简化一些技术以优化静态信息（以前依赖于幻像类型技术），特别是Omega中演示的“单例类型”模式. 已经表明，它们对于获得强大的类型化编程并不是必不可少的，但它们仍可能被广泛使用的各种示例所使用。

1 回答 1