النوع التابع

الدالة التي يتغير نوع القيمة المُعادة بتغير وسيطها (أي ليس لها مجال مُقابل ثابت ) تُسمى دالة تابعة ، ويُسمى نوع هذه الدالة نوع الضرب التابع ، أو نوع باي ( نوع Π )، أو نوع الدالة التابعة . ^{[ 4 ]} وهي تنتمي إلى عائلة من الأنواع.${\displaystyle B:A\to {\mathcal {U}}}$يمكننا بناء نوع الدوال التابعة${\textstyle \prod _{x:A}B(x)}$، والتي تكون حدودها دوال تأخذ حدًا${\displaystyle a:A}$وأعد مصطلحًا في${\displaystyle B(a)}$في هذا المثال، يُكتب نوع الدالة التابعة عادةً على النحو التالي:${\textstyle \prod _{x:A}B(x)}$أو${\textstyle \prod {(x:A)}B(x)}$.

لو${\displaystyle B:A\to {\mathcal {U}}}$إذا كانت دالة ثابتة، فإن نوع المنتج التابع المقابل لها يكافئ نوع الدالة العادية . أي،${\textstyle \prod _{x:A}B}$يُعتبر متساوياً من حيث الحكم مع${\displaystyle A\to B}$متى${\displaystyle B}$لا يعتمد على${\displaystyle x}$.

يُستمد اسم "النمط Π" من فكرة إمكانية اعتبار هذه الأنماط بمثابة حاصل ضرب ديكارتي للأنماط. كما يمكن فهم الأنماط Π على أنها نماذج للمكممات الشاملة .

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

ولتقديم مثال أكثر واقعية، خذ${\displaystyle A}$أن يكون نوع الأعداد الصحيحة غير الموقعة من 0 إلى 255 (الأعداد التي تتناسب مع 8 بتات أو 1 بايت) و${\displaystyle B(a)=X_{a}}$ل${\displaystyle a:A}$، ثم${\textstyle \prod _{x:A}B(x)}$يتحول إلى نتاج${\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}$.

النوع الثنائي لنوع المنتج التابع هو نوع الزوج التابع ، أو نوع المجموع التابع ، أو نوع سيجما ، أو (بشكل مُربك) نوع المنتج التابع . ^{[ 4 ]} يمكن أيضًا فهم أنواع سيجما على أنها مُكمِّمات وجودية . بالاستمرار في المثال أعلاه، إذا، في عالم الأنواع${\displaystyle {\mathcal {U}}}$يوجد نوع${\displaystyle A:{\mathcal {U}}}$وعائلة من الأنواع${\displaystyle B:A\to {\mathcal {U}}}$ثم يوجد نوع الزوج التابع${\textstyle \sum _{x:A}B(x)}$(الرموز البديلة مشابهة لتلك الخاصة بأنواع Π .)

يُجسّد نوع الزوج التابع فكرة الزوج المرتب حيث يعتمد نوع الحد الثاني على قيمة الحد الأول.${\textstyle (a,b):\sum _{x:A}B(x),}$ثم${\displaystyle a:A}$و${\displaystyle b:B(a)}$. لو${\displaystyle B}$إذا كانت دالة ثابتة، فإن نوع الزوج التابع يصبح (يساوي حكمياً) نوع الضرب ، أي الضرب الديكارتي العادي${\displaystyle A\times B}$[ ^{4 ]​}

ولتقديم مثال أكثر واقعية، خذ${\displaystyle A}$أن يكون مرة أخرى نوعًا من الأعداد الصحيحة غير الموقعة من 0 إلى 255، و${\displaystyle B(a)}$أن يكون مساوياً مرة أخرى لـ${\displaystyle X_{a}}$لـ 256 أخرى عشوائية${\displaystyle X_{a}}$، ثم${\textstyle \sum _{x:A}B(x)}$يتحول إلى المجموع${\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}$.

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

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

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