Почему мое определение типа отклоняется как циклическое, когда объявляется как вариант, но принимается иначе?

Question

Я возился с использованием OCaml, реализующего некоторые структуры данных в чисто функциональных структурах данных Криса Окасаки, и натолкнулся на определение этого типа:

 type tree = Node of int * int * tree list;;

Я не думал, что для этого нужен тег, так как это не тип объединения, поэтому я попытался удалить тег, однако я получил следующую ошибку:

# type tree = int * int * tree list;;
Characters 5-33:
type tree = int * int * tree list;;
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The type abbreviation tree is cyclic

Почему это происходит с двумя, казалось бы, эквивалентными определениями типов?

Answer 1

В ML-подобных языках определение рекурсивного типа - это определение, в котором рекурсия не проходит через вариантный тип. Это прагматическое определение в том смысле, что оно ведет к более полезной проверке типов.

В рекурсивных типах нет ничего неразрешимого. Вы можете включить поддержку рекурсивных типов в OCaml с помощью -rectypes флаг.

$ ocaml -rectypes
        OCaml version 4.02.1

# type tree = int * int * tree list;;
type tree = int * int * tree list
# let x: tree = (3, 3, [(4, 4, [])]);;
val x : tree = (3, 3, [(4, 4, [])])

Все обычные гарантии строгой типизации присутствуют, когда включены рекурсивные типы. Основным недостатком является то, что многие непреднамеренные программы принимаются. Другими словами, наличие рекурсивного типа часто является признаком ошибки программирования.

Answer 2

Первое определение типа определяет новый тип. Когда вы опускаете имя конструктора, тогда вместо определения нового типа вы фактически вводите аббревиатуру типа. И по умолчанию аббревиатуры типов не могут быть рекурсивными, так как обычно это не то, что вы имеете в виду.

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

type tree = { node : int * int * tree list }

или даже лучше

type tree = {
  value : int;
  depth : int;
  children : tree list;
}

(примечание: имена полей были выбраны произвольно, поскольку я не знаю их первоначальное назначение)

Подводя итог, суммируемые типы используются не только для введения непересекающихся наборов типов, но и для создания новых типов, таким образом:

 type t = Constr x

вводит тип t, который может быть построен с помощью конструктора Constr из значений типа x,