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

Question

Я просматривал стандартную библиотеку ocaml и наткнулся на этот код в файле map.ml.

module type S =
  sig
    type key
    type +'a t
    val empty: 'a t'

Мне интересно, почему есть type +'a tи почему автор использует его, а не просто 'a t,
Его поведение странно, и я не могу вывести его использование.

# type +'a t = 'a list;;
type 'a t = 'a list
# type +'a t = +'a list;;
Characters 13-14:
  type +'a t = +'a list;;
               ^
Error: Syntax error

Спасибо

Answer 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 ковариантны:

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

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

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

Если вы хотите понять теорию, ограничение значения и его ослабление обсуждаются в исследовательской статье 2004 года "Ослабление ограничения значения" Жака Гаррига, первые несколько страниц которого являются довольно интересным и доступным введением в тему и основную идею.

Answer 2

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