نوع فارغ

في نظرية الأنواع ، يُشار عادةً إلى النوع الفارغ أو النوع العبثي بـ${\displaystyle \mathbb {0} }$هو نوعٌ بلا حدود. يُمكن تعريف هذا النوع بأنه حاصل الضرب الصفري (أي مجموع منفصل لأنواع لا حدود لها). ^{[ 1 ]} كما يُمكن تعريفه بأنه النوع متعدد الأشكال.${\displaystyle \forall tt}$^{[ 2 ]}

لأي نوع${\displaystyle P}$النوع${\displaystyle \neg P}$يُعرَّف بأنه${\displaystyle P\to \mathbb {0} }$كما تشير الرموز، وفقًا لتطابق كاري-هوارد ، فإن مصطلحًا من النوع${\displaystyle \mathbb {0} }$هو اقتراح خاطئ، ومصطلح من النوع${\displaystyle \neg P}$هو دليل مضاد للقضية P. ^{[ 1 ]}

لا يشترط أن تحتوي نظرية الأنواع على نوع فارغ. وعند وجوده، لا يكون النوع الفارغ فريدًا بشكل عام. ^{[ 2 ]} على سبيل المثال،${\displaystyle T\to \mathbb {0} }$كما أنها غير مأهولة لأي نوع من أنواع السكان${\displaystyle T}$.

إذا احتوى نظام الأنواع على نوع فارغ، فيجب أن يكون النوع السفلي فارغًا أيضًا، لذلك لا يتم التمييز بينهما ويتم الإشارة إلى كليهما.${\displaystyle \bot }$.