نظام النوع

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

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

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

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

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

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

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

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

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

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

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

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

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

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

الأساسيات

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

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

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

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

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

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

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

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

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

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

أخطاء النوع

يحدث خطأ النوع عندما تتلقى عملية نوعًا مختلفًا من البيانات عما كانت تتوقعه. ^[4] على سبيل المثال، قد يحدث خطأ النوع إذا قسم سطر من التعليمات البرمجية عددين صحيحين، وتم تمرير سلسلة من الأحرف بدلاً من عدد صحيح. ^[4] إنها حالة غير مقصودة ^{[ملاحظة 2]} قد تتجلى في مراحل متعددة من تطوير البرنامج. وبالتالي، هناك حاجة إلى مرفق للكشف عن الخطأ في نظام النوع. في بعض اللغات، مثل Haskell ، حيث يتم أتمتة استنتاج النوع ، قد يكون 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الكلمة الأساسية، والتي تُستخدم لإعلان المتغيرات التي سيتم فحصها ديناميكيًا في وقت التشغيل. ^[9]^{: 117، القسم 4.1.} تسمح لغات أخرى بكتابة كود غير آمن للنوع؛ على سبيل المثال، في لغة C ، يمكن للمبرمجين تحويل قيمة بحرية بين أي نوعين لهما نفس الحجم، مما يقوض مفهوم النوع بشكل فعال.

للحصول على قائمة باللغات ذات التحقق من النوع الثابت، راجع فئة اللغات ذات النوع الثابت .

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

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

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

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

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

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

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

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

بعض اللغات، على سبيل المثال Clojure أو Common Lisp أو Cython ، يتم فحصها ديناميكيًا بشكل افتراضي، ولكنها تسمح للبرامج باختيار فحص النوع الثابت من خلال توفير تعليقات توضيحية اختيارية. أحد أسباب استخدام مثل هذه التلميحات هو تحسين أداء الأقسام الحرجة من البرنامج. يتم إضفاء الطابع الرسمي على ذلك من خلال الكتابة التدريجية. بيئة البرمجة DrRacket ، وهي بيئة تربوية تعتمد على Lisp، وسابقة للغة Racket، هي أيضًا ذات نوع ناعم. ^[11]

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

في Rust ، يوفر النوع كتابة ديناميكية للأنواع. ^[13]dyn std::any::Any'static

التحقق من النوع الثابت والديناميكي في الممارسة العملية

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

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

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

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

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

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

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

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

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

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

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

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

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

فكر في البرنامج التالي للغة آمنة للنوع وآمنة للذاكرة: ^[17]

متغير x := 5؛   
var y := "37";
متغير z := x + y؛

في هذا المثال، سيكون للمتغير zالقيمة 42. ورغم أن هذا قد لا يكون ما توقعه المبرمج، إلا أنه نتيجة محددة جيدًا. وإذا 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 OnVB.NET يسمح للمترجم بطلب التحويل بين الكائنات.

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

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

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

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

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

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

أنظمة النوع المتخصص

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

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

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

مفهوم النوع	تدوين	معنى
وظيفة	$\sigma \to \tau$	إذا و ، إذن . $M:\sigma \to \tau$ $N:\sigma$ $M(N):\tau$
منتج	$\sigma \times \tau$	إذا ، فإن الزوج st و . $M:\sigma \times \tau$ $M=(N,O)$ $N:\sigma$ $O:\tau$
مجموع	$\sigma +\tau$	إذا ، فإن الحقنة الأولى هي st ، أو الحقنة الثانية هي st . $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$ لديها عضو . $M:\langle x:\tau \rangle$ $x:\tau$
متعدد الأشكال	$\forall {}\alpha .\tau$	إذا ، فبالنسبة لأي نوع $σ$ . $M:\forall {}\alpha .\tau$ $M:\tau [\alpha :=\sigma ]$
وجودي	$\exists {}\alpha .\tau$	إذا ، فبالنسبة لبعض أنواع $σ$ . $M:\exists {}\alpha .\tau$ $M:\tau [\alpha :=\sigma ]$
متكرر	$\mu \alpha .\tau$	إذا ، إذن . $M:\mu \alpha .\tau$ $M:\tau [\alpha :=\mu \alpha .\tau ]$
الدالة التابعة ^[أ]	$(x:\sigma )\to \tau$	إذا و ، إذن . $M:(x:\sigma )\to \tau$ $N:\sigma$ $M(N):\tau [x:=N]$
الزوج التابع ^[ب]	$(x:\sigma )\times \tau$	إذا ، فإن الزوج st و . $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$ هي قيم عددية موجبة عشوائية. تم إنشاء متغير من التعلم الآلي يسمى التعلم الآلي التابع بناءً على نظام النوع هذا، ولكن نظرًا لأن فحص النوع للأنواع التابعة التقليدية غير قابل للحسم ، فلا يمكن فحص نوع جميع البرامج التي تستخدمها دون نوع من القيود. يحد التعلم الآلي التابع من نوع المساواة التي يمكنه تحديدها بحسابات بريسبرجر .

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

