ماذا تعرف عن نوع تابع

في علم الحاسوب والمنطق، يُقصد بـالنمط التابع (بالإنجليزية: Dependent type) النوع الذي تعتمد تعريفاته على قيمة معينة. ويُعدّ هذا من الخصائص المشتركة بين نظرية النمط ونظام الأنواع. في نظرية النمط الحدسية، تُستخدم الأنماط المعتمدة لترميز المحدّدات المعمّمة في المنطق، مثل "لكل" و"يوجد". وفي لغة البرمجة الوظيفية مثل أقدا، أيه تي سي، روك (المعروفة سابقًا باسم كوك), إف، إبيغرام، إدريس، ولين، تساعد الأنماط المعتمدة في تقليل الأخطاء من خلال تمكين المبرمج من إسناد أنواع تقيد أكثر مجموعة التنفيذات الممكنة.

من الأمثلة الشائعة على الأنماط المعتمدة: الدوال المعتمدة والأزواج المعتمدة. قد تعتمد نوعية القيمة المعادة من دالة معتمدة على قيمة (وليس فقط نوع) أحد معطياتها. على سبيل المثال، دالة تأخذ عددًا صحيحًا موجبًا







n





{\displaystyle n}



قد تعيد مصفوفة بطول







n





{\displaystyle n}



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

تضيف الأنماط المعتمدة تعقيدًا إلى نظام الأنواع. فقد يتطلب تحديد التساوي بين أنماط معتمدة داخل برنامج ما إجراء حسابات. وإذا سُمح بقيم عشوائية داخل الأنماط المعتمدة، فإن تحديد تساوي الأنواع قد يتطلب تحديد ما إذا كان برنامجان عشوائيان ينتجان نفس النتيجة؛ ومن ثم فإن قابلية القرار لنظام الأنواع قد تعتمد على دلالات المساواة داخل نظرية النمط المعينة، أي على ما إذا كانت نظرية النمط كثيفة أم امتدادية.

قراءة المقال الكامل على ويكيبيديا ←