نوع تابع

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

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

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

## التاريخ

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

منطق الرتبة الأولى هو امتداد لمنطق القضايا، يُضيف المُكمِّمات. وقد قام كل من ويليام آلفين هوارد ونيكولاس دي بروين بتوسيع حساب لامدا ليتوافق مع هذا المنطق الأقوى من خلال إنشاء أنواع للدوال المعتمدة، التي تتطابق مع "لكل"، والأزواج المعتمدة، التي تتطابق مع "يوجد".

وبسبب هذا العمل، وغيره من أعمال هوارد، أصبح يُعرف مبدأ المطابقة بين القضايا والأنواع باسم تطابق كاري-هوارد.

## التعريف الرسمي
بشكل غير دقيق، تُشبه الأنواع المعتمدة نوع العائلات المفهرسة من المجموعات. بشكل أكثر رسمية، إذا كان لدينا نوع A:\mathcal{U} ضمن كون من الأنواع \mathcal{U}، يمكن أن يكون لدينا **عائلة من الأنواع** B:A\to\mathcal{U}، والتي تُسنِد لكل عنصر a:A نوعًا B(a):\mathcal{U}. نقول إن النوع B(a) يتغير حسب a.

### نوع Π

الدالة التي يختلف نوع القيمة التي تُعيدها حسب الوسيط (أي لا يوجد مستقر دالة ثابت) تُعرف باسم **دالة معتمدة**، ويُطلق على نوع هذه الدالة اسم **نوع الجداء المعتمد**، أو **نوع Π** (** type**) أو **نوع الدالة المعتمدة**. انطلاقًا من عائلة من الأنواع B: A \to \mathcal{U} يمكننا بناء نوع الدوال المعتمدة \prod_{x : A} B(x)، والتي تتكون عناصرها من دوال تأخذ عنصرًا a : A وتُعيد عنصرًا من B(a). في هذا المثال، يُكتب نوع الدالة المعتمدة عادة على النحو \prod_{x:A} B(x) أو \prod {(x:A)} B(x).

إذا كانت B:A\to\mathcal{U} دالة ثابتة، فإن نوع الجداء المعتمد المقابل يكون مكافئًا لنوع الدالة العادي. أي أن \prod_{x:A}B يساوي حكميًا A\to B عندما لا تعتمد B على x.

يرجع اسم "نوع Π" إلى فكرة أن هذه الأنواع يمكن النظر إليها على أنها جداء ديكارتي للأنواع. كما يمكن فهم أنواع Π ضمن نظرية النماذج بوصفها تكميمًا كليًا.

على سبيل المثال، إذا كتبنا \operatorname{Vec}(\mathbb{R},n) للدوال المتجهة ذات *n* عنصرًا من عدد حقيقي، فإن \prod_{n:\mathbb{N}} \operatorname{Vec}(\mathbb{R},n) سيكون نوع دالة تُعيد، لكل عدد طبيعي ، متجهًا من الأعداد الحقيقية بطول . ويظهر الفضاء الدالي المعتاد كحالة خاصة عندما لا يعتمد نوع النطاق على الوسيط. على سبيل المثال، \prod_{n:\mathbb{N}} {\mathbb{R}} هو نوع الدوال من الأعداد الطبيعية إلى الأعداد الحقيقية، ويُكتب في حساب لامدا النمطي على النحو \mathbb{N}\to\mathbb{R}.

كمثال أكثر تحديدًا، إذا اعتبرنا A نوع الأعداد الصحيحة غير الموقعة من 0 إلى 255 (التي تتناسب مع 8 بت أو 1 بايت)، وB(a) = X_a لكل a : A، فإن \prod_{x:A} B(x) تتحول إلى الجداء X_0\times X_1\times X_2\times\ldots\times X_{253}\times X_{254}\times X_{255}.

### نوع Σ
الثنائية لنوع الجداء المعتمد هي **نوع الزوج المعتمد**، أو **نوع الجمع المعتمد**، أو **نوع سيغما**، أو (بشكل مربك) أيضًا **نوع الجداء المعتمد**. ويمكن أيضًا فهم أنواع سيغما على أنها تكميمات وجودية. وبالعودة إلى المثال أعلاه، إذا كان في كون الأنواع \mathcal{U} نوع A:\mathcal{U} وعائلة من الأنواع B:A\to\mathcal{U}، فإنه يوجد نوع زوج معتمد \sum_{x:A} B(x). (وتشبه الرموز البديلة لهذا النوع ما يُستخدم في أنواع .)

