OCaml: пример использования Core.Univ

Question

Поэтому я смотрю на Core.Univ как на способ создания гетерогенных массивов.

Предположим, я делаю

let int_type = Core.Type_equal.Id.create ~name:"" Sexplib.Conv.sexp_of_int;;
let int_type' = Core.Type_equal.Id.create ~name:"" Sexplib.Conv.sexp_of_int;;

let i = Core_kernel.Univ.create int_type 5;;
let j = Core_kernel.Univ.create int_type' 5;;

Когда я делаю

Core_kernel.Univ.match_ i int_type'

Это не соответствует ожидаемому, так как документация для Type_equal.Id говорит, что два звонка create с точно такими же аргументами приведет к двум различным идентификаторам.

Означает ли это, что пользователь API отвечает за то, чтобы только один экземпляр Type_equal.Id существует для каждого типа?

Answer 1

Да. Я бы сказал, что терминология Core здесь немного неудачна.

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

Это означает, что нет способа проанализировать значения, возвращаемые Core.Type_equal.Id.create определить, к какому типу они относятся, и, следовательно, нет способа обнаружить, если вы уже вызвали create для существующего идентичного типа (который позволил бы вернуть уже созданный идентификатор).

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