Подтвердить что ты не робот

Почему OCaml иногда требует расширения eta?

Если у меня есть следующая функция OCaml:

let myFun = CCVector.map ((+) 1);;

Он отлично работает в Utop, и Merlin не отмечает его как ошибку компиляции. Однако, когда я пытаюсь скомпилировать его, я получаю следующую ошибку:

Ошибка: тип этого выражения,       (int, '_a) CCVector.t → (int,' _b) CCVector.t,      содержит переменные типа, которые не могут быть обобщены

Если я eta-expand, однако, он компилируется отлично:

let myFun foo = CCVector.map ((+) 1) foo;;

Итак, мне было интересно, почему он не компилируется в eta-приведенной форме, а также почему эта-уменьшенная форма, похоже, работает в toplevel (Utop), но не при компиляции?

О, и документация для CCVector здесь. Часть "_a" может быть либо "RO", либо "RW", в зависимости от того, доступна ли она только для чтения или изменена.

4b9b3361

ОТВЕТЫ

Ответ 1

То, что вы получили здесь, - это ограничение полиморфизма ценности семейства языков ML.

Цель ограничения состоит в том, чтобы уладить let-polymorphism и побочные эффекты вместе. Например, в следующем определении:

let r = ref None

r не может иметь полиморфный тип 'a option ref. В противном случае:

let () =
  r := Some 1;       (* use r as int option ref *)
  match !r with
  | Some s -> print_string s  (* this time, use r as a different type, string option ref *)
  | None -> ()

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

Чтобы устранить эту проблему, многие исследования были выполнены в 80-х годах, и одним из них является полиморфизм ценности. Он ограничивает полиморфизм только для привязки, форма определения которого "нерасширяется". Eta расширенная форма не является экспансивной, поэтому ваша расширенная версия myFun имеет полиморфный тип, но не для eta уменьшенной. (Точнее говоря, OCaml использует смягченную версию этого полиморфизма значений, но история в основном такая же.)

Когда определение let binding является экспансивным, не вводится полиморфизм, поэтому переменные типа остаются не обобщенными. Эти типы печатаются как '_a в верхнем лепестке, и их интуитивное значение: они должны быть приведены к конкретному типу позже:

# let r = ref None                           (* expansive *)
val r : '_a option ref = {contents = None}   (* no polymorphism is allowed *)
                                             (* type checker does not reject this,
                                                hoping '_a is instantiated later. *)

Мы можем исправить тип '_a после определения:

# r := Some 1;;                              (* fixing '_a to int *)
- : unit = ()
# r;;
- : int option ref = {contents = Some 1}     (* Now '_a is unified with int *)

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

Эта задержка ввода допускается до конца набора компиляции. Топлел - это единица, которая никогда не заканчивается, и поэтому вы можете иметь значения с переменными типа '_a в любом месте сеанса. Но в разделенной компиляции переменные '_a должны быть созданы экземпляром какого-либо типа без переменных типа до конца файла ml:

(* test.ml *)
let r = ref None (* r : '_a option ref *)
(* end of test.ml. Typing fails due to the non generalizable type variable remains. *)

Это то, что происходит с вашей функцией myFun с компилятором.

AFAIK, нет идеального решения проблемы полиморфизма и побочных эффектов. Как и другие решения, ограничение полиморфизма значения имеет свой собственный недостаток: если вы хотите иметь полиморфное значение, вы должны сделать определение нерасширяющим: вы должны eta-expand myFun. Это немного паршиво, но считается приемлемым.

Вы можете прочитать некоторые другие ответы: