Гетерогенный список ГАДТ в ocaml

Question

Я хотел бы создать гетерогенный список выражений, используя канонический пример для GADT.

Даны следующие виды:

type _ value =
| Bool : bool -> bool value
| Int : int -> int value

type _ expr =
| Value : 'a value -> 'a expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
| Eq : 'a expr * 'a expr -> bool expr
| Lt : int expr * int expr -> bool expr

Я пытался создать следующий список:

 let a = [Value (Bool true); Value (Int 1);]

Кажется, что это невозможно, так как он возвращает следующее сообщение об ошибке:

Error: This expression has type int value
       but an expression was expected of type bool value
       Type int is not compatible with type bool

Есть ли способ сделать это?

Я посмотрел документацию по ocaml для GADT и не смог найти или понять, как это сделать.

Может ли кто-нибудь указать мне на то, что объясняет, почему вы не можете делать с GADT все, что вы можете делать с ADT?

Answer 1

Одним из решений будет сделать:

type any_expr = Any:'a expr -> any_expr
let a = [Any (Value (Bool true)); Any (Value (Int 1));]

но я не понимаю, почему это работает или почему это требуется. Так что, если у кого-то есть чтение, чтобы предложить, я все еще заинтересован.

Итак, я обнаружил, что это дубликат, и ключевое слово:

existential wrapper