变体与 GADT 方法

Posted 2023-02-16

【中文标题】变体与 GADT 方法

【英文标题】：Variant vs GADT approach

【发布时间】：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 

【问题讨论】：

变体方法在实现和使用方面具有简单、直接和易于理解的巨大优势。然而，GADT 方法可以部分应用于 input 类型，而无需提供值，但这只是您真正需要的优势。此类问题的答案几乎总是在很大程度上取决于上下文，因为几乎总是需要权衡取舍。如果没有，就不需要这个不太有利的功能。

谢谢，我以为是这样。可能应该将我的问题表述为“各有利弊”。除了解析数据结构之外，识别 GADT 的用例有点麻烦。

【参考方案1】：

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 x

【讨论】：

在内存表示中装箱？

那个符号对我来说是新的 :) [@@ocaml.unboxed] 是一个类型约束，表明 deppair 不能与存在值一起使用吗？

一点也不，它是一个注解，向编译器指示应该优化内存表示。见caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec260

为了澄清这里使用的术语，是type deppair 包装了主要的gadt 类型，这里是存在的吗？这也是使用 GADT 时的一般模式，即总是必须在“存在”中包装/解开一个 gadt 以模拟正常的 ADT 功能？

@Drup GADT 表示为带有包含作为字段的参数的标记的块。就像 ADT 一样。那么你说哪里少了一层拳击呢？实际上，在您的代码中，ADT 是一个带有标签和一个字段的块，而 Pair 是一个带有标签和两对的块。这不是在浪费内存吗？

【参考方案2】：

正如您所注意到的，GADT 的（非）可读性是一个很大的缺点。尽可能避免使用 GADT。更容易打字，更容易阅读。也不太复杂的错误消息。

在运行时简化它们是相同的。它们表示为带有标签和字段的简单整数或块，代码使用标签进行匹配和分支。所以两者都不会给你带来优势。

在编译时 GADT 更强大，因为编译器可以以 ADT 不允许的方式检查类型。一个示例是存在类型，例如另一个答案中的示例。因此，当您无法使用 ADT 时，请使用 GADT。