أنواع خطية

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

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

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

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

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

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

أنواع الاتحاد

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

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

أنواع وجودية

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

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

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

بشكل عام، من المستحيل أن يستنتج مدقق النوع النوع الوجودي الذي تنتمي إليه وحدة معينة. في المثال أعلاه، يمكن أن يكون لـ intT { a: int; f: (int → int); } أيضًا النوع ∃X { a: X; f: (int → 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# يرث من فئة الكائن. بعض اللغات، مثل Java و Raku ، لها نوع جذر ولكنها تحتوي أيضًا على أنواع بدائية ليست كائنات. ^[30] توفر Java أنواع كائنات مغلفة موجودة مع الأنواع البدائية حتى يتمكن المطورون من استخدام أنواع كائنات المغلف أو الأنواع البدائية غير الكائنية الأبسط. يحول Raku تلقائيًا الأنواع البدائية إلى كائنات عند الوصول إلى طرقها. ^[31]

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

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

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

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

انظر أيضا

ملحوظات

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

مراجع

^ بيرس 2002، ص 1: "نظام النوع هو طريقة نحوية قابلة للتطبيق لإثبات غياب سلوكيات معينة للبرنامج من خلال تصنيف العبارات وفقًا لأنواع القيم التي تحسبها."
^ Cardelli 2004، ص 1: "الغرض الأساسي لنظام النوع هو منع حدوث أخطاء التنفيذ أثناء تشغيل البرنامج."
^ بيرس 2002، ص 208.
^ ab Sethi, R. (1996). لغات البرمجة: المفاهيم والإنشاءات (الطبعة الثانية). Addison-Wesley. ص 142. ISBN 978-0-201-59065-4. OCLC 604732680.
^ Nordström, B.; Petersson, K.; Smith, JM (2001). "نظرية النوع لمارتن لوف". البنى الجبرية والمنطقية . دليل المنطق في علوم الكمبيوتر. المجلد 5. مطبعة جامعة أكسفورد. ص 2. رقم ISBN 978-0-19-154627-3.
^ Turner, DA (12 يونيو 2012). "بعض تاريخ لغات البرمجة الوظيفية" (PDF) . محاضرة مدعوة في TFP12، في جامعة سانت أندروز . انظر القسم الخاص بـ Algol 60.
^ "... أي نظام كتابة سليم وقابل للحسم يجب أن يكون غير مكتمل" —D. Remy (2017). ص. 29، Remy, Didier. "أنظمة الكتابة للغات البرمجة" (PDF) . مؤرشف من الأصل (PDF) في 14 نوفمبر 2017. تم الاسترجاع في 26 مايو 2013 .
^ بيرس 2002.
^ abc Skeet, Jon (2019). C# in Depth (4 ed.). Manning. ISBN 978-1617294532.
^ Miglani, Gaurav (2018). "Dynamic Method Dispatch or Runtime Polymorphism in Java". مؤرشف من الأصل في 2020-12-07 . تم الاسترجاع في 2021-03-28 .
^ رايت، أندرو ك. (1995). الطباعة الناعمة العملية (دكتوراه). جامعة رايس. المجلد : 1911/16900.
^ "dynamic (C# Reference)". مكتبة MSDN . Microsoft . تم الاسترجاع في 14 يناير 2014 .
^ "std::any — Rust". doc.rust-lang.org . تم الاسترجاع في 2021-07-07 .
^ ماير، إريك؛ درايتون، بيتر. "الكتابة الثابتة حيثما أمكن، والكتابة الديناميكية عند الحاجة: نهاية الحرب الباردة بين لغات البرمجة" (PDF) . شركة مايكروسوفت .
^ Laucher, Amanda; Snively, Paul (2012). "الأنواع مقابل الاختبارات". InfoQ.
^ Xi, Hongwei (1998). Dependent Types in Practical Programming (PhD). قسم العلوم الرياضية، جامعة كارنيجي ميلون. CiteSeerX 10.1.1.41.548 .
Xi, Hongwei; Pfenning, Frank (1999). "Dependent Types in Practical Programming". Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . 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 .
^ "الوضع الصارم (JavaScript)". MSDN . Microsoft . تم الاسترجاع في 2013-07-17 .
^ "الكتابة الصارمة". دليل PHP: مرجع اللغة: الوظائف .
^ ab Bracha, G. "أنواع قابلة للتوصيل" (PDF) .
^ "بالتأكيد. يُطلق عليه "الكتابة التدريجية"، وأود أن أصفه بأنه عصري..." هل توجد لغة تسمح بالكتابة الثابتة والديناميكية؟ . stackoverflow. 2012.
^ abc Kopylov, Alexei (2003). "التقاطع التابع: طريقة جديدة لتعريف السجلات في نظرية النوع". ندوة معهد مهندسي الكهرباء والإلكترونيات الثامنة عشر حول المنطق في علوم الكمبيوتر . LICS 2003. جمعية IEEE للكمبيوتر. ص. 86-95. CiteSeerX 10.1.1.89.4223 . doi :10.1109/LICS.2003.1210048.
^ Mitchell, John C.; Plotkin, Gordon D. (July 1988). "الأنواع المجردة لها نوع وجودي" (PDF) . برنامج الترجمة التابع لـ ACM. Lang. Syst . 10 (3): 470–502. doi :10.1145/44501.45065. S2CID 1222153.
^ ab Siek, Jeremy (24 مارس 2014). "ما هي الكتابة التدريجية؟".
^ سيك، جيريمي؛ طه، وليد (سبتمبر 2006). الكتابة التدريجية للغات الوظيفية (PDF) . المخطط والبرمجة الوظيفية 2006. جامعة شيكاغو . ص 81-92.
^ باريندريجت ، هينك. ديكرز، ويل؛ ستاتمان ، ريتشارد (20 يونيو 2013). حساب التفاضل والتكامل لامدا مع الأنواع. مطبعة جامعة كامبريدج. ص. 66. ردمك 978-0-521-76614-2.
^ "8.2.4 توحيد نظام النوع". مواصفات لغة C# (الطبعة الخامسة). ECMA. ديسمبر 2017. ECMA-334.
^ "الأنواع الأصلية". توثيق Perl 6 .
^ "الأعداد، § التعبئة التلقائية". وثائق Perl 6 .

قراءة إضافية

Cardelli, Luca ; Wegner, Peter (December 1985). "On Understanding Types, Data Abstraction, and Polymorphism" (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.

روابط خارجية

الوسائط المتعلقة بأنظمة الكتابة على ويكيميديا كومنز
سميث، كريس (2011). "ما الذي يجب معرفته قبل مناقشة أنظمة النوع".

Original text

Rate this translation

Your feedback will be used to help improve Google Translate

[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] Cardelli 2004، ص 1: "الغرض الأساسي لنظام النوع هو منع حدوث أخطاء التنفيذ أثناء تشغيل البرنامج."

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

[Sethi1997-5] Sethi, R. (1996). لغات البرمجة: المفاهيم والإنشاءات (الطبعة الثانية). Addison-Wesley. ص 142. ISBN 978-0-201-59065-4. OCLC 604732680.

[hlcs-6] Nordström, B.; Petersson, K.; Smith, JM (2001). "نظرية النوع لمارتن لوف". البنى الجبرية والمنطقية . دليل المنطق في علوم الكمبيوتر. المجلد 5. مطبعة جامعة أكسفورد. ص 2. رقم ISBN 978-0-19-154627-3.

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

[9] "... أي نظام كتابة سليم وقابل للحسم يجب أن يكون غير مكتمل" —D. Remy (2017). ص. 29، Remy, Didier. "أنظمة الكتابة للغات البرمجة" (PDF) . مؤرشف من الأصل (PDF) في 14 نوفمبر 2017. تم الاسترجاع في 26 مايو 2013 .

[FOOTNOTEPierce2002-10] بيرس 2002.

[Skeet-11] Skeet, Jon (2019). C# in Depth (4 ed.). Manning. ISBN 978-1617294532.

[12] Miglani, Gaurav (2018). "Dynamic Method Dispatch or Runtime Polymorphism in Java". مؤرشف من الأصل في 2020-12-07 . تم الاسترجاع في 2021-03-28 .

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

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

[15] "std::any — Rust". doc.rust-lang.org . تم الاسترجاع في 2021-07-07 .

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

[17] Laucher, Amanda; Snively, Paul (2012). "الأنواع مقابل الاختبارات". InfoQ.

[18] Xi, Hongwei (1998). Dependent Types in Practical Programming (PhD). قسم العلوم الرياضية، جامعة كارنيجي ميلون. CiteSeerX 10.1.1.41.548 .
Xi, Hongwei; Pfenning, Frank (1999). "Dependent Types in Practical Programming". Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . 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] "الوضع الصارم (JavaScript)". MSDN . Microsoft . تم الاسترجاع في 2013-07-17 .

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

[Bracha-24] Bracha, G. "أنواع قابلة للتوصيل" (PDF) .

[25] "بالتأكيد. يُطلق عليه "الكتابة التدريجية"، وأود أن أصفه بأنه عصري..." هل توجد لغة تسمح بالكتابة الثابتة والديناميكية؟ . stackoverflow. 2012.

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

[29] Mitchell, John C.; Plotkin, Gordon D. (July 1988). "الأنواع المجردة لها نوع وجودي" (PDF) . برنامج الترجمة التابع لـ ACM. Lang. Syst . 10 (3): 470–502. doi :10.1145/44501.45065. S2CID 1222153.

[siek-30] Siek, Jeremy (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] "الأنواع الأصلية". توثيق Perl 6 .

[35] "الأعداد، § التعبئة التلقائية". وثائق Perl 6 .

ف ت هـ أنواع البيانات
غير مفسر	قليل بايت تريت تريتي كلمة مصفوفة بت
رقمي	الدقة التعسفية أو البيغنوم معقد عشري نقطة ثابتة نقطة عائمة دقة منخفضة ميني فلوت نصف الدقة بفلوت16 دقة واحدة دقة مزدوجة دقة رباعية دقة الثماني دقة ممتدة طويل مزدوج عدد صحيح التوقيع فاصلة عاقِل
مؤشر	عنوان بدني افتراضي مرجع
نص	شخصية خيط منتهية بـ null
مركب	نوع البيانات الجبرية معمم مصفوفة المصفوفة الترابطية فصل متكل المساواة حثي تقاطع قائمة هدف كائن ميتافيزيقي نوع الخيار منتج سجل أو هيكل التكرير تعيين الاتحاد مُوسَم
آخر	منطقي النوع السفلي مجموعة نوع مُعَدَّد استثناء نوع الوظيفة نوع البيانات غير الشفاف نوع البيانات المتكررة إشارة ضوئية تدفق معرف مكتوب بشكل قوي النوع الأعلى نوع الفئة نوع فارغ نوع الوحدة فارغ
مواضيع ذات صلة	نوع البيانات المجردة ملاكمة هيكل البيانات نوعي عطوف ميتاكلاس تعدد الأشكال البارامترية نوع البيانات البدائي الواجهة التصنيف الفرعي منشئ النوع تحويل النوع نظام النوع نظرية النوع عامل