نوع البيانات المتكرر

يمكن أيضًا تعريف أنواع البيانات عن طريق الاستدعاء الذاتي المتبادل . وأهم مثال أساسي على ذلك هو الشجرة ، التي يمكن تعريفها بشكل استدعائي متبادل بدلالة الغابة (قائمة من الأشجار). رمزيًا:

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

تتكون الغابة f من قائمة من الأشجار، بينما تتكون الشجرة t من زوج من القيمة v والغابة f (أبنائها). هذا التعريف أنيق وسهل التطبيق في المفاهيم المجردة (كما هو الحال عند إثبات نظريات حول خصائص الأشجار)، لأنه يعبر عن الشجرة بعبارات بسيطة: قائمة من نوع واحد، وزوج من نوعين.

يمكن تحويل هذا التعريف المتداخل إلى تعريف متداخل بشكل فردي عن طريق تضمين تعريف الغابة:

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

تتكون الشجرة t من زوج من القيمة v وقائمة من الأشجار (أبنائها). هذا التعريف أكثر إيجازًا، ولكنه أكثر تعقيدًا بعض الشيء: تتكون الشجرة من زوج من نوع وقائمة من نوع آخر، مما يتطلب فصلهما لإثبات النتائج المتعلقة بهما.

في لغة النمذجة القياسية (Standard ML) ، يمكن تعريف أنواع بيانات الشجرة والغابة بشكل متكرر متبادل على النحو التالي، مما يسمح بالأشجار الفارغة: ^{[ 1 ]}

نوع البيانات 'a tree = فارغ | عقدة من 'a * 'a forest و 'a forest = لا شيء | عقدة من 'a tree * 'a forest

في لغة هاسكل، يمكن تعريف أنواع بيانات الشجرة والغابة بشكل مشابه:

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 ]}

تُجسّد الأنواع المتماثلة شكل تعريفات الأنواع ذاتية المرجعية (أو المتبادلة المرجعية) الموجودة في لغات البرمجة الكائنية التوجه الاسمية ، وتظهر أيضًا في الدلالات النظرية للأنواع للكائنات والفئات . وفي لغات البرمجة الوظيفية، تُعدّ الأنواع المتماثلة (في صورة أنواع البيانات) شائعة أيضًا. ^{[ 3 ]}