يُجسد نوع الزوج المعتمد فكرة الزوج المرتب الذي يعتمد فيه نوع العنصر الثاني على قيمة العنصر الأول. إذا كان (a,b):\sum_{x:A} B(x), فإن a:A وb:B(a). وإذا كانت B دالة ثابتة، فإن نوع الزوج المعتمد يتحول إلى مكافئ حكميًا لـ نوع الجداء، أي الجداء الديكارتي العادي A\times B.

كمثال أكثر تحديدًا، إذا اعتبرنا A مرة أخرى نوع الأعداد الصحيحة غير الموقعة من 0 إلى 255، وكانت B(a) تساوي X_a مرة أخرى لـ 256 نوعًا اختياريًا مختلفًا من X_a، فإن \sum_{x:A} B(x) تتحول إلى الجمع X_0+X_1+X_2+\ldots+X_{253}+X_{254}+X_{255}.

#### مثال بصيغة تكميم وجودي
ليكن A:\mathcal{U} نوعًا ما، وليكن B:A\to\mathcal{U}. وفقًا لتطابق كاري–هوارد، يمكن تفسير B كمحمول منطقي على عناصر A. ولعنصر معين a : A، فإن كون النوع B(a) مأهولًا يدل على ما إذا كان a يحقق هذا المحمول. ويمكن توسيع هذا التطابق ليشمل التكميم الوجودي والأزواج المعتمدة: تكون القضية \exists{a}{\in}A\,B(a) صحيحة إذا وفقط إذا كان النوع \sum_{a:A}B(a) مأهولًا.

على سبيل المثال، يكون m:\mathbb{N} أصغر من أو يساوي n:\mathbb{N} إذا وفقط إذا وُجد عدد طبيعي آخر k:\mathbb{N} بحيث m + k = n. في المنطق، تُصاغ هذه القضية على النحو التالي:

m\le n \iff \exists{k}{\in}\mathbb{N}\,m+k=n.

وهذه القضية تتطابق مع نوع الزوج المعتمد التالي:

\sum_{k:\mathbb{N}} m+k=n.

أي أن برهانًا على أن m أصغر من أو يساوي n هو زوج يحتوي على عدد غير سالب k، وهو الفرق بين m وn، وبرهان على المساواة m + k = n.

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

### نظرية النوع التابع من المرتبة الأولى
النظام \lambda \Pi الخاص بالأنواع التابعة النقية من المرتبة الأولى، والمقابل لإطار العمل المنطقي LF، يتم الحصول عليه عن طريق تعميم نوع فضاء الدوال في حساب لامبدا البسيط إلى نوع الجداء التابع.

### نظرية النوع التابع من المرتبة الثانية
النظام \lambda \Pi 2 الخاص بالأنواع التابعة من المرتبة الثانية يُستمد من \lambda \Pi بالسماح بالتكميم على مُنشئي الأنواع. في هذه النظرية، يشمل عامل الجداء التابع كلًا من العامل \to الخاص بحساب لامبدا البسيط، والموثق \forall الخاص بنظام F.

### حساب لامبدا التعددي من المرتبة الأعلى بأنواع تابعة
النظام من المرتبة الأعلى \lambda \Pi \omega يُوسّع \lambda \Pi 2 ليشمل جميع أشكال التجريد الأربعة في مكعب اللامبدا: دوال من حدود إلى حدود، من أنواع إلى أنواع، من حدود إلى أنواع، ومن أنواع إلى حدود. يقابل هذا النظام حساب التركيبات والذي يُعد الاشتقاق منه، أي حساب التركيبات الاستقرائية، النظام الأساسي لروك.

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

## مقارنة اللغات مع الأنواع التابعة

## انظر أيضًا
* تصميم بالعقود

## المراجع

## قراءة إضافية

* 
* 
* 
* Brandl، Helmut (2022). حساب التركيبات (Calculus of Constructions)
* 
* 
* 
* 
* 
* 
* 

## روابط خارجية
* البرمجة ذات الأنواع المعتمدة 2008
* البرمجة ذات الأنواع المعتمدة 2010
* البرمجة ذات الأنواع المعتمدة 2011
* "النوع المعتمد" في ويكي هاسكل

تصنيف:أسس الرياضيات
تصنيف:نظرية النمط
تصنيف:أنظمة أنواع