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

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

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

Ліс f складається зі списку дерев, тоді як дерево t складається з пари значення v та лісу f (його нащадків). Це визначення елегантне і з ним легко працювати абстрактно (наприклад, при доведенні теорем про властивості дерев), оскільки воно виражає дерево простими термінами: список одного типу та пара двох типів.

Це взаємно-рекурсивне визначення можна перетворити на однорекурсивне визначення шляхом вбудованого визначення лісу:

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

Дерево t складається з пари значення v та списку дерев (його нащадків). Це визначення є більш компактним, але дещо заплутанішим: дерево складається з пари одного типу та списку іншого, які вимагають розплутування, щоб довести результати.

У Стандартному ML типи дерев та лісів можуть бути взаємно рекурсивно визначені наступним чином, дозволяючи порожні дерева: [1]

datatype 'a tree = Empty | Node of 'a * 'a forest
and   '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)

З ізорекурсивними типами — рекурсивним ${\displaystyle \mu \alpha .T}$ та його розширення (або розгортання)${\displaystyle T[\mu \alpha .T/\alpha ]}$ (Де позначення${\displaystyle X[Y/Z]}$ вказує на те, що всі екземпляри Z замінені на Y у X) — це різні типи (які не перетинаються) зі спеціальними терміновими конструкціями, які зазвичай називають roll і unroll (згортати і розгортати) що утворюють між собою ізоморфізм. Якщо бути точним: ${\displaystyle roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T}$ і${\displaystyle unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]}$, а ці дві є оберненими функціями.

Відповідно до еквірекурсивних правил, рекурсивний тип ${\displaystyle \mu \alpha .T}$ та його розгортання ${\displaystyle T[\mu \alpha .T/\alpha ]}$ рівні — тобто ці два вирази типу розуміються як один і той же тип. Насправді, більшість теорій еквірекурсивних типів йдуть далі і по суті вказують, що будь-які два вирази типу з однаковим «нескінченним розширенням» еквівалентні. В результаті цих правил еквірекурсивні типи вносять значно більшу складність у систему типів, ніж ізорекурсивні типи. Алгоритмічні проблеми, такі як перевірка типу та висновок типу, є складнішими також для еквірекурсивних типів. Оскільки пряме порівняння не має сенсу для еквірекурсивного типу, їх можна перетворити в канонічну форму за час O (n log n), яку легко порівняти.[2]

Еквірекурсивні типи охоплюють форму самореференційних (або взаємно референційних) визначень типів, що спостерігаються у процедурних та об'єктно-орієнтованих мовах програмування, а також виникають у теоретично-типовій семантиці об'єктів і класів. У функціональних мовах програмування набагато частіше зустрічаються ізорекурсивні типи (під виглядом типів даних).

Рекурсія не дозволена в синонімах типів у Miranda, OCaml (якщо не використовується прапорець -rectypes або це запис чи варіант) та Haskell; так, наприклад, такі типи Haskell є незаконними:

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

Натомість його потрібно загортати в алгебричний тип даних (навіть якщо він має лише один конструктор):

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

Це тому, що синоніми типів, як typedefs в C, замінюються їх визначенням під час компіляції. (Синоніми типів не є «справжніми» типами; вони просто «псевдоніми» для зручності програміста.) Але якщо це буде зроблено з рекурсивним типом, воно буде циклічно нескінченне, оскільки незалежно від того, скільки разів псевдонім замінено, він все одно посилається на себе, наприклад, «Bad» буде рости нескінченно довго: Bad → (Int, Bad) → (Int, (Int, Bad)) → ....

Інший спосіб побачити це полягає в тому, що потрібен рівень опосередкованості (алгебричний тип даних) для того, щоб система ізорекурсивного типу могла зрозуміти, коли згортати і розгортати.