Variant vs GADT approach

Question

In OCaml, I want to define a function f that accepts an input to update a record x. Among the following two approaches, I'm interested whether one has an advantage over the other (readability aside).

Variant approach

type input =
  | A of int
  | B of string

let f x = function
  | A a -> { x with a }
  | B b -> { x with b }

GADT approach

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 pros:

• Straightforward, no need for type annotations or anything fancy
• Writing a function of type string -> input is straightforward.

GADT pros:

• Avoid one layer of boxing.
  However, this is completely negated if you need a parsing functions, which would force you to pack things under an existential.

---

To be more precise, the GADT version can be seen as a decomposition of the ADT version. You can transform one into the other in a systematic way, and the memory layout will be similar (with the help of a small annotation):

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