types - OCaml 中的依赖类型

Question

Haskell 和 Scala 中有很多关于依赖类型的信息。对于 OCaml，不是那么多。有没有足够熟练的人提供一个关于如何在 OCaml 中实现这一点的编码示例(如果可能的话)？当然有(废弃的)Dependent ML ，但似乎不可能在“常规” OCaml 代码中合并这些东西。

基本上，我想要做的是删除像 assert(n > 0) 这样的代码并在编译时检查它。

编辑

作为旁注，值得一提的是 OCaml Hybrid Contract Checking分支，这可以满足依赖类型系统的一些需求。而不是 assert(n > 0)然后你会写一个契约(Contract):

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 的 lightweight dependent typing 页面，其中包含 ML 语言中使用的类似相关技术的示例(在 OCaml 中或您可以转换为 OCaml)。他在 2007 年与 Chung-chieh Shan 的关于 Lighweight static capabilities (PDF) 的论文尤其相关。

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