变式与GADT方法
变式与GADT方法
提问于 2018-02-20 11:22:11
在OCaml中，我想要定义一个函数f，它接受input来更新记录x。在以下两种方法中，我感兴趣的是一种方法是否比另一种方法更有优势(撇开可读性不说)。
变体方法
type input =
| A of int
| B of string
let f x = function
| A a -> { x with a }
| B b -> { x with b }GADT方法
type _ input =
| A : int input
| B : string input
let f (type t) x (i: t input) (v: t) =
match i with
| A -> { x with a = v }
| B -> { x with b = v }回答 2
Stack Overflow用户
回答已采纳
发布于 2018-02-20 12:01:57
ADT的优点：
- 简单明了，不需要类型注释或任何花哨的东西。
- 编写
string -> input类型的函数很简单。
GADT的优点：
- 避免一层拳击。 但是，如果您需要一个解析函数，这是完全否定的，这将迫使您将事情打包到一个存在主义下。
更准确地说，GADT版本可以看作是ADT版本的分解。您可以以系统的方式将其中一个转换为另一个，并且内存布局将是相似的(借助一个小型注释)：
type a and b and c
type sum =
| A of a
| B of b
| C of c
type _ tag =
| A : a tag
| B : b tag
| C : c tag
type deppair = Pair : ('a tag * 'a) -> deppair [@@ocaml.unboxed]
let pack (type x) (tag : x tag) (x : x) = Pair (tag, x)
let to_sum (Pair (tag, v)) : sum = match tag with
| A -> A v
| B -> B v
| C -> C v
let of_sum : sum -> deppair = function
| A x -> pack A x
| B x -> pack B x
| C x -> pack C xStack Overflow用户
发布于 2018-02-20 16:42:03
正如您注意到的，GADT的不可读性是一个很大的缺点。在可能的情况下尽量避免GADT。打字容易，阅读方便。不太复杂的错误信息。
在运行时简化，它们是相同的。它们被表示为带有标记和字段的简单ints或块，代码使用标记进行匹配和分支。所以这两种情况都没有给你优势。
在编译时，GADT更强大，因为编译器可以以ADT不允许的方式检查类型。一个例子是存在类型，如另一个答案中的示例。因此，当您不能使用ADT时使用GADT。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/48884180
复制相关文章
相似问题
腾讯云开发者
