نوع تابع

الدالة التي يختلف نوع القيمة التي تُعيدها حسب الوسيط (أي لا يوجد مستقر دالة ثابت) تُعرف باسم دالة معتمدة، ويُطلق على نوع هذه الدالة اسم نوع الجداء المعتمد، أو نوع Π (Π type) أو نوع الدالة المعتمدة.^[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}$ ليشمل جميع أشكال التجريد الأربعة في مكعب اللامبدا: دوال من حدود إلى حدود، من أنواع إلى أنواع، من حدود إلى أنواع، ومن أنواع إلى حدود. يقابل هذا النظام حساب التركيبات والذي يُعد الاشتقاق منه، أي حساب التركيبات الاستقرائية، النظام الأساسي لروك.