ocaml - 变体与 GADT 方法

Question

在 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 }

Answer 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