问题 OCaml中的依赖类型


关于Haskell和Scala中的依赖类型有很多信息。对于OCaml,不是那么多。是否有足够的技术人员提供有关如何在OCaml中实现此目的的编码示例(如果可能的话)?当然(被遗弃的) 依赖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式语言,具有相关时间。


10659
2018-03-28 23:18


起源

请问这个“关于Haskell和Scala中依赖类型的大量信息”在哪里?尽管对Haskell社区有一个合理的概述,但我不知道你指的是什么。 (我肯定会考虑UPenn的工作 依赖类型的Haskell 虽然相关,但这是非常研究而不是实际,并且可能不是“很多”的数量。我不知道你对Scala的想法 - 除了与路径依赖类型的关系? - gasche
嗯,在stackoverflow上,我在想。也许我被Scalas路径依赖类型所欺骗。 - Olle Härstedt


答案:


参考链接是Oleg的 轻量级依赖打字 页面,包含ML语言中使用的依赖类技术的示例(在OCaml中或您可以转换为OCaml)。他的论文 轻量级静态功能(PDF) 与2007年的Chung-chieh Shan特别相关。

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


12
2018-03-29 05:50