Сочетание параметрического полиморфизма и полиморфных вариантов (типы обратных кавычек)

Question

Предположим, у меня есть тип, состоящий из нескольких (ковариантно) полиморфных вариантов, например следующих:

[> `Ok of int | `Error of string]

Далее предположим, что я хочу разложить это определение на какой-то конструктор типа и конкретный тип. int. Моя первая попытка была следующей:

type 'a error = [> `Ok of 'a | `Error of string]

Однако использование такого определения вызывает действительно странную ошибку типа с упоминанием переменной типа 'b это нигде не фигурирует в определении.

$ ocaml
        OCaml version 4.07.0

# type 'a error = [> `Ok of 'a | `Error of string ];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound

Этот 'b является автоматически сгенерированным именем, добавляя явное 'b сдвигает переменную на 'c.

$ ocaml
        OCaml version 4.07.0

# type ('a, 'b) error = [> `Ok of 'a | `Error of 'b ];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of 'b | `Ok of 'a ] as 'c the variable 'c is unbound

Используя инвариантную конструкцию [ `Thing1 of type1 | `Thing2 of type 2 ] кажется, отлично работает в этом контексте.

$ ocaml
        OCaml version 4.07.0

# type 'a error = [ `Ok of 'a | `Error of string ] ;;
type 'a error = [ `Error of string | `Ok of 'a ]
#

Однако явная пометка параметра типа как ковариантного не спасает исходный пример.

$ ocaml
        OCaml version 4.07.0

# type +'a error = [> `Ok of 'a | `Error of string];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound

И, на всякий случай, добавление аннотации контравариантности также не работает.

$ ocaml
        OCaml version 4.07.0

# type -'a error = [> `Ok of 'a | `Error of string];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound

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

$ ocaml
        OCaml version 4.07.0

# type ('a, 'b) string = [> `Ok of 'a | `Error of string] ;;
Error: The type constructor string expects 2 argument(s),
       but is here applied to 0 argument(s)

Есть ли способ создать конструктор типа, который может эффективно "заменять различные типы" на int в [> `Ok of int | `Error of string]?

Answer 1

Это не проблема дисперсии или параметрического полиморфизма, а проблема полиморфизма строк. Когда вы добавляете> или <он также добавляет переменную неявного типа, переменную строки, которая будет содержать "полный" тип. Вы можете увидеть, что эта переменная типа явно указана в ошибке:

[> `Error of string | `Ok of 'a ] as 'b

Обратите внимание as 'b часть в конце.

Чтобы задать псевдоним типа, вы должны сделать переменную типа явной, чтобы вы могли ссылаться на нее как на параметр типа в псевдониме:

type ('a, 'r) error = [> `Ok of 'a | `Error of string ] as 'r

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

type 'r obj = < foo: int; .. > as 'r