نوع تابع

نوع Σ

ومن ناحية أخرى، الثنائية لنوع الجداء المعتمد هي نوع الزوج المعتمد، أو نوع الجمع المعتمد، أو نوع سيغما، أو (بشكل مربك) كذلك نوع الجداء المعتمد. ويمكن كذلك فهم أنواع سيغما على أنها تكميمات وجودية. وبالعودة إلى المثال أعلاه، إذا كان في كون الأنواع نوع وعائلة من الأنواع ، فإنه يوجد نوع زوج معتمد . (وتشبه الرموز البديلة لهذا النوع ما يُستعمل في أنواع .)

من جانب آخر، يُجسد نوع الزوج المعتمد فكرة الزوج المرتب الذي يعتمد فيه نوع العنصر الثاني على قيمة العنصر الأول. إذا كان فإن و. وإذا كانت دالة ثابتة، فإن نوع الزوج المعتمد يتحول إلى مكافئ حكميًا لـ نوع الجداء، أي الجداء الديكارتي العادي .

إضافةً إلى ذلك، كمثال أكثر تحديدًا، إذا اعتبرنا مرة أخرى نوع الأعداد الصحيحة غير الموقعة من 0 إلى 255، وكانت تساوي مرة أخرى لـ 256 نوعًا اختياريًا مختلفًا من ، فإن تتحول إلى الجمع .

التعريف الرسمي

علاوةً على ذلك، بشكل غير دقيق، تُشبه الأنواع المعتمدة نوع العائلات المفهرسة من المجموعات. بشكل أكثر رسمية، إذا كان لدينا نوع ضمن كون من الأنواع ، يمكن أن يكون لدينا عائلة من الأنواع ، والتي تُسنِد لكل عنصر نوعًا . نقول إن النوع يتغير حسب .

نوع Π

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

من جهة ثانية، كمثال أكثر تحديدًا، إذا اعتبرنا نوع الأعداد الصحيحة غير الموقعة من 0 إلى 255 (التي تتناسب مع 8 بت أو 1 بايت)، و لكل ، فإن تتحول إلى الجداء .

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

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

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

البرمجة والمنطق في آنٍ واحد

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

• مقارنة اللغات مع الأنواع التابعة
• انظر كذلك
• تصميم بالعقود
• المراجع

قراءة إضافية

• Brandl، Helmut (2022). حساب التركيبات (Calculus of Constructions)
• روابط خارجية
• البرمجة ذات الأنواع المعتمدة 2008
• البرمجة ذات الأنواع المعتمدة 2010
• البرمجة ذات الأنواع المعتمدة 2011

أنظمة مكعب اللامبدا

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

نظرية النوع التابع من المرتبة الأولى

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

نظرية النوع التابع من المرتبة الثانية

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

حساب لامبدا التعددي من المرتبة الأعلى بأنواع تابعة

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

التاريخ

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

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

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

مثال بصيغة تكميم وجودي

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

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

وفي هذا الصدد، مثلًا، يكون أصغر من أو يساوي إذا وفقط إذا وُجد عدد طبيعي آخر بحيث . في المنطق، تُصاغ هذه القضية على النحو التالي:

ومن ناحية أخرى، ليكن نوعًا ما، وليكن . بحسب تطابق كاري–هوارد، يمكن تفسير كمحمول منطقي على عناصر . ولعنصر معين ، فإن كون النوع مأهولًا يدل على ما إذا كان يحقق هذا المحمول. ويمكن توسيع هذا التطابق ليشمل التكميم الوجودي والأزواج المعتمدة: تكون القضية صحيحة إذا وفقط إذا كان النوع مأهولًا.