OCaml 中的依赖类型

Posted 2023-02-19

【中文标题】OCaml 中的依赖类型

【英文标题】：Dependent types in OCaml

【发布时间】：2013-03-19 14:23:02

【问题描述】：

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

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

编辑

作为旁注，值得一提的是 OCaml Hybrid Contract Checking 分支，它可以满足依赖类型系统的一些需求。然后，您将编写一份合同，而不是 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 的语言，具有依赖类型。

【问题讨论】：

请问“关于 Haskell 和 Scala 中依赖类型的大量信息”在哪里？尽管对 Haskell 社区有一个合理的概述，但我不知道您指的是什么。 （我肯定会认为 UPenn 在 Dependently-Typed Haskell 上的工作是相关的，但这是非常研究性的而不是实用的，而且数量上可能不是“很多”）。我不知道你对 Scala 有什么想法——除了与路径相关类型的关系？

嗯，在***上，我在想。也许我被 Scala 的路径依赖类型愚弄了。

【参考方案1】：

参考链接是 Oleg 的 lightweight static guarantees 页面，其中包含 ML 语言中使用的类似依赖技术的示例（在 OCaml 中或您可以翻译为 OCaml）。他在 2007 年与 Chung-jieh Shan 在Lighweight static capabilities (PDF) 上发表的论文尤其具有相关性。

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