Free constructions for comprehension categories

تخيل أنك تقوم ببناء قلعة ضخمة من قطع الليغو المتداخلة. في عالم علوم الحاسوب، وتحديداً في مجال يُسمى "نظرية الأنواع" (Type Theory)، تُسمى هذه الطوب "أنواعاً"، وتُسمى تعليمات كيفية تركيبها معاً "قواعد لغة البرمجة". تماماً كما هو الحال في الحياة الواقعية، إذا حاولت وضع حجر ثقيل فوق قطعة بلاستيكية هشة، سينهار الهيكل بأكتها. ولمنع حدما يحدث ذلك، يستخدم علماء الحاسوب "الأنواع" للتأكد من أن الكود آمن ومنطقي. ولكن أحياناً، تصبح القواعد معقدة. ماذا لو أردت القول إن "الكلب" هو أيضاً "ثديي"؟ أو أن "الكرة الحمراء" هي نوع محدد من "الكرات"؟ هنا تصبح الأمور صعبة.

للتعامل مع هذه العلاقات المعقدة، يستخدم الرياضيون وعلماء الحاسوب أداة تسمى "نظرية الفئات" (Category Theory). فكر في هذا كخريطة فائقة القوة لا تكتفي فقط بإظهار مكان قطع الليغو، بل توضح أيضاً كيف يمكن تحويل إحداها إلى الأخرى. أحد الطرق الشائعة لرسم هذه الخريطة هو استخدام ما يسمى "التليف" (Fibration). إذا تخيلت كومة من الأوراق الشفافة، فإن التليف يشبه طريقة تنظيم تلك الأوراق بحيث إذا قمت بتحريك ورقة واحدة (سياق أو مجموعة قواعد)، فإن الأشكال المرسومة عليها (الأنواع) تتحرك معها بشكل مثالي. هذه الورقة البحثية تغوص في عمق طريقتين مختلفتين لرسم هذه الخرائط، محاولةً معرفة أيهما أفضل وكيفية تحويل إحداهما إلى الأخرى.

الورقة بعنوان "البناءات الحرة لفئات الاستيعاب" (Free Constructions for Comprehension Categories)، وهي من تأليف فرانشيسكو دانيانو، جاكوبو إيمينيجر، وأندريا جوستو. وهي تتناول لغزاً محدداً في عالم نظرية الأنواع: العلاقة بين نموذجين مختلفين يُسميان "فئات استيعاب جاكوبس" (Jacobs comprehension categories) و"فئات استيعاب لوفير-إرهارد" (Lawvere-Ehrhard comprehension categories).

فكر في فئة استيعاب جاكوبس كورشة عمل مرنة للغاية ومفتوحة النهايات. في ورشة العمل هذه، لديك قطع الليغو (الأنواع) وتعليماتك (السياقات). ولديك أيضاً كتاب قواعد خاص يخبرك بكيفية توسيع تعليماتك بإضافة متغير جديد، مثل قول: "لنضف متغيراً x من النوع A". في هذا النموذج، تُعامل "المورفيزمات" (Morphisms) (وهي تشبه القواعد لتحويل نوع إلى آخر، أو التضمين النوعي) كبيانات منفصلة ومستقلة. الأمر يشبه امتلاك صندوق من الوصلات الإضافية التي يمكنك استخدامها لربط الطوب، لكنها ليست مرتبطة ارتباطاً وثيقاً بالطوب نفسه. هذا يجعل النموذج عاماً جداً، ولكنه أحياناً يكون جامحاً وصعب السيطرة عليه لأن هناك طرقاً كثيرة للربط بين الأشياء.

على الجانب الآخر، تقدم الورقة فئات استيعاب لوفير-إرهارد كنسخة أكثر انضباطاً و"تهذيباً" من ورشة العمل. في هذا النموذج الأكثر صرامة، لا يكون الاتصال بين الأنواع مجرد وصلة فضفاضة؛ بل هو جزء مبني في نسيج النظام نفسه. يوضح المؤلفون أنه في عالم لوفير-إرهارد، يتم تحديد كل "حد" (Term) (أي حالة محددة لنوع ما، مثل كلب محدد) تماماً من خلال نوع خاص من "مورفيزم النوع" القادم من "نوع الوحدة" (Unit Type) (فكر فيه كشيء عام أو مكان محايد عالمي). كما لو أن كل شكل ليغو محدد تبنيه يتم تعريفه تلقائياً من خلال علاقته بشكل "عام" واحد. هذا يخلق علاقة أوثق وأكثر قابلية للتنبؤ بين القواعد والكائنات.

