Когда в OCaml создаются физически различные значения?

Я пытаюсь понять, что означают операторы физического равенства (Pervasives.(==) и Pervasives.(!=)) в OCaml.

В руководстве по языку сказано, что выражение "" является «константой», а не «выражением»:

6.5 Константы

константа :: == ... строковый литерал

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

(* a *)  ""          == "";;             (* false *)
(* b *)  "foo"       == "foo";;          (* false *)
(* c *)  ""          == String.copy "";; (* false *)
(* d *)  ()          == ();;             (* true  *)
(* e *)  (42, -42)   == (42, -42);;      (* false *)
(* f *)  ("", 1)     == ("", 1);;        (* false *)
(* g *)  None        == None;;           (* true  *)
(* h *)  (Some None) == (Some None);;    (* false *)

Раздел «19.3 Представление типов данных OCaml» предполагает, что спецификация языка требует, чтобы буллы, целые числа, символы, значение единицы, простые варианты и пустые списки были бескорыстными.

Должна ли реализация вести себя, как указано выше, чтобы соответствовать реализации OCaml?

Может ли соответствующая реализация OCaml переписать указатель на b, чтобы он указывал на a, когда a = b (* structurally *) истинно, и оба являются значениями неизменяемого типа (или фактически неизменяемыми значениями, такими как строки / массивы нулевой длины), как это иногда делается для уменьшения количества достижимых более молодых значений в генеральном GC?


person Mike Samuel    schedule 05.08.2012    source источник


Ответы (2)


Когда я читал спецификацию языка, было очень мало гарантий относительно того, когда значения различны. Я считаю, что единственная гарантия содержится в документации модуля Pervasives.:

Для изменяемых типов, таких как ссылки, массивы, строки, записи с изменяемыми полями и объекты с изменяемыми переменными экземпляра, e1 == e2 истинно тогда и только тогда, когда физическая модификация e1 также влияет на e2. В неизменяемых типах поведение (==) зависит от реализации; однако гарантируется, что e1 == e2 подразумевает compare e1 e2 = 0.

Одна из замечательных особенностей FP заключается в том, что компилятор и среда выполнения могут делать произвольные умные вещи с неизменяемыми значениями. Так что эта гарантия - это все, что вы действительно хотели бы иметь (ИМХО).

В общем, да, среда выполнения или компилятор могут (опять же, ИМХО) делиться (а не делиться) неизменяемыми значениями любым способом, который, по его мнению, будет полезен.

Я бы не стал интерпретировать раздел представления как часть спецификации языка. Это просто полезная документация по текущей реализации.

person Jeffrey Scofield    schedule 05.08.2012
comment
Спасибо. Это дает хороший ответ на два вопроса: не существует эффективных неизменяемых значений, таких как массивы нулевой длины, а для неизменяемых значений разрешена оптимизация. Он не отвечает на вопрос, подразумевает ли для стабильных неизменяемых привязок a и b a != b во время T0 a != b во время T1 ›T0, как в примере оптимизации GC. - person Mike Samuel; 06.08.2012
comment
На самом деле, я думаю, что словоблудие о псевдонимах только в том случае, если физическая модификация действительно позволяет String.copy "" == "", поскольку невозможно наблюдать физическую модификацию экземпляра "". - person Mike Samuel; 06.08.2012

Просто замечание: строковые константы объединяются в пул иначе, чем то, что вы тестируете:

let f () = "foo"
let b = f () == f () (* true *)

Это действительно может привести к ошибкам, если вы измените вывод вызова f (): это также повлияет на все последующие вызовы. Консенсус в отношении такого поведения заключается в том, что изменяемая строка является исторической ошибкой (один должен иметь изменяемый тип буфера отличный от основного типа строки, для которого более важны варианты кодирования и сложность конкатенации) и что Пулы, нарушающие семантику, достаточно интересны с точки зрения производительности, чтобы можно было предположить, что строковые константы не изменяются. Если кто-то хочет избежать объединения, нужно просто вызвать String.copy непосредственно для строковой константы.

person gasche    schedule 13.08.2012