نظام الكتابة

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

نظام الأنواع البسيط للغة برمجة هو مجموعة من القواعد التي تربط نوع بيانات (مثل عدد صحيح ، عدد عشري ، سلسلة نصية ) بكل مصطلح (تعبير ذو قيمة بيانات) في برنامج حاسوبي . في أنظمة الأنواع الأكثر تعقيدًا، يمكن إسناد أنواع إلى مجموعة متنوعة ^من البنى، مثل المتغيرات والتعبيرات والدوال والوحدات . [ ¹^]

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

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

يُقيّد نوع المصطلح السياقات التي يُمكن استخدامه فيها. بالنسبة للمتغير، يُحدد نظام النوع القيم المسموح بها لهذا المتغير. ولكي يُقدّم هذا المتغير كمعامل لعملية ما، يجب أن تكون العملية قادرة على قبول أي قيمة يسمح بها نوع المتغير في هذا المعامل.

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

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

لأنظمة الأنواع أغراض أخرى أيضًا، مثل التعبير عن قواعد العمل، وتمكين تحسينات معينة للمترجم ، والسماح بالإرسال المتعدد ، وتوفير شكل من أشكال التوثيق .

نظرة عامة على الاستخدام

من الأمثلة على نظام الأنواع البسيط لغة C. تتكون أجزاء برنامج C من تعريفات الدوال ، حيث يتم استدعاء دالة من دالة أخرى.

تحدد واجهة الدالة اسم الدالة وقائمة المعاملات التي تُمرر إلى شيفرة الدالة. أما شيفرة الدالة المستدعِية فتحدد اسم الدالة المستدعَية، بالإضافة إلى أسماء المتغيرات التي تحمل القيم المراد تمريرها إليها.

أثناء تنفيذ برنامج حاسوبي ، تُخزَّن القيم مؤقتًا، ثم ينتقل التنفيذ إلى شيفرة الدالة المُستدعاة. تقوم شيفرة الدالة المُستدعاة بالوصول إلى القيم واستخدامها.

إذا تمت كتابة التعليمات داخل الدالة بافتراض استلام قيمة عددية صحيحة ، ولكن الكود المستدعي مرر قيمة عددية عشرية ، فسيتم حساب النتيجة الخاطئة بواسطة الدالة المستدعاة.

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

قد يستخدم المترجم أيضًا النوع الثابت للقيمة لتحسين مساحة التخزين المطلوبة واختيار الخوارزميات المناسبة لإجراء العمليات عليها. في العديد من مترجمات لغة C ، يُمثَّل نوع البيانات float ، على سبيل المثال، بـ 32 بت ، وفقًا لمواصفات IEEE للأعداد العشرية أحادية الدقة . وبالتالي، ستستخدم هذه المترجمات عمليات المعالج الدقيق الخاصة بالأعداد العشرية على هذه القيم (مثل الجمع والضرب، إلخ).

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

الأساسيات

بشكل رسمي، تدرس نظرية الأنواع أنظمة الأنواع. يجب أن تتيح لغة البرمجة إمكانية التحقق من الأنواع باستخدام نظام الأنواع، سواءً أثناء الترجمة أو أثناء التشغيل، سواءً تم تحديدها يدويًا أو استنتاجها تلقائيًا. وكما لخصها مارك ماناس بإيجاز: ^{[ 3 ]}

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

يُضفي تحديد نوع البيانات، أو ما يُسمى بالتصنيف ، معنىً على سلسلة من البتات ، مثل قيمة في الذاكرة أو كائن ما ، مثل متغير . لا يستطيع جهاز الحاسوب العام التمييز بين عنوان الذاكرة ورمز التعليمات ، أو بين حرف وعدد صحيح وعدد عشري ، لأنه لا يُفرّق جوهريًا بين أي من القيم المحتملة التي قد تُمثلها سلسلة البتات . ^{[ ملاحظة 1 ]} يُنقل ربط سلسلة البتات بنوع معين هذا المعنى إلى الجهاز القابل للبرمجة لتشكيل نظام رمزي يتألف من هذا الجهاز وبرنامج ما.

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

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

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

سواءً أكان نظام الأنواع مؤتمتًا بواسطة المُصرّف أو مُحددًا من قِبل المُبرمج، فإنه يجعل سلوك البرنامج غير قانوني إذا كان خارج قواعد نظام الأنواع. تشمل مزايا أنظمة الأنواع التي يُحددها المُبرمج ما يلي:

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

تشمل المزايا التي توفرها أنظمة الأنواع المحددة بواسطة المترجم ما يلي:

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

أخطاء في الكتابة

يحدث خطأ في النوع عندما تتلقى عملية ما بيانات من نوع مختلف عن المتوقع. ^{[ 4 ]} على سبيل المثال، يحدث خطأ في النوع إذا قسم سطر من التعليمات البرمجية عددين صحيحين، وتم تمرير سلسلة من الأحرف إليه بدلاً من عدد صحيح. ^{[ 4 ]} هذه حالة غير مقصودة ^{[ ملاحظة 2 ]} قد تظهر في مراحل متعددة من تطوير البرنامج. لذا، يلزم وجود آلية لاكتشاف هذا الخطأ في نظام النوع. في بعض اللغات، مثل هاسكل ، التي يتم فيها استنتاج النوع تلقائيًا، قد يكون برنامج lint متاحًا للمترجم للمساعدة في اكتشاف الخطأ.

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

التدقيق الإملائي

قد تحدث عملية التحقق من قيود الأنواع وفرضها، أو ما يُعرف بفحص الأنواع ، في وقت الترجمة (فحص ثابت) أو في وقت التشغيل (فحص ديناميكي).

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

لا تُستخدم هذه المصطلحات عادةً بالمعنى الدقيق.

التحقق من النوع الثابت

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

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

يُعدّ التحقق الثابت من أنواع اللغات الكاملة تورينج متحفظًا بطبيعته. بمعنى آخر، إذا كان نظام الأنواع سليمًا (أي أنه يرفض جميع البرامج غير الصحيحة) وقابلًا للتقرير (أي أنه من الممكن كتابة خوارزمية لتحديد ما إذا كان البرنامج مكتوبًا بشكل صحيح)، فلا بد أن يكون غير كامل (أي أن هناك برامج صحيحة، يتم رفضها أيضًا، حتى وإن لم تواجه أخطاءً أثناء التشغيل). ^{[ 7 ]} على سبيل المثال، لنفترض برنامجًا يحتوي على الكود التالي:

if <complex test> then <do something> else <signal that there is a type error>

حتى لو كانت قيمة التعبير <complex test>دائمًا صحيحة trueأثناء التشغيل، فإن معظم مدققي الأنواع سيرفضون البرنامج باعتباره غير صحيح النوع، لأنه من الصعب (إن لم يكن من المستحيل) على المحلل الثابت تحديد أن التفرع elseلن يُنفذ. ^{[ 8 ]} وبالتالي، سيكتشف مدقق الأنواع الثابت أخطاء الأنواع بسرعة في مسارات التعليمات البرمجية قليلة الاستخدام. بدون فحص الأنواع الثابت، حتى اختبارات تغطية التعليمات البرمجية بنسبة 100% قد لا تتمكن من العثور على مثل هذه الأخطاء. قد تفشل الاختبارات في اكتشاف هذه الأخطاء، لأنه يجب مراعاة جميع المواضع التي تُنشأ فيها القيم وجميع المواضع التي تُستخدم فيها قيمة معينة.

