Рекурсивный тип данных

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

Важным применением рекурсии в информатике является определение динамических структур данных, таких как списки и деревья. Рекурсивные структуры данных могут динамически увеличиваться до сколь угодно большого размера в соответствии с требованиями времени выполнения; напротив, требования к размеру статического массива должны быть установлены во время компиляции.

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

Пример

См. Также: Рекурсия (информатика) § Рекурсивные структуры данных (структурная рекурсия)

Примером является тип списка в Haskell :

data List a = Nil | Cons a (List a)

Это указывает на то, что список a представляет собой либо пустой список, либо ячейку cons, содержащую «a» («голову» списка) и другой список («хвост»).

Другой пример — аналогичный односвязный тип в Java:

class List<E> {    E value;    List<E> next;}

Это указывает на то, что непустой список типа E содержит элемент данных типа E и ссылку на другой объект List для остальной части списка (или нулевую ссылку, указывающую, что это конец списка).

Взаимно рекурсивные типы данных

Дополнительная информация: Взаимная рекурсия § Типы данных.

Типы данных также могут определяться посредством взаимной рекурсии . Наиболее важным базовым примером этого является дерево , которое можно взаимно рекурсивно определить в терминах леса (списка деревьев). Символически:

f: [t[1], ..., t[k]]t: v f

Лес f состоит из списка деревьев, а дерево t состоит из пары значения v и леса f (его дочерних элементов). Это определение элегантно и с ним легко работать абстрактно (например, при доказательстве теорем о свойствах деревьев), поскольку оно выражает дерево простыми словами: список одного типа и пара двух типов.

Это взаимно рекурсивное определение можно преобразовать в однорекурсивное определение, встроив определение леса:

t: v [t[1], ..., t[k]]

Дерево t состоит из пары значений v и списка деревьев (его дочерних элементов). Это определение более компактно, но несколько сложнее: дерево состоит из пары одного типа и списка другого, распутывание которых необходимо для доказательства результатов.

В Standard ML типы данных «дерево» и «лес» могут быть взаимно рекурсивно определены следующим образом, что позволяет создавать пустые деревья:

datatype 'a tree = Empty | Node of 'a * 'a forestand      'a forest = Nil | Cons of 'a tree * 'a forest

В Haskell типы данных «дерево» и «лес» можно определить аналогичным образом:

data Tree a = Empty            | Node (a, Forest a)data Forest a = Nil              | Cons (Tree a) (Forest a)

Теория

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

Например, натуральные числа (см. арифметику Пеано ) могут определяться типом данных Haskell:

data Nat = Zero | Succ Nat

В теории типов мы бы сказали: $nat=\mu \alpha .1+\alpha$ где два плеча типа суммы представляют конструкторы данных Zero и Succ. Ноль не принимает аргументов (таким образом, представленный типом единицы ), а Succ принимает другой Nat (таким образом, еще один элемент $\mu \alpha .1+\alpha$).

Существует две формы рекурсивных типов: так называемые изорекурсивные типы и эквирекурсивные типы. Эти две формы различаются тем, как вводятся и исключаются термины рекурсивного типа.

Изорекурсивные типы

В случае изорекурсивных типов рекурсивный тип $\mu \alpha .T$ и его расширение (или развертывание ) $T[\mu \alpha .T/\alpha ]$ (где обозначение $X[Y/Z]$ указывает, что все экземпляры Z заменяются на Y в X) являются отдельными (и непересекающимися) типами со специальными терминальными конструкциями, обычно называемымиroll и unroll , которые образуют изоморфизм между ними. Если быть точным: $roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T$ и $unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]$, и эти две являются обратными функциями .

Эквикурсивные типы

Согласно правилам эквикурсивности, рекурсивный тип $\mu \alpha .T$ и его развертывание $T[\mu \alpha .T/\alpha ]$ равны . – то есть эти два выражения типа считаются обозначающими один и тот же тип Фактически, большинство теорий эквикурсивных типов идут дальше и по существу определяют, что любые два выражения типа с одним и тем же «бесконечным расширением» эквивалентны. В результате этих правил эквайрекурсивные типы вносят значительно большую сложность в систему типов, чем изорекурсивные типы. Алгоритмические задачи, такие как проверка типов и вывод типов, также более сложны для эквикурсивных типов. Поскольку прямое сравнение не имеет смысла для эквикурсивного типа, их можно преобразовать в каноническую форму за время O(n log n), что позволяет легко сравнивать.

Изорекурсивные типы отражают форму самореферентных (или взаимно ссылающихся) определений типов, наблюдаемых в номинальных объектно-ориентированных языках программирования, а также возникают в теоретико-типовой семантике объектов и классов . В языках функционального программирования также распространены изорекурсивные типы (под видом типов данных).

Синонимы рекурсивного типа

В TypeScript рекурсия разрешена в псевдонимах типов. Таким образом, допускается следующий пример.

type Tree = number | Tree[];let tree: Tree = [1, [2, 3]];

Однако рекурсия не разрешена в синонимах типов в Miranda , OCaml (если только -rectypes используется флаг или это запись или вариант), или Haskell; так, например, следующие типы Haskell недопустимы:

type Bad = (Int, Bad)type Evil = Bool -> Evil

Вместо этого они должны быть заключены в алгебраический тип данных (даже если у них только один конструктор):

data Good = Pair Int Gooddata Fine = Fun (Bool -> Fine)

Это связано с тем, что синонимы типов, такие как определения типов в C, заменяются их определениями во время компиляции. (Синонимы типов не являются «настоящими» типами; это просто «псевдонимы» для удобства программиста.) Но если попытаться сделать это с рекурсивным типом, цикл будет бесконечным, поскольку независимо от того, сколько раз будет подставлен псевдоним, он все равно будет ссылается на себя, например, «Плохое» будет расти бесконечно: Bad → (Int, Bad) → (Int, (Int, Bad)) → ... .

Другой способ увидеть это состоит в том, что некоторый уровень косвенности (алгебраический тип данных) необходим, чтобы позволить системе изорекурсивных типов определить, когда следует свернуть и развернуть .

См. также

• Рекурсивное определение
• Алгебраический тип данных
• Индуктивный тип
• Узел (информатика)

Источники

• Харпер, Роберт (1998), Объявления типов данных , заархивировано из оригинала 1 октября 1999 г.