在 OCaml 中演示 GADT 的具体简单示例？

An concrete simple example to demonstrate GADT in OCaml?

我在 OCaml 中搜索了 GADT 的概念，为什么我们需要它以及何时使用它等

我了解 GADT 不仅在 OCaml 中，而且是一个更通用的术语。

我找到了

What are GADTs?

http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85

http://www.reddit.com/r/ocaml/comments/1jmjwf/explain_me_gadts_like_im_5_or_like_im_an/

等，但有的在Haskell里面，有的在no GADT和GADT[=之间没有很好的对比例子35=].

所以我想要的是一个简单但很好的具体示例，我可以在其中查看如果没有 GADT，情况会很糟糕。

可以给我吗？

我也在寻找 GADT 的良好应用，因为大多数时候，当我迟早使用它们时，我发现没有它们也可以完成同样的工作，而且通常更干净方法。所以，这不是一个完整的调查，只是我自己的一点经验。

  1. 普世价值观，也就是存在主义。它们允许您创建异构容器和类型安全序列化。请参见 Core 的 Univ 和 Univ_map 模块的示例。

  2. 语法树的类型安全求值器。此处 GADT 可用于删除一些运行时检查。

  3. 纯粹且类型安全的 Printf implementation，它已经是 OCaml 的一部分，也使用 GADT

    4. 重写了

这里是关于如何使用 GADT 的真实生活 example。在示例中，我使用 GADT 来指定 table 关系，例如 one_to_one、one_to_many 等。根据使用的关系，相应地推断函数类型。例如，one_to_maybe_one 关系，returns 函数 'a -> 'b option，one_to_many 创建具有 'a -> 'b list 的函数。同样可以通过创建几个不同的函数来实现，比如 link_one_to_one、link_one_to_many 等，而不是一个函数 link ~one_to:relation。因此，可以认为这种方法是有争议的。

GADT 之所以有用，有两个原因。

第一个（也是最常见的一个）是关于动态类型的：您可以添加一些动态类型而不丢失对它的静态检查。虽然这并不简单，但您可以通过它确定您的类型条件将得到满足。 ocaml manual 中给出了最简单的示例。 例如，这在标准库中用于以类型安全的方式重写 printf（在此之前，它是一个非常可怕的 Obj.magic）

集合

您可能想要使用 GADT 的第二个原因是当您想要在类型结构上维护一些复杂的不变量时。但这很难表达，而且您通常需要付出很多努力才能做到这一点。 好吧，我没有任何方便的例子，但我曾经看到一个朋友写下了一个 AVL 树的实现，它被类型系统证明平衡是正确的，这很酷。

要了解更多 GADT 功能及其良好用例，您可以阅读 Mads Hartmann 的相当不错的 blog post。