لا يمكن التحقق من عدد من ميزات لغات البرمجة المفيدة والشائعة بشكل ثابت، مثل التحويل التنازلي . لذلك، تحتوي العديد من اللغات على كل من التحقق الثابت والديناميكي من الأنواع؛ يتحقق مدقق الأنواع الثابت مما يمكنه التحقق منه، بينما تتحقق عمليات التحقق الديناميكية من الباقي.

تُتيح العديد من اللغات التي تعتمد على التحقق الثابت من الأنواع إمكانية تجاوز مدقق الأنواع. تسمح بعض اللغات للمبرمجين بالاختيار بين أمان الأنواع الثابت والديناميكي. على سبيل المثال، تاريخيًا، كانت لغة C# تُعلن عن المتغيرات بشكل ثابت، ^{[ 9 ]}^{: 77، القسم 3.2،} ولكن C# 4.0 تُقدم dynamicالكلمة المفتاحية `static`، والتي تُستخدم لإعلان المتغيرات المراد التحقق منها ديناميكيًا أثناء وقت التشغيل. ^{[ 9 ]}^{: 117، القسم 4.1.} تسمح لغات أخرى بكتابة شيفرة غير آمنة من حيث الأنواع؛ على سبيل المثال، في لغة C ، يُمكن للمبرمجين تحويل قيمة بحرية بين أي نوعين لهما نفس الحجم، مما يُخالف مفهوم النوع فعليًا.

التحقق الديناميكي من النوع ومعلومات النوع في وقت التشغيل

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

تتضمن معظم لغات البرمجة الآمنة من حيث النوع نوعًا من التحقق الديناميكي من النوع، حتى وإن كانت تحتوي أيضًا على مدقق نوع ثابت. ^{[ 10 ]} والسبب في ذلك هو صعوبة أو استحالة التحقق الثابت من العديد من الميزات أو الخصائص المفيدة. على سبيل المثال، لنفترض أن برنامجًا ما يُعرّف نوعين، A وB، حيث B نوع فرعي من A. إذا حاول البرنامج تحويل قيمة من النوع A إلى النوع B، وهو ما يُعرف بالتحويل التنازلي ، فإن العملية تكون قانونية فقط إذا كانت القيمة المُحوّلة هي بالفعل قيمة من النوع B. وبالتالي، يلزم إجراء فحص ديناميكي للتأكد من سلامة العملية. يُعد هذا الشرط أحد الانتقادات الموجهة للتحويل التنازلي.

بحكم التعريف، قد يؤدي التحقق الديناميكي من الأنواع إلى فشل البرنامج أثناء التشغيل. في بعض لغات البرمجة، من الممكن توقع هذه الإخفاقات والتعافي منها. أما في لغات أخرى، فتُعتبر أخطاء التحقق من الأنواع كارثية.

تُسمى لغات البرمجة التي تتضمن فحص النوع الديناميكي ولكن ليس فحص النوع الثابت غالبًا "لغات البرمجة ذات النوع الديناميكي".

الجمع بين التحقق الثابت والديناميكي من النوع

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

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

تُجري بعض اللغات، مثل كلوجر وكومون ليسب وسيثون ، فحصًا ديناميكيًا للأنواع افتراضيًا، لكنها تسمح للبرامج باختيار الفحص الثابت للأنواع عبر توفير تعليقات توضيحية اختيارية. أحد أسباب استخدام هذه التعليقات هو تحسين أداء الأجزاء الحرجة من البرنامج. ويتم ذلك من خلال الكتابة التدريجية . بيئة البرمجة DrRacket ، وهي بيئة تعليمية مبنية على لغة ليسب، وسلف للغة Racket، تُعتبر أيضًا ذات كتابة مرنة. ^{[ 11 ]}

في المقابل، بدءًا من الإصدار 4.0، توفر لغة C# طريقةً للإشارة إلى عدم ضرورة التحقق من نوع متغير ما بشكل ثابت. فالمتغير الذي يكون نوعه dynamicغير محدد لن يخضع لهذا التحقق. وبدلاً من ذلك، يعتمد البرنامج على معلومات النوع أثناء التشغيل لتحديد كيفية استخدام المتغير. ^{[ 12 ]}^{[ 9 ]}^{: 113-119}

في لغة Rust ، يوفر كائن السمة تحديدًا ديناميكيًا للأنواع التي لا تحتوي على دورات حياة أو تحتوي فقط على دورات حياة. ^[¹³^]dynstd::any::Any'static

التحقق من الأنواع الثابتة والديناميكية عملياً

يتطلب الاختيار بين الكتابة الثابتة والكتابة الديناميكية بعض المقايضات .

يُمكن للتصنيف الثابت اكتشاف أخطاء الأنواع بدقة أثناء الترجمة، مما يزيد من موثوقية البرنامج النهائي. مع ذلك، يختلف المبرمجون حول مدى شيوع أخطاء الأنواع، مما يُؤدي إلى مزيد من الخلافات حول نسبة الأخطاء البرمجية التي يُمكن اكتشافها من خلال تمثيل الأنواع المُصممة بشكل صحيح في الكود. ^{[ 14 ]}^{[ 15 ]} يعتقد مُؤيدو التصنيف الثابت أن البرامج تكون أكثر موثوقية عند فحص أنواعها بدقة، بينما يُشير مُؤيدو التصنيف الديناميكي إلى الكود المُوزع الذي أثبت موثوقيته وإلى قواعد بيانات الأخطاء الصغيرة. تزداد قيمة التصنيف الثابت مع ازدياد قوة نظام الأنواع. وقد اقترح مُؤيدو التصنيف التابع ، المُطبق في لغات مثل Dependent ML و Epigram ، أنه يُمكن اعتبار جميع الأخطاء تقريبًا أخطاءً في الأنواع، إذا تم تعريف الأنواع المُستخدمة في البرنامج بشكل صحيح من قِبل المُبرمج أو استنتاجها بشكل صحيح من قِبل المُترجم. ^[¹⁶^]

يؤدي التحديد الثابت للأنواع عادةً إلى تنفيذ أسرع للتعليمات البرمجية المُجمَّعة. فعندما يعرف المُجمِّع أنواع البيانات المُستخدمة بدقة (وهو أمر ضروري للتحقق الثابت، سواءً من خلال التصريح أو الاستدلال)، فإنه يستطيع إنتاج تعليمات برمجية مُحسَّنة. ولهذا السبب، تسمح بعض اللغات ذات التحديد الديناميكي للأنواع، مثل Common Lisp، بتصريحات اختيارية للأنواع لتحسين الأداء.

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

