Как рекурсивные типы без листовых случаев могут быть приняты в OCaml? - PullRequest
Новая
       63

Как рекурсивные типы без листовых случаев могут быть приняты в OCaml?

1 голос
/ 03 мая 2020

Общеизвестно, что OCaml отказывается определять голые рекурсивные типы, такие как type t = t -> int и пример Y-комбинатора в Rosetta Code также не работают.

Однако недавно я обнаружил, что небольшая настройка рекурсивного определения типа, например type t = A of (t -> int), работает хорошо. Следующий код представляет собой несколько проверочных концепций для проверки того, какой из них работает хорошо. 

(* OCaml version 4.08.0 *)
(* Precisely, ocaml-base-compiler.4.08.0 *)

# type t = t -> int;;
Error: The type abbreviation t is cyclic

# type t = int -> t;;
Error: The type abbreviation t is cyclic


# type t1 = A of (int -> t1);;
type t1 = A of (int -> t1)

# let v1 = 
    let rec f _ = A f in
    A f;;
val v1 : t1 = A <fun>


# type t2 = B of (t2 -> int);;
type t2 = B of (t2 -> int)

# let v2 =
    let g _ = 3 in
    B g;;
val v2 : t2 = B <fun>


# type t3 = C of (t3 -> t3);;
type t3 = C of (t3 -> t3)

# let v3 = 
    let rec h _ = C h in
    C h;;
val v3 : t3 = C <fun>

Я знаю, что тип может рекурсивно появляться для определения типов данных алгебраического типа c, таких как list или * 1011. * типа, но все они имеют конечные варианты, такие как NIL или LEAF конструктор. Ни у t1, t2, t3 нет конечных случаев, но они не отклоняются.

Я понятия не имею, как понять, как система типов OCaml допускает такие типы определений типов. Не могли бы вы объяснить, почему принимаются типы t1, t2, t3 и как интерпретировать значение значений v1, v2 и v3? Есть ли практическое применение для рекурсивных типов, у которых нет листовых случаев?

1 Ответ

2 голосов
/ 03 мая 2020

Ранние версии OCaml с радостью приняли такие типы, как type t = t -> int. Они даже выводили их. Проблема в том, что в большинстве практических случаев такой тип просто маскирует ошибку программирования. Таким образом, по многочисленным просьбам они были запрещены, и теперь вам нужен явный тип данных. Вы все еще можете получить старое поведение, если используете опцию -rectypes с компилятором.

Это было просто прагматическое решение c. С такими типами нет проблемы semanti c, по крайней мере, не в таком языке, как OCaml.

Типы данных не обязательно должны иметь нерекурсивные конструкторы в качестве «конечных» случаев, если только тип по крайней мере один конструктор содержит значения, для которых не требуется другое значение определенного типа.

Например, 

type 'a list1 = List1 of 'a * 'a list1 option

- это возможный тип для представления непустых списков. Это работает, потому что оно включает List1 (x, None) в качестве нерекурсивного значения.

Функции являются аналогичным примером в этом смысле.

...