الاكتشاف الرئيسي للورقة هو أن هذين النموذجين ليسا عدوين؛ بل هما مرتبطان بطريقة رياضية محددة للغاية. يثبت المؤلفون أن فئات لوفير-إرهارد هي في الأساس فئات جاكوبس حيث تكون "المورفيزمات" (الوصلات) و"الحدود" (الأشكال المحددة) متطابقتين تماماً، مثل وجهي العملة الواحدة. ويظهرون أنه إذا كانت لديك فئة جاكوبس حيث يمتلك كل نوع "وحدة" فريدة، فإنها تصبح تلقائياً فئة لوفير-إرهارد.

لكن السحر الحقيقي في الورقة يكمن في "البناءات الحرة". المؤلفون لا يكتفون بالمقارنة بينهما فحسب؛ بل يبنون آلة يمكنها تحويل أحدهما إلى الآخر. هم يصفون ثلاث عمليات خطوة بخطوة:

1. من التليف إلى جاكوبس: يوضحون كيفية أخذ تليف أساسي (مجرد كومة من الأوراق) وبناء فئة استيعاب جاكوبس كاملة فوقه تلقائياً. هذا يشبه أخذ كومة من قطع الليغو الخام وتوليد دليل تعليمات كامل لها تلقائياً.
2. من جاكﺒس إلى "الطرفيات": يوضحون كيفية أخذ فئة جاكوبس وإضافة "كائنات طرفية مليفّة" (Fibred terminal objects) إليها. في تشبيه الليغو الخاص بنا، هذا يشبه إضافة "لوحة قاعدة عالمية" خاصة إلى كل مجموعة تعليمات، مما يضمن أن لكل سياق نقطة بداية فريدة ومعيارية.
3. من "الطرفيات" إلى لوفير-إرهرد: أخيراً، يوضحون كيفية أخذ فئة جاكوبس المعززة هذه وإجبارها على أن تصبح فئة لوفير-إرهرد. هذه الخطوة هي الأكثر تعقيداً؛ فهي تتضمن تحديد ودمج "المورفيزمات" المختلفة التي كانت تقوم بنفس الوظيفة، مما يؤدي فعلياً إلى تنظيف ورشة العمل بحيث يصبح كل اتصال فريداً وضرورياً.

المؤلفون واثقون جداً من نتائجهم. فهم لا يقترحون هذه الروابط فحسب؛ بل يقدمون براهين رياضية صارمة (باستخدام أشياء تسمى "الارتباطات الثنائية" و"المساواتات") تثبت أن هذه البناءات تعمل بشكل مثالي. وهم يبرهنون أنه يمكنك البدء بتليف بسيط، ومن خلال تطبيق هذه الخطوات الثلاث بالترتيب، ستنتهي دائماً بفئة استيعاب لوفير-إرهارد.

لماذا يهم هذا؟ لأنه في عالم لغات البرمجة، أصبح امتلاك نظام تضمين نوعي "مرتبط بالبرهان" (حيث تهم الطرق المختلفة لتحويل الأنواع) أمراً بالغ الأهمية بشكل متزايد. تمنح هذه الورقة علماء الحاسوب الأدوات لبناء هذه الأنظمة المعقدة من الصفر، مما يضمن أن القواعد التي يبتكرونها متسقة وسليمة رياضياً. إنه يشبه منح المهندسين المعماريين مجموعة من المخططات التي تضمن أن ناطحات السحاب الخاصة بهم لن تنهار، بغض النظر عن عدد الطوابق الجديدة التي يضيفونها. وتختتم الورقة باقتراح أن هذه "البناءات الحرة" قد تكون المفتاح لبناء لغات برمجة جديدة وأكثر قوة تتعامل مع علاقات الأنواع المعقدة بكل سهولة.