Почему перед этим типом есть знак плюса?

Ответ 1

Чтобы основать на Джеффри ответ, причина, по которой разработчики выполнили работу по маркировке абстрактного типа как ковариантного здесь, скорее всего, не поможет вам использовать подтипирование (по сути, никто не использует подтипирование в OCaml, поскольку параметрический полиморфизм в целом предпочтителен), но использовать еще менее известный аспект системы типов, называемый "ослабленным ограничением стоимости", благодаря чему ковариантные абстрактные типы допускают больший полиморфизм.

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

Мы обсуждали этот в reddit/ocaml несколько месяцев назад:

Рассмотрим следующий пример кода:

module type S = sig
  type 'a collection
  val empty : unit -> 'a collection
end

module C : S = struct
  type 'a collection =
    | Nil
    | Cons of 'a * 'a collection
  let empty () = Nil
end

let test = C.empty ()

Тип, который вы получаете для test, есть '_a C.collection, а не 'a C.collection, который вы ожидаете. Это не полиморфный тип ('_a - это мономорфная переменная вывода, которая еще не полностью определена), и вы не будете в восторге от этого в большинстве случаев.

Это потому, что C.empty () не является значением, поэтому его тип не обобщен (~ сделан полиморфным). Чтобы воспользоваться ослабленным ограничением стоимости, вы должны отметить абстрактный тип 'a collection covariant:

module type S = sig
  type +'a collection
  val empty : unit -> 'a collection
end

Конечно, это происходит только потому, что модуль C запечатан сигнатурой S: module C : S = .... Если модулю C не была дана явная подпись, система типов вывела бы самую общую дисперсию (здесь ковариация), и никто бы этого не заметил.

Программирование на абстрактном интерфейсе часто полезно (при определении функтора или приведении в соответствие дисциплины типа phantom или написании модульных программ), поэтому такая ситуация определенно происходит, и тогда полезно знать о ослабленном ограничении стоимости.

Если вы хотите понять теорию, ограничение стоимости и ее расслабление обсуждаются в статье исследования 2004 года Рассматривая ограничение стоимости от Jacques Garrigue, чьи первые несколько страниц представляют собой довольно интересное и доступное введение в тему и основную идею.

Ответ 2

Это означает, что тип является ковариантным по отношению к типу модуля. Предположим, у вас есть две карты, ключи которых одного типа. Этот + говорит, что если значения одной карты A являются подтипом значений другого отображения B, то общий тип отображения A является подтипом типа B типа. Я нашел довольно хорошее описание этого в блоге