我在OCaml中搜索过GADT的概念,我们为什么需要它以及何时使用它等等.
我知道GADT不仅仅是在OCaml中,而是一个更通用的术语.
我发现了
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中,而其他一些在没有GADT和GADT之间没有很好的比较例子.
所以我想要的是一个简单而又好的具体例子,我可以看到,如果没有GADT,事情就不好了.
我可以请那个吗？
GADT有两个原因.
第一个(也是最常见的一个)是关于动态类型:你可以添加一些动态类型,而不会丢失它的静态检查.但这并不简单,但你可以确定你的类型条件将得到满足.最简单的例子在ocaml手册中给出.这在标准库中用于以类型安全的方式重写printf(在此之前,它是一个非常可怕的Obj.magic集合)
您可能想要使用GADT的第二个原因是,您希望在类型结构上保留一些复杂的不变量.这很难表达,你经常需要付出很多努力才能做到这一点.好吧,我没有任何方便的例子,但我曾经看到一位朋友写下AVL树的实现,如果打字系统证明平衡是正确的,这很酷.
对于更多的GADT功能及其良好的使用案例,您可以阅读Mads Hartmann 撰写的相当不错的博客文章.
我也在寻找 GADT 的良好应用，因为大多数时候，当我迟早使用它们时，我发现，没有它们也可以完成同样的工作，而且通常以更简洁的方式完成。所以，这不是一个完整的调查，只是我自己的一点经验。
普世价值，又名存在主义。它们允许您创建异构容器和类型安全序列化。例如，请参阅核心Univ和Univ_map模块。
语法树的类型安全评估器。在这里，GADT 对于删除一些运行时检查很有用。
纯且类型安全的Printf 实现，已经是 OCaml 的一部分，也使用 GADT 进行了重写
以下是如何使用 GADT 的真实示例。在示例中，我使用 GADT 来指定表关系，例如one_to_one、one_to_many等。根据使用的关系，相应地推断函数类型。例如，one_to_maybe_one关系，返回一个函数'a -> 'b option，one_to_many用 创建一个函数'a -> 'b list。只需创建几个不同的函数（例如link_one_to_one、link_one_to_many等而不是一个函数 ）即可实现相同的效果link ~one_to:relation。因此，人们可以认为这种方法是有争议的。