بيئة الكتابة

في نظرية الأنواع ، تمثل بيئة الكتابة (أو سياق الكتابة ) العلاقة بين أسماء المتغيرات وأنواع البيانات .

بصورة أكثر رسمية، بيئة${\displaystyle \Gamma }$هي مجموعة أو قائمة مرتبة من الأزواج${\displaystyle \langle x,\tau \rangle }$، وعادة ما تُكتب على النحو التالي${\displaystyle x:\tau }$، أين${\displaystyle x}$متغير و${\displaystyle \tau }$نوعها.

الحكم​

${\displaystyle \Gamma \vdash e:\tau }$

تُقرأ على النحو التالي: "${\displaystyle e}$له نوع${\displaystyle \tau }$في السياق${\displaystyle \Gamma }$[ ^{1 ]​}

لكل فحص لنوع جسم الدالة:

${\displaystyle \Gamma =\{(f,\tau _{1}\times ...\times \tau _{n}\to \tau _{0})|(f,xs,(\tau _{1},...,\tau _{n}),t_{f},\tau _{0})\in e\}}$

مثال على قواعد الكتابة: $${\displaystyle {\begin{array}{c}\Gamma \vdash b:Bool,\Gamma \vdash t_{1}:\tau ,\Gamma \vdash t_{2}:\tau \\\hline \Gamma \vdash ({\text{if}}(b)t_{1}{\text{else}}t_{2}):\tau \\\end{array}}}$$

في لغات البرمجة ذات الكتابة الثابتة ، تُستخدم هذه البيئات ويتم صيانتها بواسطة قواعد الكتابة للتحقق من نوع برنامج أو تعبير معين. ^{[ 1 ]}

• نظام الكتابة