مُنشئ النوع

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

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

بصورة مجردة، مُنشئ النوع هو مُعامل نوع من الرتبة n يأخذ كمعامل صفر أو أكثر من الأنواع، ويُعيد نوعًا آخر. وباستخدام تقنية التخصيص الجزئي (currying)، يُمكن (إعادة) كتابة مُعاملات النوع من الرتبة n كسلسلة من تطبيقات مُعاملات النوع من الرتبة n. لذلك، يُمكننا اعتبار مُعاملات النوع بمثابة حساب لامدا بسيط النوع، والذي له نوع أساسي واحد فقط، يُشار إليه عادةً بـ${\displaystyle *}$، وتنطق "type"، وهو نوع جميع الأنواع في اللغة الأساسية، والتي تسمى الآن الأنواع المناسبة من أجل تمييزها عن أنواع عوامل النوع في حسابها الخاص، والتي تسمى الأنواع .

قد تربط عوامل النوع متغيرات النوع. على سبيل المثال، يتطلب تحديد بنية حساب لامدا البسيط على مستوى النوع ربط عوامل النوع، أو عوامل النوع ذات الرتبة الأعلى. تتوافق عوامل النوع الرابطة هذه مع المحور الثاني لمكعب لامدا ، ونظريات النوع مثل حساب لامدا البسيط مع عوامل النوع، λω _. يؤدي دمج عوامل النوع مع حساب لامدا متعدد الأشكال ( النظام F ) إلى النظام _Fω .

تستخدم بعض لغات البرمجة الوظيفية مُنشئات الأنواع بشكل صريح. ومن الأمثلة البارزة على ذلك لغة هاسكل ، حيث dataتُعتبر جميع تعريفات الأنواع بمثابة تعريفات لمنشئات الأنواع، وتُسمى الأنواع الأساسية (أو مُنشئات الأنواع الصفرية) ثوابت الأنواع. ^{[ 1 ] [ 2 ]} كما يمكن اعتبار مُنشئات الأنواع أنواع بيانات متعددة الأشكال ذات معلمات .

• النوع (نظرية الأنواع)
• نوع البيانات الجبرية
• نوع البيانات المتكرر