تتطلب اللغات ذات الكتابة الثابتة التي تفتقر إلى استنتاج الأنواع (مثل C و Java قبل الإصدار 10 ) من المبرمجين تحديد أنواع البيانات التي يجب أن تستخدمها الدوال أو الطرق. يُمكن اعتبار هذا بمثابة توثيق إضافي للبرنامج، أي أنه تفاعلي وديناميكي، بدلاً من كونه ثابتًا. يسمح هذا للمترجم بمنع فقدان التزامن، ومنع تجاهل المبرمجين له. مع ذلك، يُمكن أن تكون اللغة ذات كتابة ثابتة دون الحاجة إلى تحديد أنواع البيانات (من الأمثلة على ذلك Haskell و Scala و OCaml و F# و Swift ، وإلى حد أقل C# و C++ )، لذا فإن تحديد أنواع البيانات بشكل صريح ليس مطلوبًا للكتابة الثابتة في جميع اللغات.

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

يُتيح نظام الكتابة الديناميكي عادةً إمكانية الكتابة الضمنية (مما يُسهّل إعادة استخدام الكود ). كما تتميز العديد من اللغات ذات الكتابة الثابتة بخاصية الكتابة الضمنية أو آليات أخرى مثل البرمجة العامة التي تُسهّل أيضًا إعادة استخدام الكود.

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

أنظمة الأنواع القوية والضعيفة

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

أمان النوع وأمان الذاكرة

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

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

ضع في اعتبارك البرنامج التالي للغة التي تتميز بأنها آمنة من حيث النوع وآمنة من حيث الذاكرة: ^{[ 17 ]}

var x := 5; var y := "37"; var z := x + y;

في هذا المثال، ستكون قيمة المتغير z42. مع أن هذه القيمة قد لا تكون ما توقعه المبرمج، إلا أنها نتيجة محددة بدقة. لو yكانت القيمة سلسلة نصية مختلفة، لا يمكن تحويلها إلى رقم (مثل " Hello, World ")، لكانت النتيجة محددة بدقة أيضًا. قد يكون البرنامج آمنًا من حيث النوع أو الذاكرة، ومع ذلك قد يتعطل عند إجراء عملية غير صالحة. ينطبق هذا على اللغات التي لا يكون نظام أنواعها متقدمًا بما يكفي لتحديد صلاحية العمليات بدقة على جميع المعاملات الممكنة. ولكن إذا واجه البرنامج عملية غير آمنة من حيث النوع، فغالبًا ما يكون إنهاء البرنامج هو الخيار الوحيد.

والآن، لننظر إلى مثال مشابه في لغة C:

int x = 5 ; char y [] = "37" ; char * z = x + y ; printf ( "%c \n " , * z );

في هذا المثال، zسيشير المؤشر إلى عنوان ذاكرة يقع بعد خمسة أحرف من العنوان الحالي y، أي بعد ثلاثة أحرف من الحرف الصفري الأخير للسلسلة التي يشير إليها المؤشر y. هذه ذاكرة لا يُتوقع من البرنامج الوصول إليها. في لغة C، يُعد هذا سلوكًا غير مُعرَّف ، وقد يقوم البرنامج بأي شيء؛ فمع مُصرِّف بسيط، قد يطبع أي بايت مُخزَّن بعد السلسلة "37". كما يُبيِّن هذا المثال، فإن لغة C ليست آمنة من حيث الذاكرة. وبما أن البيانات العشوائية تُعتبر حرفًا، فإنها أيضًا ليست لغة آمنة من حيث النوع.

بشكل عام، يرتبط أمان النوع وأمان الذاكرة ارتباطًا وثيقًا. على سبيل المثال، اللغة التي تدعم العمليات الحسابية على المؤشرات وتحويل الأرقام إلى مؤشرات (مثل لغة C) ليست آمنة من حيث الذاكرة ولا من حيث النوع، لأنها تسمح بالوصول إلى أي ذاكرة كما لو كانت ذاكرة صالحة من أي نوع.

مستويات متفاوتة من التحقق من النوع

تسمح بعض لغات البرمجة بتطبيق مستويات مختلفة من التحقق على أجزاء مختلفة من الكود. ومن الأمثلة على ذلك:

يطبق التوجيه use strictفي JavaScript ^{[ 18 ]}^{[ 19 ]}^{[ 20 ]} و Perl فحصًا أقوى.
يسمح هذا declare(strict_types=1)في PHP ^{[ 21 ]} على أساس كل ملف فقط بقبول متغير من النوع المحدد لتصريح النوع، أو TypeErrorسيتم طرح استثناء.
يسمح هذا Option Strict Onفي VB.NET للمترجم بطلب التحويل بين الكائنات.

يمكن أيضًا استخدام أدوات إضافية مثل lint و IBM Rational Purify لتحقيق مستوى أعلى من الصرامة.

أنظمة الكتابة الاختيارية

اقترح جلعاد براخا ، بشكل رئيسي ، أن يكون اختيار نظام الأنواع مستقلاً عن اختيار اللغة؛ أي أن يكون نظام الأنواع وحدةً قابلةً للدمج في اللغة حسب الحاجة. وهو يعتقد أن هذا مفيد، لأن ما يسميه أنظمة الأنواع الإلزامية يجعل اللغات أقل تعبيرًا والبرمجيات أكثر هشاشة. ^{[ 22 ]} ويُعدّ شرط عدم تأثير نظام الأنواع على دلالات اللغة صعب التحقيق.

يُعدّ التحديد الاختياري للأنواع مرتبطًا بالتحديد التدريجي للأنواع ، ولكنه يختلف عنه . فبينما يُمكن استخدام كلا النوعين لإجراء تحليل ثابت للشيفرة ( التحديد الثابت للأنواع)، فإن أنظمة الأنواع الاختيارية لا تُفرض سلامة الأنواع أثناء التشغيل ( التحديد الديناميكي للأنواع ). ^{[ 22 ]}^{[ 23 ]}

تعدد الأشكال والأنواع

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

أنظمة الكتابة المتخصصة

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

يُقدّم الجدول التالي نظرة عامة على مفاهيم نظرية الأنواع المستخدمة في أنظمة الأنواع المتخصصة. تتراوح الأسماء $M وN وO$ بين المصطلحات والأسماء $\sigma ,\tau$ نطاق الأنواع. سيتم استخدام الترميز التالي:

$M:\sigma$ هذا يعني أن $M$ له نوع $\sigma$ ؛
$M(N)$ هل هذا هو تطبيق لـ $M$ على $N$ ؛
${\displaystyle \tau [\alpha$ (resp. $\tau [x:=N]$ يصف هذا النوع الناتج عن استبدال جميع حالات متغير النوع $α$ (أو متغير الحد $x$ ) في $\tau$ حسب النوع $σ$ (على التوالي المصطلح $N$ ).

مفهوم النوع	الترميز	معنى
وظيفة	$\sigma \to \tau$	لو $M:\sigma \to \tau$ و $N:\sigma$ ، ثم $M(N):\tau$ .
منتج	$\sigma \times \tau$	لو $M:\sigma \times \tau$ ، ثم $M=(N,O)$ هو زوج $N:\sigma$ و $O:\tau$ .
مجموع	$\sigma +\tau$	لو $M:\sigma +\tau$ ، ثم $M=\iota _{1}(N)$ هي أول حقنة $N:\sigma$ ، أو $M=\iota _{2}(N)$ الحقنة الثانية $N:\tau$ .
تقاطع	$\sigma \cap \tau$	لو $M:\sigma \cap \tau$ ، ثم $M:\sigma$ و $M:\tau$ .
الاتحاد	$\sigma \cup \tau$	لو $M:\sigma \cup \tau$ ، ثم $M:\sigma$ أو $M:\tau$ .
سِجِلّ	$\langle x:\tau \rangle$	لو $M:\langle x:\tau \rangle$ إذاً، فإن $M$ لديها عضو $x:\tau$ .
متعدد الأشكال	$\forall {}\alpha .\tau$	لو $M:\forall {}\alpha .\tau$ ، ثم ${\displaystyle M:\tau [\alpha$ لأي نوع $σ$ .
الوجودية	$\exists {}\alpha .\tau$	لو $M:\exists {}\alpha .\tau$ ، ثم ${\displaystyle M:\tau [\alpha$ لنوع $σ$ ما .
التكراري	$\mu \alpha .\tau$	لو $M:\mu \alpha .\tau$ ، ثم ${\displaystyle M:\tau [\alpha$ .
الدالة التابعة ^{[ أ ]}	$(x:\sigma )\to \tau$	لو $M:(x:\sigma )\to \tau$ و $N:\sigma$ ، ثم $M(N):\tau [x:=N]$ .
الزوج التابع ^{[ ب ]}	$(x:\sigma )\times \tau$	لو $M:(x:\sigma )\times \tau$ ، ثم $M=(N,O)$ هو زوج $N:\sigma$ و $O:\tau [x:=N]$ .
التقاطع التابع ^{[ 24 ]}	$(x:\sigma )\cap \tau$	لو $M:(x:\sigma )\cap \tau$ ، ثم $M:\sigma$ و $M:\tau [x:=M]$ .
التقاطع العائلي ^{[ 24 ]}	$\bigcap _{x:\sigma }\tau$	لو ${\textstyle M:\bigcap _{x:\sigma }\tau }$ ، ثم $M:\tau [x:=N]$ لأي مدة $N:\sigma$ .
الاتحاد العائلي ^{[ 24 ]}	$\bigcup _{x:\sigma }\tau$	لو ${\textstyle M:\bigcup _{x:\sigma }\tau }$ ، ثم $M:\tau [x:=N]$ لفترة زمنية معينة $N:\sigma$ .

↑ يُشار إليه أيضًا باسم نوع المنتج التابع ، نظرًا لـ ${\textstyle (x:\sigma )\to \tau =\prod _{x:\sigma }\tau }$ .
↑ يُشار إليه أيضًا باسم نوع المجموع التابع ، لأن ${\textstyle (x:\sigma )\times \tau =\sum _{x:\sigma }\tau }$ .

الأنواع التابعة

تعتمد الأنواع التابعة على فكرة استخدام القيم العددية أو القيم لوصف نوع قيمة أخرى بدقة أكبر. على سبيل المثال، $\mathrm {matrix} (3,3)$ قد يكون هذا النوع من $3\times 3$ المصفوفة. يمكننا بعد ذلك تحديد قواعد الكتابة مثل القاعدة التالية لضرب المصفوفات:

\mathrm {matrix} _{\mathrm {multiply} }:\mathrm {matrix} (k,m)\times \mathrm {matrix} (m,n)\to \mathrm {matrix} (k,n)

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

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

الأنواع الخطية

تُعرَّف الأنواع الخطية ، المستندة إلى نظرية المنطق الخطي والمرتبطة ارتباطًا وثيقًا بأنواع التفرد ، بأنها أنواع تُسند إلى قيم تتميز بخاصية وجود مرجع واحد فقط لها في جميع الأوقات. تُعد هذه الأنواع قيّمة لوصف القيم الكبيرة غير القابلة للتغيير ، مثل الملفات والسلاسل النصية، وما إلى ذلك، لأنه يمكن تحسين أي عملية تُدمر كائنًا خطيًا وتُنشئ كائنًا مشابهًا له في الوقت نفسه (مثل `<T> str = str + "a"`) لتصبح تعديلًا موضعيًا. عادةً ما يكون هذا غير ممكن، لأن مثل هذه التعديلات قد تُسبب آثارًا جانبية على أجزاء من البرنامج التي تحتفظ بمراجع أخرى للكائن، مما يُخلّ بشفافية المرجع . كما تُستخدم هذه الأنواع في نظام التشغيل التجريبي "سينغولاريتي " للتواصل بين العمليات، مما يضمن بشكل ثابت عدم قدرة العمليات على مشاركة الكائنات في الذاكرة المشتركة لمنع حدوث حالات التزامن. تستخدم لغة "كلين" ( لغة شبيهة بلغة "هاسكل" ) نظام الأنواع هذا لتحقيق سرعة عالية (مقارنةً بإجراء نسخ عميق) مع الحفاظ على الأمان.

أنواع التقاطعات

أنواع التقاطع هي أنواع تصف القيم التي تنتمي إلى نوعين آخرين محددين، مع وجود مجموعات قيم متداخلة. على سبيل المثال، في معظم تطبيقات لغة C، يتراوح نطاق نوع البيانات `signed char` بين -128 و127، بينما يتراوح نطاق نوع البيانات `unsigned char` بين 0 و255، لذا فإن نوع التقاطع بين هذين النوعين سيكون نطاقه بين 0 و127. يمكن تمرير نوع التقاطع هذا بأمان إلى الدوال التي تتوقع إما `signed char` أو `unsigned char`، لأنه متوافق مع كلا النوعين.

تُعدّ أنواع التقاطع مفيدةً لوصف أنواع الدوال المُحمّلة: على سبيل المثال، إذا كان " int→ int" هو نوع الدوال التي تأخذ وسيطًا من نوع عدد صحيح وتُرجع عددًا صحيحًا، و" float→ float" هو نوع الدوال التي تأخذ وسيطًا من نوع عدد عشري وتُرجع عددًا عشريًا، فيمكن استخدام تقاطع هذين النوعين لوصف الدوال التي تُنفّذ أحد هذين النوعين، بناءً على نوع المُدخل المُعطى لها. يُمكن تمرير مثل هذه الدالة إلى دالة أخرى تتوقع دالة " int→ int" بأمان؛ ببساطة لن تستخدم وظيفة " float→ float".

في التسلسل الهرمي للتصنيف الفرعي، يمثل تقاطع نوع مع نوع سلف (مثل النوع الأب) النوع الأكثر اشتقاقًا. أما تقاطع الأنواع الشقيقة فهو فارغ.

تتضمن لغة فورسايث تطبيقًا عامًا لأنواع التقاطع. أما النوع المقيد فهو أنواع التحسين .

أنواع النقابات

أنواع الاتحاد هي أنواع تصف قيمًا تنتمي إلى أحد نوعين. على سبيل المثال، في لغة C، يتراوح نطاق نوع البيانات `signed char` من -128 إلى 127، بينما يتراوح نطاق نوع البيانات `unsigned char` من 0 إلى 255. لذا، فإن اتحاد هذين النوعين سيكون له نطاق "افتراضي" إجمالي من -128 إلى 255، ويمكن استخدامه جزئيًا حسب عنصر الاتحاد الذي يتم الوصول إليه. أي دالة تتعامل مع نوع الاتحاد هذا ستتعامل مع أعداد صحيحة ضمن هذا النطاق الكامل. بشكل عام، العمليات الصالحة الوحيدة على نوع الاتحاد هي العمليات الصالحة على كلا النوعين المتحدين. مفهوم "الاتحاد" في لغة C مشابه لأنواع الاتحاد، ولكنه ليس آمنًا من حيث النوع، لأنه يسمح بعمليات صالحة على أي من النوعين، وليس كليهما . أنواع الاتحاد مهمة في تحليل البرامج، حيث تُستخدم لتمثيل القيم الرمزية التي لا تُعرف طبيعتها الدقيقة (مثل القيمة أو النوع).

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

الأنواع الوجودية

تُستخدم الأنواع الوجودية بكثرة مع أنواع السجلات لتمثيل الوحدات النمطية وأنواع البيانات المجردة ، وذلك لقدرتها على فصل التنفيذ عن الواجهة. على سبيل المثال، يصف النوع "T = ∃X { a: X; f: (X → int); }" واجهة وحدة نمطية تحتوي على عضو بيانات يُسمى a من النوع X ودالة تُسمى f تأخذ مُعاملًا من النوع X نفسه وتُرجع عددًا صحيحًا. يمكن تنفيذ ذلك بطرق مختلفة؛ على سبيل المثال:

intT = { أ: int; و: (كثافة العمليات → كثافة العمليات)؛ }
floatT = { a: float; f: (float → int); }

هذان النوعان هما نوعان فرعيان من النوع الوجودي الأكثر عمومية T، ويتوافقان مع أنواع التنفيذ الملموسة، لذا فإن أي قيمة لأحد هذين النوعين هي قيمة من النوع T. وبالنظر إلى قيمة "t" من النوع "T"، نعلم أن "tf(ta)" مُعرَّف النوع بشكل صحيح، بغض النظر عن النوع المجرد X. يُتيح هذا مرونة في اختيار الأنواع المناسبة لتنفيذ معين، بينما تُعزل العملاء الذين يستخدمون قيم نوع الواجهة فقط - النوع الوجودي - عن هذه الخيارات.

بشكل عام، يستحيل على مدقق الأنواع استنتاج نوع الوجود الذي ينتمي إليه أي وحدة نمطية. في المثال أعلاه، يمكن أن يكون للوحدة النمطية intT { a: int; f: (int → int); } النوع ∃X { a: X; f: (X → int); }. الحل الأبسط هو إضافة تعليق توضيحي لكل وحدة نمطية بنوعها المقصود، على سبيل المثال:

intT = { أ: int; و: (كثافة العمليات → كثافة العمليات)؛ } كـ ∃X { أ: X؛ و: (X → كثافة العمليات)؛ }

على الرغم من أن أنواع البيانات المجردة والوحدات النمطية قد تم تطبيقها في لغات البرمجة لفترة طويلة، إلا أنه لم يتم وضع النظرية الرسمية إلا في عام 1988 على يد جون سي. ميتشل وغوردون بلوتكين تحت شعار: "أنواع البيانات المجردة لها نوع وجودي". ^{[ 25 ]} النظرية عبارة عن حساب لامدا من الدرجة الثانية يشبه النظام F ، ولكن مع التكميم الوجودي بدلاً من التكميم الشامل.

الطباعة التدريجية

في نظام أنواع يعتمد على الكتابة التدريجية ، يمكن تحديد نوع المتغيرات إما أثناء الترجمة (وهو ما يُعرف بالكتابة الثابتة)، أو أثناء التشغيل (وهو ما يُعرف بالكتابة الديناميكية). ^{[ 26 ]} يتيح هذا لمطوري البرامج اختيار أيٍّ من نموذجي الكتابة المناسبين، ضمن لغة برمجة واحدة. ^{[ 26 ]} تستخدم الكتابة التدريجية نوعًا خاصًا يُسمى "ديناميكي" لتمثيل الأنواع غير المعروفة ثابتًا؛ إذ تستبدل مفهوم تساوي الأنواع بعلاقة جديدة تُسمى " الاتساق" تربط النوع الديناميكي بكل نوع آخر. علاقة الاتساق متناظرة ولكنها غير متعدية. ^{[ 27 ]}

التصريح والاستنتاج الصريح أو الضمني

تتطلب العديد من أنظمة الأنواع الثابتة، مثل تلك المستخدمة في لغتي C و Java، تعريفات صريحة للأنواع : إذ يجب على المبرمج ربط كل متغير بنوع محدد بشكل واضح. بينما تعتمد أنظمة أخرى، مثل Haskell، على استنتاج الأنواع : حيث يستنتج المترجم أنواع المتغيرات بناءً على كيفية استخدام المبرمجين لها. على سبيل المثال، عند وجود دالة تجمع عددين ، يمكن للمترجم استنتاج أن هذين العددين يجب أن يكونا أعدادًا، لأن عملية الجمع مُعرّفة للأعداد فقط. وبالتالي، فإن أي استدعاء لهذه الدالة في أي مكان آخر من البرنامج يُحدد نوعًا غير عددي (مثل سلسلة نصية أو قائمة) كوسيط سيؤدي إلى ظهور خطأ.f(x,y)xyxyf

يمكن للثوابت والتعبيرات العددية والنصية في التعليمات البرمجية أن تشير، بل وغالبًا ما تفعل، إلى نوع البيانات في سياق معين. على سبيل المثال، قد يشير تعبير ما إلى نوع بيانات الفاصلة العائمة ، بينما قد يشير تعبير آخر إلى قائمة من الأعداد الصحيحة - عادةً ما تكون مصفوفة .3.14[1,2,3]

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

مشاكل اتخاذ القرار

يرتبط نظام الأنواع الذي يخصص أنواعًا للمصطلحات في بيئات الأنواع باستخدام قواعد الكتابة بشكل طبيعي بمشاكل اتخاذ القرار المتعلقة بفحص الأنواع ، وقابلية الكتابة ، وسكن الأنواع . ^{[ 28 ]}

بافتراض بيئة نوع $\Gamma$ مصطلح $e$ ونوع $\tau$ قرر ما إذا كان المصطلح $e$ يمكن تعيين النوع $\tau$ في بيئة النوع.
بفرض مصطلح $e$ ، تحديد ما إذا كانت هناك بيئة نوع $\Gamma$ ونوع $\tau$ بحيث يكون المصطلح $e$ يمكن تعيين النوع $\tau$ في بيئة النوع $\Gamma$ .
بافتراض بيئة نوع $\Gamma$ ونوع $\tau$ قرر ما إذا كان هناك مصطلح $e$ التي يمكن تعيين النوع لها $\tau$ في بيئة النوع.

نظام النوع الموحد

تتميز بعض لغات البرمجة، مثل C# و Scala، بنظام أنواع موحد. ^{[ 29 ]} وهذا يعني أن جميع أنواع C#، بما فيها الأنواع الأولية، ترث من كائن جذر واحد. فكل نوع في C# يرث من فئة Object. أما لغات أخرى، مثل Java و Raku ، فلديها نوع جذر، ولكنها تحتوي أيضًا على أنواع أولية ليست كائنات. ^{[ 30 ]} توفر Java أنواع كائنات مُغلِّفة تتواجد جنبًا إلى جنب مع الأنواع الأولية، مما يتيح للمطورين استخدام إما أنواع الكائنات المُغلِّفة أو الأنواع الأولية الأبسط غير الكائنية. بينما يقوم Raku بتحويل الأنواع الأولية إلى كائنات تلقائيًا عند الوصول إلى توابعها. ^{[ 31 ]}

التوافق: التكافؤ والتصنيف الفرعي

يجب على مدقق الأنواع في لغة ذات كتابة ثابتة التحقق من أن نوع أي تعبير يتوافق مع النوع المتوقع في السياق الذي يظهر فيه هذا التعبير. على سبيل المثال، في عبارة إسناد من الشكل ، يجب أن يتوافق النوع المستنتج للتعبير مع النوع المُعلن أو المستنتج للمتغير . هذا المفهوم للتوافق، والذي يُسمى التوافقية ، خاص بكل لغة برمجة.x := eex

إذا كان نوع `x` eونوع `y` xمتطابقين، وكان التعيين مسموحًا لهذا النوع، فإن هذا التعبير صحيح. وبالتالي، في أبسط أنظمة الأنواع، يختزل سؤال توافق نوعين إلى سؤال تساويهما ( أو تكافؤهما ). مع ذلك، تختلف لغات البرمجة في معاييرها لتحديد متى يُفهم من تعبيرين نوعيين أنهما يدلان على النوع نفسه. تتباين هذه النظريات المعادلة للأنواع تباينًا واسعًا، ومن أبرزها أنظمة الأنواع البنيوية ، حيث يكون أي نوعين يصفان قيمًا بنفس البنية متكافئين، وأنظمة الأنواع الاسمية ، حيث لا يدل أي تعبيرين نوعيين مختلفين نحويًا على النوع نفسه ( أي ، يجب أن يكون للنوعين الاسم نفسه ليكونا متساويين).

في اللغات التي تعتمد على التنميط الفرعي ، تكون علاقة التوافق أكثر تعقيدًا: إذا Bكان `x` نوعًا فرعيًا من `y` ، فيمكن استخدام Aقيمة من النوع `x` في سياق يُتوقع فيه استخدام قيمة من النوع `y` ( متغير مشترك )، حتى لو لم يكن العكس صحيحًا. وكما هو الحال مع التكافؤ، تُعرَّف علاقة التنميط الفرعي بشكل مختلف لكل لغة برمجة، مع وجود العديد من الاختلافات الممكنة. وقد يكون لوجود تعدد الأشكال البارامتري أو المخصص في اللغة آثار على توافق الأنواع.BA

انظر أيضاً

مقارنة أنظمة الأنواع
تباين النوع – مفهوم في لغات البرمجة
تعدد الأشكال (علوم الحاسوب) - استخدام واجهة أو رمز واحد فيما يتعلق بأنواع متعددة مختلفة
توقيع النوع – يحدد المدخلات والمخرجات لدالة أو روتين فرعي أو طريقة
نظرية الأنواع – النظرية الرياضية لأنواع البيانات

ملحوظات

↑ حددت سلسلة حواسيب Burroughs ALGOL محتويات موقع الذاكرة بواسطة بتات العلم. تُحدد بتات العلم محتويات موقع الذاكرة. يتم تحديد التعليمات ونوع البيانات والوظائف بواسطة رمز مكون من 3 بتات بالإضافة إلى محتوياته المكونة من 48 بتًا. كان برنامج التحكم الرئيسي (MCP) هو الوحيد القادر على الكتابة إلى بتات رمز العلم.
↑ على سبيل المثال، قد يظهر خلل في التجريد أثناء التطوير، مما قد يُشير إلى الحاجة إلى مزيد من تطوير أنواع البيانات. — "ينتهي تقييم البرنامج ذي الأنواع الصحيحة دائمًا". — ب. نوردستروم، ك. بيترسون، وج. م. سميث^{[ 5 ]} قد يُؤدي التغيير المنهجي في المتغيرات لتجنب التقاط متغير حر إلى إدخال خطأ ، في لغة برمجة وظيفية حيث تُعتبر الدوال عناصر أساسية.^{[ 6 ]} — من مقالة حساب لامدا .

مراجع

↑ بيرس 2002 ، ص 1: "نظام النوع هو طريقة نحوية قابلة للتطبيق لإثبات عدم وجود سلوكيات معينة للبرنامج عن طريق تصنيف العبارات وفقًا لأنواع القيم التي تحسبها."
↑ كارديلي 2004 ، ص 1: "الغرض الأساسي من نظام النوع هو منع حدوث أخطاء التنفيذ أثناء تشغيل البرنامج".
↑ بيرس 2002 ، ص 208.
1 2 سيثي، ر. (1996). لغات البرمجة: المفاهيم والتركيبات (الطبعة الثانية ). أديسون-ويسلي. ص 142. ISBN 978-0-201-59065-4. OCLC 604732680 .
↑ نوردستروم، ب.؛ بيترسون، ك.؛ سميث، ج.م. (2001). "نظرية مارتن-لوف للأنواع" . البنى الجبرية والمنطقية . دليل المنطق في علوم الحاسوب. المجلد 5. مطبعة جامعة أكسفورد. ص 2. ISBN 978-0-19-154627-3.
↑ تيرنر، د.أ. (12 يونيو 2012). "نبذة تاريخية عن لغات البرمجة الوظيفية" (ملف PDF) . محاضرة مدعوة في مؤتمر TFP12، بجامعة سانت أندروز . انظر القسم الخاص بلغة Algol 60.
↑ "... أي نظام أنواع سليم وقابل للتقرير يجب أن يكون غير مكتمل" - ديدييه ريمي (2017). ص 29، ريمي، ديدييه. "أنظمة الأنواع للغات البرمجة" (ملف PDF) . مؤرشف من الأصل (ملف PDF) في 14 نوفمبر 2017. تم الاطلاع عليه في 26 مايو 2013 .
↑ بيرس 2002 .
1 2 3 سكيت، جون (2019). سي شارب في العمق ( الطبعة الرابعة). مانينغ. ISBN 978-1617294532.
↑ ميغلاني، غاوراف (2018). "توزيع الأساليب الديناميكي أو تعدد الأشكال في وقت التشغيل في جافا" . مؤرشف من الأصل بتاريخ 7 ديسمبر 2020. تم الاطلاع عليه بتاريخ 28 مارس 2021 .
↑ رايت، أندرو ك. (1995). الطباعة العملية على الورق (دكتوراه). جامعة رايس. hdl : 1911/16900 .
↑ "dynamic (C# Reference)" . مكتبة MSDN . مايكروسوفت . تم الاسترجاع في 14 يناير 2014 .
↑ "std::any — Rust" . doc.rust-lang.org . تم الاطلاع عليه بتاريخ 2021-07-07 .
↑ ماير، إريك؛ درايتون، بيتر. "الكتابة الثابتة حيثما أمكن، والكتابة الديناميكية عند الحاجة: نهاية الحرب الباردة بين لغات البرمجة" (ملف PDF) . شركة مايكروسوفت .
↑ لاوتشر، أماندا؛ سنيفلي، بول (2012). "الأنواع مقابل الاختبارات" . InfoQ.
↑ شي، هونغوي (1998). الأنواع التابعة في البرمجة العملية (أطروحة دكتوراه). قسم العلوم الرياضية، جامعة كارنيجي ميلون. CiteSeerX 10.1.1.41.548 . شي، هونغوي؛ بفينينغ، فرانك (1999). "الأنواع التابعة في البرمجة العملية". وقائع الندوة السادسة والعشرين لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة . ACM. الصفحات 214-227 . CiteSeerX 10.1.1.69.2042 . doi : 10.1145/292540.292560 . ISBN 1581130953. S2CID 245490 .
↑ تُعد لغة Visual Basic مثالاً على لغة آمنة من حيث النوع وآمنة من حيث الذاكرة.
↑ "4.2.2 الصيغة الصارمة من ECMAScript" . مواصفات لغة ECMAScript® 2020 ( الطبعة الحادية عشرة). ECMA. يونيو 2020. ECMA-262.
↑ "الوضع الصارم - جافا سكريبت" . MDN . Developer.mozilla.org. 2013-07-03 . تم الاطلاع عليه بتاريخ 2013-07-17 .
↑ "الوضع الصارم (جافا سكريبت)" . MSDN . مايكروسوفت . تم الاسترجاع في 17 يوليو 2013 .
↑ "الكتابة الصارمة" . دليل PHP: مرجع اللغة: الدوال .
1 2 براخا، ج. "أنواع قابلة للتوصيل" (PDF) .
↑ «بالتأكيد. يُطلق عليه "الكتابة التدريجية"، وأعتبره رائجًا. ...» هل توجد لغة برمجة تسمح بالكتابة الثابتة والديناميكية معًا؟ (stackoverflow، ٢٠١٢)
1 2 3 كوبيلوف، أليكسي (2003). "التقاطع التابع: طريقة جديدة لتعريف السجلات في نظرية الأنواع". المؤتمر الثامن عشر لجمعية مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب . LICS 2003. جمعية مهندسي الكهرباء والإلكترونيات. الصفحات 86-95 . CiteSeerX 10.1.1.89.4223 . doi : 10.1109/LICS.2003.1210048 .
↑ ميتشل، جون سي؛ بلوتكين، جوردون دي (يوليو 1988). "للأنواع المجردة نوع وجودي" (ملف PDF) . مجلة ACM للمعاملات في لغات وأنظمة البرمجة . 10 (3): 470-502 . doi : 10.1145/44501.45065 . S2CID 1222153 .
1 2 سيك، جيريمي (24 مارس 2014). "ما هو الكتابة التدريجية؟" .
↑ سيك، جيريمي؛ طه، وليد (سبتمبر 2006). الكتابة التدريجية للغات الوظيفية (ملف PDF) . سكيم والبرمجة الوظيفية 2006. جامعة شيكاغو . الصفحات 81-92 .
^ باريندريجت ، هينك. ديكرز، ويل؛ ستاتمان ، ريتشارد (20 يونيو 2013). حساب التفاضل والتكامل لامدا مع الأنواع . مطبعة جامعة كامبريدج. ص. 66. ردمك 978-0-521-76614-2.
↑ "8.2.4 توحيد نظام الأنواع". مواصفات لغة C# ( الطبعة الخامسة). ECMA. ديسمبر 2017. ECMA-334.
↑ "الأنواع الأصلية" . وثائق بيرل 6 .
↑ "الأرقام، § التغليف التلقائي" . وثائق بيرل 6 .

للمزيد من القراءة

كارديلي، لوكا ؛ ويغنر، بيتر (ديسمبر 1985). "حول فهم الأنواع، وتجريد البيانات، وتعدد الأشكال" (ملف PDF) . مجلة ACM Computing Surveys . 17 (4): 471-523 . CiteSeerX 10.1.1.117.695 . doi : 10.1145/6041.6042 . S2CID 2921816 .
بيرس، بنجامين سي. (2002). أنواع لغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا. ISBN 978-0-262-16209-8.
كارديلي، لوكا (2004). "أنظمة الأنواع" (ملف PDF) . في: ألين ب. تاكر (محرر). دليل CRC لعلوم وهندسة الحاسوب ( الطبعة الثانية). مطبعة CRC. رقم ISBN 978-1584883609.
ترات، لورانس (يوليو 2009). "5. لغات البرمجة ذات الكتابة الديناميكية" . التقدم في الحوسبة . المجلد 77. إلسيفير. الصفحات 149-184 . doi : 10.1016/S0065-2458(09)01205-4 . ISBN 978-0-12-374812-6.

روابط خارجية

الوسائط المتعلقة بأنظمة الكتابة على ويكيميديا كومنز
"ما يجب معرفته قبل مناقشة أنظمة الكتابة"

[26] يُشار إليه أيضًا باسم نوع المنتج التابع ، نظرًا لـ ${\textstyle (x:\sigma )\to \tau =\prod _{x:\sigma }\tau }$ .

[27] يُشار إليه أيضًا باسم نوع المجموع التابع ، لأن ${\textstyle (x:\sigma )\times \tau =\sum _{x:\sigma }\tau }$ .

[Burroughs-4] حددت سلسلة حواسيب Burroughs ALGOL محتويات موقع الذاكرة بواسطة بتات العلم. تُحدد بتات العلم محتويات موقع الذاكرة. يتم تحديد التعليمات ونوع البيانات والوظائف بواسطة رمز مكون من 3 بتات بالإضافة إلى محتوياته المكونة من 48 بتًا. كان برنامج التحكم الرئيسي (MCP) هو الوحيد القادر على الكتابة إلى بتات رمز العلم.

[leakyCondition-8] على سبيل المثال، قد يظهر خلل في التجريد أثناء التطوير، مما قد يُشير إلى الحاجة إلى مزيد من تطوير أنواع البيانات. — "ينتهي تقييم البرنامج ذي الأنواع الصحيحة دائمًا". — ب. نوردستروم، ك. بيترسون، وج. م. سميث^{[ 5 ]} قد يُؤدي التغيير المنهجي في المتغيرات لتجنب التقاط متغير حر إلى إدخال خطأ ، في لغة برمجة وظيفية حيث تُعتبر الدوال عناصر أساسية.^{[ 6 ]} — من مقالة حساب لامدا .

[FOOTNOTEPierce20021-1] بيرس 2002 ، ص 1: "نظام النوع هو طريقة نحوية قابلة للتطبيق لإثبات عدم وجود سلوكيات معينة للبرنامج عن طريق تصنيف العبارات وفقًا لأنواع القيم التي تحسبها."

[FOOTNOTECardelli20041-2] كارديلي 2004 ، ص 1: "الغرض الأساسي من نظام النوع هو منع حدوث أخطاء التنفيذ أثناء تشغيل البرنامج".

[FOOTNOTEPierce2002208-3] بيرس 2002 ، ص 208.

[Sethi1997-5] 1 2 سيثي، ر. (1996). لغات البرمجة: المفاهيم والتركيبات (الطبعة الثانية ). أديسون-ويسلي. ص 142. ISBN 978-0-201-59065-4. OCLC 604732680 .

[hlcs-6] نوردستروم، ب.؛ بيترسون، ك.؛ سميث، ج.م. (2001). "نظرية مارتن-لوف للأنواع" . البنى الجبرية والمنطقية . دليل المنطق في علوم الحاسوب. المجلد 5. مطبعة جامعة أكسفورد. ص 2. ISBN 978-0-19-154627-3.

[tfp12-7] تيرنر، د.أ. (12 يونيو 2012). "نبذة تاريخية عن لغات البرمجة الوظيفية" (ملف PDF) . محاضرة مدعوة في مؤتمر TFP12، بجامعة سانت أندروز . انظر القسم الخاص بلغة Algol 60.

[9] "... أي نظام أنواع سليم وقابل للتقرير يجب أن يكون غير مكتمل" - ديدييه ريمي (2017). ص 29، ريمي، ديدييه. "أنظمة الأنواع للغات البرمجة" (ملف PDF) . مؤرشف من الأصل (ملف PDF) في 14 نوفمبر 2017. تم الاطلاع عليه في 26 مايو 2013 .

[FOOTNOTEPierce2002-10] بيرس 2002 .

[Skeet-11] 1 2 3 سكيت، جون (2019). سي شارب في العمق ( الطبعة الرابعة). مانينغ. ISBN 978-1617294532.

[12] ميغلاني، غاوراف (2018). "توزيع الأساليب الديناميكي أو تعدد الأشكال في وقت التشغيل في جافا" . مؤرشف من الأصل بتاريخ 7 ديسمبر 2020. تم الاطلاع عليه بتاريخ 28 مارس 2021 .

[13] رايت، أندرو ك. (1995). الطباعة العملية على الورق (دكتوراه). جامعة رايس. hdl : 1911/16900 .

[14] "dynamic (C# Reference)" . مكتبة MSDN . مايكروسوفت . تم الاسترجاع في 14 يناير 2014 .

[15] "std::any — Rust" . doc.rust-lang.org . تم الاطلاع عليه بتاريخ 2021-07-07 .

[16] ماير، إريك؛ درايتون، بيتر. "الكتابة الثابتة حيثما أمكن، والكتابة الديناميكية عند الحاجة: نهاية الحرب الباردة بين لغات البرمجة" (ملف PDF) . شركة مايكروسوفت .

[17] لاوتشر، أماندا؛ سنيفلي، بول (2012). "الأنواع مقابل الاختبارات" . InfoQ.

[18] شي، هونغوي (1998). الأنواع التابعة في البرمجة العملية (أطروحة دكتوراه). قسم العلوم الرياضية، جامعة كارنيجي ميلون. CiteSeerX 10.1.1.41.548 . شي، هونغوي؛ بفينينغ، فرانك (1999). "الأنواع التابعة في البرمجة العملية". وقائع الندوة السادسة والعشرين لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة . ACM. الصفحات 214-227 . CiteSeerX 10.1.1.69.2042 . doi : 10.1145/292540.292560 . ISBN 1581130953. S2CID 245490 .

[19] تُعد لغة Visual Basic مثالاً على لغة آمنة من حيث النوع وآمنة من حيث الذاكرة.

[20] "4.2.2 الصيغة الصارمة من ECMAScript" . مواصفات لغة ECMAScript® 2020 ( الطبعة الحادية عشرة). ECMA. يونيو 2020. ECMA-262.

[21] "الوضع الصارم - جافا سكريبت" . MDN . Developer.mozilla.org. 2013-07-03 . تم الاطلاع عليه بتاريخ 2013-07-17 .

[22] "الوضع الصارم (جافا سكريبت)" . MSDN . مايكروسوفت . تم الاسترجاع في 17 يوليو 2013 .

[23] "الكتابة الصارمة" . دليل PHP: مرجع اللغة: الدوال .

[Bracha-24] 1 2 براخا، ج. "أنواع قابلة للتوصيل" (PDF) .

[25] «بالتأكيد. يُطلق عليه "الكتابة التدريجية"، وأعتبره رائجًا. ...» هل توجد لغة برمجة تسمح بالكتابة الثابتة والديناميكية معًا؟ (stackoverflow، ٢٠١٢)

[K03-28] 1 2 3 كوبيلوف، أليكسي (2003). "التقاطع التابع: طريقة جديدة لتعريف السجلات في نظرية الأنواع". المؤتمر الثامن عشر لجمعية مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب . LICS 2003. جمعية مهندسي الكهرباء والإلكترونيات. الصفحات 86-95 . CiteSeerX 10.1.1.89.4223 . doi : 10.1109/LICS.2003.1210048 .

[29] ميتشل، جون سي؛ بلوتكين، جوردون دي (يوليو 1988). "للأنواع المجردة نوع وجودي" (ملف PDF) . مجلة ACM للمعاملات في لغات وأنظمة البرمجة . 10 (3): 470-502 . doi : 10.1145/44501.45065 . S2CID 1222153 .

[siek-30] 1 2 سيك، جيريمي (24 مارس 2014). "ما هو الكتابة التدريجية؟" .

[siekTaha-31] سيك، جيريمي؛ طه، وليد (سبتمبر 2006). الكتابة التدريجية للغات الوظيفية (ملف PDF) . سكيم والبرمجة الوظيفية 2006. جامعة شيكاغو . الصفحات 81-92 .

[32] باريندريجت ، هينك. ديكرز، ويل؛ ستاتمان ، ريتشارد (20 يونيو 2013). حساب التفاضل والتكامل لامدا مع الأنواع . مطبعة جامعة كامبريدج. ص. 66. ردمك 978-0-521-76614-2.

[33] "8.2.4 توحيد نظام الأنواع". مواصفات لغة C# ( الطبعة الخامسة). ECMA. ديسمبر 2017. ECMA-334.

[34] "الأنواع الأصلية" . وثائق بيرل 6 .

[35] "الأرقام، § التغليف التلقائي" . وثائق بيرل 6 .

من

[ 2 ]

[ 3 ]

[ ملاحظة 1 ]

[ 4 ]

[ ملاحظة 2 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[

[ 14 ]

[ 15 ]

[

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ أ ]

[ ب ]

[ 24 ]

[ 25 ]

[ 26 ]

[ 27 ]

[ 28 ]

[ 29 ]

[ 30 ]

[ 31 ]

[ 5 ]

[ 6 ]