OCaml中的依赖类型

有很多关于Haskell和Scala中依赖类型的信息。对于OCaml而言，并非如此。有没有人有足够的技巧来提供一个关于如何在OCaml中实现这一点的代码示例（如果可能的话）？当然，（放弃）Dependent ML，但似乎不可能将这些东西纳入“常规”OCaml代码。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 *)

来源

2013-03-28 Olle Härstedt

请问这是“关于Haskell和Scala中相关类型的大量信息”？尽管对Haskell社区进行了合理的概述，但我不知道你指的是什么。（我肯定会认为UPenn在[Dependently-Typed Haskell]（http://www.cis.upenn.edu/~sweirich/）上的工作是相关的，但这是极其研究而非实际的，可能不是“很多”体积）。我不知道你在为Scala想什么 - 除了可能与路径依赖类型的关系？ – gasche

Ehm，在stackoverflow上，我在想。也许我被斯卡拉路径依赖类型愚弄。 –

参考链接是Oleg的lightweight dependent typing页，实例（OCaml中或可以转化为OCaml的）的ML语言中使用依赖般的技术。他在2007年与Chung-chieh Shan在Lighweight static capabilities (PDF)上的论文尤其相关。编辑：从版本4.00（在编写上述文档之后发布）开始，OCaml具有GADT，它可以简化精炼静态信息（以前依赖于幻像类型技术）的一些技术，特别是“单例类型”模式在Omega中显示。已经表明，它们对于获得强有力的类型编程并不是必不可少的，但它们仍然可以被野外发现的各种示例所使用。

来源

2013-03-29 05:50:45 gasche

OCaml中的依赖类型

回答

相关问题