OCaml, почему пустой массив имеет полиморфный тип?

Question

Массивы OCaml являются изменяемыми.Для большинства изменяемых типов даже «пустое» значение не имеет полиморфного типа.

Например,

# ref None;;
- : '_a option ref = {contents = None}
# Hashtbl.create 0;;
- : ('_a, '_b) Hashtbl.t = <abstr>

Однако пустой массив имеет полиморфный тип

# [||];;
- : 'a array = [||]

Похоже, что это невозможно, поскольку массивы являются изменяемыми.

В этом случае получается, что длина массива не может измениться и, следовательно, нет возможности нарушить целостность.

Есть ли специальные массивы в системе типов, чтобы это разрешалось?

Answer 1

Ответ прост - пустой массив имеет полиморфный тип, потому что он является константой.Это особый случай?Ну, в основном, потому что массив является встроенным типом, который не представлен как ADT, так что да, в typecore.ml в функции is_nonexpansive есть случай для массива

  | Texp_array [] -> true

Однако это не особый случай, это просто вопрос определения, какие синтаксические выражения образуют константы.

Обратите внимание, что в общем случае ослабленное ограничение значений позволяет обобщать выражения, не являющиеся экспансивными (а не только синтаксические константы, как в классическом ограничении значений).Где неэкспансионное выражение - это либо выражение в нормальной форме (т. Е. Константа), либо выражение, вычисление которого не будет иметь никаких наблюдаемых побочных эффектов.В нашем случае [||] является идеальной константой.

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

Кроме того, ref None не пустое значение.Значение ref само по себе является просто записью с одним изменяемым полем, type 'a ref = {mutable contents : 'a}, поэтому оно никогда не может быть пустым.Тот факт, что он содержит неизменяемое значение (или ссылается на неизменяемое значение, если хотите), не делает его ни пустым, ни полиморфным.Так же, как [|None|], он также не пустой.Это синглтон.Кроме того, последний имеет слабый полиморфный тип.

Answer 2

Я не верю в это.Подобные ситуации возникают с пользовательскими типами данных, и поведение такое же.

В качестве примера рассмотрим:

type 'a t = Empty | One of { mutable contents : 'a }

Как и в случае с массивом, 'a t является изменяемым.Однако конструктор Empty можно использовать полиморфно, как пустой массив:

# let n = Empty in n, n;;
- : 'a t * 'b t = (Empty, Empty)

# let o = One {contents = None};;
val o : '_weak1 option t = One {contents = None}

Это работает, даже если присутствует значение типа 'a, если оно нев неизменяемой позиции:

type 'a t = NonMut of 'a | Mut of { mutable contents : 'a }

# let n = NonMut None in n, n;;
- : 'a option t * 'b option t = (NonMut None, NonMut None)

Обратите внимание, что аргумент 'a t все еще не является вариативным, и вы потеряете полиморфизм при скрытии конструктора внутри функции или модуля (примерно потому, что дисперсия будет выведена из аргументовконструктор типа).

# (fun () -> Empty) ();;
- : '_weak1 t = Empty

Сравнить с пустым списком:

# (fun () -> []) ();;
- : 'a list = []