استدلال النوع

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

شرح غير تقني

في لغة مكتوبة، يحدد نوع المصطلح الطرق التي يمكن أو لا يمكن استخدامه بها في تلك اللغة. على سبيل المثال، ضع في اعتبارك اللغة الإنجليزية والمصطلحات التي يمكن أن تملأ الفراغ في عبارة "sing _". مصطلح "a song" من النوع القابل للغناء، لذا يمكن وضعه في الفراغ لتكوين عبارة ذات معنى: "sing a song". من ناحية أخرى، لا يحتوي مصطلح "a friend" على النوع القابل للغناء، لذا فإن "sing a friend" عبارة هراء. في أفضل الأحوال قد يكون استعارة؛ إن ثني قواعد النوع هو سمة من سمات اللغة الشعرية.

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

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

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

هناك عدة طرق يمكن أن يحصل بها المصطلح على نوعه:

قد يتم توفير النوع من مكان خارج المقطع. على سبيل المثال، إذا أشار المتحدث إلى "أغنية" باللغة الإنجليزية، فإنه لا يتعين عليه عمومًا إخبار المستمع بأن "الأغنية" قابلة للغناء والتأليف؛ فهذه المعلومات جزء من الخلفية المعرفية المشتركة بينهما.
يمكن إعلان النوع صراحةً. على سبيل المثال، قد يكتب المبرمج عبارة مثل تلك الموجودة delay: seconds := 4في الكود الخاص به، حيث تكون النقطتان هي الرمز الرياضي التقليدي لتمييز المصطلح بنوعه. أي أن هذه العبارة لا تحدد delayالقيمة فقط 4، بل delay: secondsيشير الجزء أيضًا إلى أن delayنوع 's هو مقدار الوقت بالثواني.
يمكن استنتاج النوع من السياق. على سبيل المثال، في عبارة "اشتريته مقابل أغنية"، يمكننا أن نلاحظ أن محاولة إعطاء المصطلح "أغنية" أنواعًا مثل "قابل للغناء" و"قابل للتأليف" من شأنها أن تؤدي إلى هراء، في حين أن النوع "كمية من العملة" يعمل بشكل صحيح. لذلك، دون الحاجة إلى إخبارنا، نستنتج أن "الأغنية" هنا يجب أن تعني "القليل إلى لا شيء"، كما في المثل الإنجليزي " for a song "، وليس "قطعة موسيقية، عادةً ما تكون بكلمات".

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

التحقق من النوع مقابل الاستدلال على النوع

في الكتابة، يكون التعبير E معارضًا للنوع T، والذي يُكتب رسميًا على هيئة E : T. وعادةً ما يكون للكتابة معنى فقط في سياق ما، وهو ما تم حذفه هنا.

وفي هذا الإطار، تكتسب الأسئلة التالية أهمية خاصة:

E : T؟ في هذه الحالة، يتم إعطاء كل من التعبير E والنوع T. الآن، هل E هو T حقًا؟ يُعرف هذا السيناريو باسم فحص النوع .
E : _؟ هنا، فقط التعبير هو المعروف. إذا كانت هناك طريقة لاستنتاج نوع لـ E، فسنكون قد أنجزنا استنباط النوع .
_ : T؟ على العكس من ذلك. إذا أعطينا نوعًا واحدًا فقط، فهل هناك أي تعبير له أم أن النوع لا يحتوي على أي قيم؟ هل هناك أي مثال على T؟ يُعرف هذا باسم استيطان النوع .

بالنسبة لحساب لامدا المكتوب بطريقة بسيطة ، يمكن حل جميع الأسئلة الثلاثة . ولكن الوضع ليس مريحًا عندما يُسمح بأنواع أكثر تعبيرًا .

أنواع في لغات البرمجة

الأنواع هي ميزة موجودة في بعض اللغات ذات النوع الثابت القوي . وغالبًا ما تكون سمة مميزة للغات البرمجة الوظيفية بشكل عام. تتضمن بعض اللغات التي تتضمن استدلال النوع C23 ، ^[2]C++11 ، ^[3]C# (بدءًا من الإصدار 3.0)، Chapel ، Clean ، Crystal ، D ، F# ، ^[4]FreeBASIC ، Go ، Haskell ، Java (بدءًا من الإصدار 10)، Julia ، ^[5]Kotlin ، ^[6]ML ، Nim ، OCaml ، Opa ، Q#، RPython ، Rust ، ^[7]Scala ، ^[8]Swift ، ^[9]TypeScript ، ^[10]Vala ، ^[11]Dart ، ^[12] و Visual Basic ^[13] (بدءًا من الإصدار 9.0). تستخدم غالبيتها شكلًا بسيطًا من استدلال النوع؛ يمكن لنظام نوع Hindley-Milner توفير استدلال نوع أكثر اكتمالاً. إن القدرة على استنتاج الأنواع تلقائيًا تجعل العديد من مهام البرمجة أسهل، مما يترك للمبرمج حرية حذف تعليقات النوع مع السماح له بالتحقق من النوع.

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

int add_one ( int x ) { int النتيجة ؛ /* إعلان النتيجة الصحيحة */   
      

    النتيجة = x + 1 ؛ إرجاع النتيجة ؛ }

إن توقيع تعريف هذه الدالة، int add_one(int x), يعلن أن add_oneهي دالة تأخذ وسيطة واحدة، وهي عدد صحيح ، وتعيد عددًا صحيحًا. int result;يعلن أن المتغير المحلي resultهو عدد صحيح. في لغة افتراضية تدعم الاستدلال النوعي، يمكن كتابة الكود على هذا النحو بدلاً من ذلك:

add_one ( x ) { var result ؛ /* نتيجة متغير من النوع المستنتج */ var result2 ؛ /* نتيجة متغير من النوع المستنتج #2 */ 
       
      

    النتيجة = x + 1 ؛ النتيجة2 = x + 1.0 ؛ /* هذا السطر لن يعمل (في اللغة المقترحة) */ إرجاع النتيجة ؛ }

هذا مماثل لكيفية كتابة الكود بلغة Dart ، إلا أنه يخضع لبعض القيود المضافة كما هو موضح أدناه. سيكون من الممكن استنتاج أنواع جميع المتغيرات في وقت التجميع. في المثال أعلاه، سيستنتج المترجم ذلك resultويكون xله نوع عدد صحيح لأن الثابت 1هو نوع عدد صحيح، وبالتالي فهو add_oneدالة int -> int. لا يتم استخدام المتغير result2بطريقة قانونية، لذلك لن يكون له نوع.

في اللغة التخيلية التي كُتب بها المثال الأخير، يفترض المترجم أنه في حالة عدم وجود معلومات تشير إلى العكس، فإنه +يأخذ عددين صحيحين ويعيد عددًا صحيحًا واحدًا. (وهكذا يعمل الأمر في OCaml على سبيل المثال ). ومن هذا، يمكن لمستنتج النوع أن يستنتج أن نوع x + 1هو عدد صحيح، مما يعني resultأنه عدد صحيح وبالتالي فإن قيمة الإرجاع لـ add_oneهو عدد صحيح. وبالمثل، يتطلب since +أن تكون كل من حجتيه من نفس النوع، xويجب أن يكون عددًا صحيحًا، وبالتالي، add_oneيقبل عددًا صحيحًا واحدًا كحجة.

ومع ذلك، في السطر التالي، يتم حساب النتيجة2 عن طريق إضافة عدد عشري 1.0مع حساب الفاصلة العائمة ، مما يتسبب في تعارض في استخدام xلكل من التعبيرات الصحيحة والفاصلة العائمة. كانت خوارزمية الاستدلال على النوع الصحيحة لمثل هذا الموقف معروفة منذ عام 1958 ومن المعروف أنها صحيحة منذ عام 1982. إنها تعيد النظر في الاستدلالات السابقة وتستخدم النوع الأكثر عمومية من البداية: في هذه الحالة الفاصلة العائمة. ومع ذلك، يمكن أن يكون لهذا آثار ضارة، على سبيل المثال، يمكن أن يؤدي استخدام الفاصلة العائمة من البداية إلى إدخال مشكلات في الدقة لم تكن لتوجد مع نوع عدد صحيح.

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

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

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

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

إصدار يقبل إدخال عدد صحيح ويستخدم تحويل النوع الضمني.

إصدار يقبل رقمًا فاصلًا عائمًا كمدخل ويستخدم تعليمات الفاصلة العائمة في جميع الأنحاء.

الوصف الفني

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

للحصول على المعلومات المطلوبة لاستنتاج نوع تعبير، يقوم المترجم إما بجمع هذه المعلومات كمجموع واختزال لاحق لتعليقات النوع المعطاة لتعبيراته الفرعية، أو من خلال فهم ضمني لنوع القيم الذرية المختلفة (على سبيل المثال true: Bool؛ 42: Integer؛ 3.14159: Real؛ إلخ). ومن خلال التعرف على الاختزال النهائي للتعبيرات إلى قيم ذرية مكتوبة ضمنيًا، يتمكن المترجم للغة استنتاج النوع من تجميع برنامج تمامًا دون تعليقات النوع.

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

تعتمد بعض طرق استنباط النوع على نظريات إرضاء القيود ^[15] أو نظريات قابلية الإرضاء ^[16] .

مثال رفيع المستوى

على سبيل المثال، تطبق دالة Haskellmap دالة على كل عنصر من عناصر القائمة، ويمكن تعريفها على النحو التالي:

الخريطة f [] = [] الخريطة f ( الأولى : الباقية ) = f الأولى : الخريطة f الباقية

(تذكر أنه :في Haskell يشير إلى cons ، وهو هيكلة عنصر الرأس وذيل القائمة في قائمة أكبر أو تفكيك قائمة غير فارغة إلى عنصر الرأس وذيلها. ولا يشير إلى "من النوع" كما هو الحال في الرياضيات وفي أماكن أخرى في هذه المقالة؛ في Haskell يتم كتابة عامل "من النوع" ::بدلاً من ذلك.)

تتم عملية الاستدلال على mapالنوع في الدالة على النحو التالي. mapهي دالة ذات وسيطتين، لذا فإن نوعها مقيد بأن يكون من النموذج . في Haskell، تتطابق الأنماط و دائمًا مع القوائم، لذا يجب أن تكون الوسيطة الثانية من نوع القائمة: لبعض الأنواع . يتم تطبيق وسيطتها الأولى على الوسيطة ، والتي يجب أن يكون لها type ، المطابق للنوع في وسيطة القائمة، so ( تعني "من النوع") لبعض الأنواع . قيمة الإرجاع لـ ، أخيرًا، هي قائمة بكل ما ينتج، so . a -> b -> c[](first:rest)b = [d]dffirstdf :: d -> e::emap ff[e]

يؤدي تجميع الأجزاء معًا إلى . لا يوجد شيء خاص بشأن متغيرات النوع، لذا يمكن إعادة تسميتها باسم map :: (d -> e) -> [d] -> [e]

الخريطة :: ( أ -> ب ) -> [ أ ] -> [ ب ]

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

مثال تفصيلي

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

الخريطة f [] = [] الخريطة f ( الأولى : الباقية ) = f الأولى : الخريطة f الباقية

(مرة أخرى، تذكر أن :هنا هو منشئ قائمة Haskell، وليس عامل "of type"، والذي تكتبه Haskell بدلاً من ذلك ::.)

أولاً، نقوم بإنشاء متغيرات نوع جديدة لكل مصطلح فردي:

αيجب أن يشير إلى نوع mapما نريد استنتاجه.
βيجب أن يشير إلى نوع fالمعادلة الأولى.
[γ]يجب أن يشير إلى نوع []على الجانب الأيسر من المعادلة الأولى.
[δ]يجب أن يشير إلى نوع []على الجانب الأيمن من المعادلة الأولى.
εيجب أن يشير إلى نوع fالمعادلة الثانية.
ζ -> [ζ] -> [ζ]يجب أن يشير إلى نوع :الجانب الأيسر من المعادلة الأولى. (هذا النمط معروف من تعريفه.)
ηيجب أن يشير إلى نوع first.
θيجب أن يشير إلى نوع rest.
ι -> [ι] -> [ι]يجب أن يشير إلى نوع :على الجانب الأيمن من المعادلة الأولى.

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

κيجب أن يشير إلى نوع . نستنتج أنه حيث يعني الرمز "مشابه" "يتحد مع"؛ فإننا نقول أن نوع , يجب أن يكون متوافقًا مع نوع الدالة التي تأخذ a وقائمة من s وتعيد a .map f []α ~ β -> [γ] -> κ~αmapβγκ
λيجب أن تشير إلى نوع . نستنتج أن .(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
μيجب أن تشير إلى نوع . نستنتج أن .map f (first:rest)α ~ ε -> λ -> μ
νيجب أن تشير إلى نوع . نستنتج أن .f firstε ~ η -> ν
ξيجب أن تشير إلى نوع . نستنتج أن .map f restα ~ ε -> θ -> ξ
οيجب أن تشير إلى نوع . نستنتج أن .f first : map f restι -> [ι] -> [ι] ~ ν -> ξ -> ο

نقوم أيضًا بتقييد الجانبين الأيسر والأيمن لكل معادلة للتوحيد مع بعضهما البعض: κ ~ [δ]و μ ~ ο. في المجمل، نظام التوحيدات المطلوب حله هو:

α ~ β -> [γ] -> κ
ζ -> [ζ] -> [ζ] ~ η -> θ -> α
α ~ ε -> λ -> μ
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο
ك ~ [δ]
μ ~ ο

ثم نستبدل حتى لا يمكن إزالة أي متغيرات أخرى. الترتيب الدقيق غير مهم؛ إذا تم التحقق من نوع الكود، فإن أي ترتيب سيؤدي إلى نفس الشكل النهائي. دعنا نبدأ باستبدال οfor μو [δ]for κ:

α ~ β -> [γ] -> [δ]
ζ -> [ζ] -> [ζ] ~ η -> θ -> α
α ~ ε -> λ -> ο
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο

الاستبدال ζبـ η، [ζ]و ، θو ، و ، و ، كلها ممكنة لأن منشئ النوع مثل قابل للعكس في وسيطاته: λιν[ι]ξο· -> ·

α ~ β -> [γ] -> [δ]
α ~ ε -> [ζ] -> [ι]
ε ~ ζ -> ι

استبدال و ζ -> ιبـ ، مع الحفاظ على القيد الثاني حتى نتمكن من الاسترداد في النهاية: εβ -> [γ] -> [δ]αα

α ~ (ζ -> ι) -> [ζ] -> [ι]
β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι]

وأخيرًا، يؤدي استبدال (ζ -> ι)كل من for و βwell و for لأن منشئ النوع مثل قابل للعكس إلى إزالة جميع المتغيرات الخاصة بالقيد الثاني: ζγιδ[·]

α ~ (ζ -> ι) -> [ζ] -> [ι]

لم يعد من الممكن إجراء أي استبدالات، وإعادة التسمية تعطينا نفس النتيجة التي وجدناها دون الخوض في هذه التفاصيل. map :: (a -> b) -> [a] -> [b]

خوارزمية الاستدلال من نوع هندلي-ميلنر

الخوارزمية التي استخدمت لأول مرة لإجراء استدلال النوع تسمى الآن بشكل غير رسمي خوارزمية هندلي-ميلنر، على الرغم من أنه يجب أن تُنسب الخوارزمية بشكل صحيح إلى داماس وميلنر. ^[17] كما يُطلق عليها تقليديًا إعادة بناء النوع . ^[1]^{: 320} إذا تم كتابة المصطلح جيدًا وفقًا لقواعد كتابة هندلي-ميلنر، فإن القواعد تولد كتابة رئيسية للمصطلح. عملية اكتشاف هذه الكتابة الرئيسية هي عملية "إعادة البناء".

أصل هذه الخوارزمية هو خوارزمية الاستدلال على النوع لحساب لامدا المكتوب ببساطة والتي ابتكرها هاسكل كاري وروبرت فيز في عام 1958. ^{[ بحاجة لمصدر ]} في عام 1969، وسع جيه روجر هندلي هذا العمل وأثبت أن خوارزميتهم استنتجت دائمًا النوع الأكثر عمومية. في عام 1978، قدم روبن ميلنر ، ^[18] بشكل مستقل عن عمل هندلي، خوارزمية مكافئة، وهي الخوارزمية W. في عام 1982، أثبت لويس داماس ^[17] أخيرًا أن خوارزمية ميلنر كاملة ووسعها لدعم الأنظمة ذات المراجع المتعددة الأشكال.

الآثار الجانبية لاستخدام النوع الأكثر عمومية

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

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

استدلال النوع للغات الطبيعية

تم استخدام خوارزميات استنتاج النوع لتحليل اللغات الطبيعية وكذلك لغات البرمجة. ^[19]^[20]^[21] تُستخدم خوارزميات استنتاج النوع أيضًا في بعض أنظمة الاستدلال النحوي ^[22]^[23] وأنظمة القواعد النحوية القائمة على القيود للغات الطبيعية. ^[24]

مراجع

^ ab Benjamin C. Pierce (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.
^ "WG14-N3007 : استدلال النوع لتعريفات الكائنات". open-std.org . 2022-06-10. مؤرشف من الأصل في 24 ديسمبر 2022.
^ "محددات نوع العنصر النائب (منذ C++11) - cppreference.com". en.cppreference.com . تم الاسترجاع في 2021-08-15 .
^ cartermp. "استدلال النوع - F#". docs.microsoft.com . تم الاسترجاع في 2020-11-21 .
^ "الاستدلال · لغة جوليا". docs.julialang.org . تم الاسترجاع في 2020-11-21 .
^ "مواصفات لغة Kotlin". kotlinlang.org . تم الاسترجاع في 2021-06-28 .
^ "العبارات - مرجع Rust". doc.rust-lang.org . تم الاسترجاع في 2021-06-28 .
^ "استدلال النوع". توثيق سكالا . تم الاسترجاع في 2020-11-21 .
^ "الأساسيات — لغة البرمجة سويفت (سويفت 5.5)". docs.swift.org . تم الاسترجاع في 2021-06-28 .
^ "التوثيق - استدلال النوع". www.typescriptlang.org . تم الاسترجاع في 2020-11-21 .
^ "مشاريع/فالا/دروس تعليمية - ويكي جنوم!". wiki.gnome.org . تم الاسترجاع في 2021-06-28 .
^ "نظام نوع دارت". dart.dev . تم الاسترجاع في 2020-11-21 .
^ KathleenDollard. "استدلال النوع المحلي - Visual Basic". docs.microsoft.com . تم الاسترجاع في 2021-06-28 .
^ برايان أوسوليفان؛ دون ستيوارت؛ جون جورزين (2008). "الفصل 25. تحديد الملفات الشخصية والتحسين". هاسكل في العالم الحقيقي . أوريلي.
^ تالبين، جان بيير، وبيير جوفيلوت. "استدلال النوع المتعدد الأشكال والمنطقة والتأثير". مجلة البرمجة الوظيفية 2.3 (1992): 245-271.
^ حسن، مصطفى؛ أوربان، كاترينا؛ إيلرز، ماركو؛ مولر، بيتر (2018). "استدلال النوع القائم على MaxSMT لـ Python 3". التحقق بمساعدة الكمبيوتر . مذكرات محاضرات في علوم الكمبيوتر. المجلد 10982. ص 12-19. doi :10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5.
^ ab Damas, Luis; Milner, Robin (1982), "Principal type-schemes for function programs", POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on principles of programming language (PDF) , ACM, pp. 207–212
^ ميلنر، روبن (1978)، "نظرية تعدد أشكال النوع في البرمجة"، مجلة علوم الحاسب والنظام ، 17 (3): 348-375، doi : 10.1016/0022-0000(78)90014-4 ، hdl : 20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66
^ مركز الذكاء الاصطناعي. التحليل والاستدلال على النوع للغات الطبيعية والحاسوبية محفوظ في 2012-07-04 على موقع واي باك مشين . أطروحة. جامعة ستانفورد، 1989.
^ إيميلي، مارتن سي، وريمي زاجاك. "قواعد توحيد الكتابة المؤرشفة في 2018-02-05 على موقع واي باك مشين ." وقائع المؤتمر الثالث عشر حول اللغويات الحاسوبية - المجلد 3. جمعية اللغويات الحاسوبية، 1990.
^ باريسكي، ريمو. "تحليل اللغة الطبيعية المعتمد على النوع". (1988).
^ فيشر، كاثلين، وآخرون. "فيشر، كاثلين، وآخرون. "من التراب إلى المجارف: توليد أدوات أوتوماتيكي بالكامل من بيانات مخصصة." إشعارات ACM SIGPLAN. المجلد 43. العدد 1. ACM، 2008." إشعارات ACM SIGPLAN. المجلد 43. العدد 1. ACM، 2008.
^ لابين، شالوم؛ شيبر، ستيوارت م. (2007). "نظرية التعلم الآلي وممارسته كمصدر للرؤية الثاقبة في القواعد النحوية الشاملة" (PDF) . مجلة اللغويات . 43 (2): 393-427. doi :10.1017/s0022226707004628. S2CID 215762538.
^ ستيوارت م. شيبر (1992). قواعد النحو القائمة على القيود: التحليل والاستدلال على النوع للغات الطبيعية والحاسوبية. مطبعة معهد ماساتشوستس للتكنولوجيا. رقم ISBN 978-0-262-19324-5.

روابط خارجية

رسالة بريد إلكتروني مؤرشفة بقلم روجر هندلي، تشرح تاريخ استدلال النوع
يقدم كتاب استدلال النوع المتعدد الأشكال لمايكل شوارتزباخ نظرة عامة حول استدلال النوع المتعدد الأشكال.
ورقة بحثية عن فحص النوع الأساسي بقلم لوكا كارديلي، تصف الخوارزمية، وتتضمن التنفيذ في Modula-2
تنفيذ الاستدلال من نوع هندلي-ميلنر في سكالا ، بقلم أندرو فورست (تم استرجاعه في 30 يوليو 2009)
تنفيذ Hindley-Milner في Perl 5، بقلم نيكيتا بوريسوف في Wayback Machine (تم أرشفته في 18 فبراير 2007)
ما هو هندلي-ميلنر؟ (ولماذا هو رائع؟) يشرح هندلي-ميلنر، أمثلة في سكالا

Original text

Rate this translation

Your feedback will be used to help improve Google Translate

[TAPL-1] Benjamin C. Pierce (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.

[2] "WG14-N3007 : استدلال النوع لتعريفات الكائنات". open-std.org . 2022-06-10. مؤرشف من الأصل في 24 ديسمبر 2022.

[3] "محددات نوع العنصر النائب (منذ C++11) - cppreference.com". en.cppreference.com . تم الاسترجاع في 2021-08-15 .

[4] rtermp. "استدلال النوع - F#". docs.microsoft.com . تم الاسترجاع في 2020-11-21 .

[5] "الاستدلال · لغة جوليا". docs.julialang.org . تم الاسترجاع في 2020-11-21 .

[6] "مواصفات لغة Kotlin". kotlinlang.org . تم الاسترجاع في 2021-06-28 .

[7] "العبارات - مرجع Rust". doc.rust-lang.org . تم الاسترجاع في 2021-06-28 .

[8] "استدلال النوع". توثيق سكالا . تم الاسترجاع في 2020-11-21 .

[9] "الأساسيات — لغة البرمجة سويفت (سويفت 5.5)". docs.swift.org . تم الاسترجاع في 2021-06-28 .

[10] "التوثيق - استدلال النوع". www.typescriptlang.org . تم الاسترجاع في 2020-11-21 .

[11] "مشاريع/فالا/دروس تعليمية - ويكي جنوم!". wiki.gnome.org . تم الاسترجاع في 2021-06-28 .

[12] "نظام نوع دارت". dart.dev . تم الاسترجاع في 2020-11-21 .

[13] KathleenDollard. "استدلال النوع المحلي - Visual Basic". docs.microsoft.com . تم الاسترجاع في 2021-06-28 .

[14] برايان أوسوليفان؛ دون ستيوارت؛ جون جورزين (2008). "الفصل 25. تحديد الملفات الشخصية والتحسين". هاسكل في العالم الحقيقي . أوريلي.

[15] تالبين، جان بيير، وبيير جوفيلوت. "استدلال النوع المتعدد الأشكال والمنطقة والتأثير". مجلة البرمجة الوظيفية 2.3 (1992): 245-271.

[16] حسن، مصطفى؛ أوربان، كاترينا؛ إيلرز، ماركو؛ مولر، بيتر (2018). "استدلال النوع القائم على MaxSMT لـ Python 3". التحقق بمساعدة الكمبيوتر . مذكرات محاضرات في علوم الكمبيوتر. المجلد 10982. ص 12-19. doi :10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5.

[Damas-and-Milner-1982-17] Damas, Luis; Milner, Robin (1982), "Principal type-schemes for function programs", POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on principles of programming language (PDF) , ACM, pp. 207–212

[18] ميلنر، روبن (1978)، "نظرية تعدد أشكال النوع في البرمجة"، مجلة علوم الحاسب والنظام ، 17 (3): 348-375، doi : 10.1016/0022-0000(78)90014-4 ، hdl : 20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66

[19] مركز الذكاء الاصطناعي. التحليل والاستدلال على النوع للغات الطبيعية والحاسوبية محفوظ في 2012-07-04 على موقع واي باك مشين . أطروحة. جامعة ستانفورد، 1989.

[20] إيميلي، مارتن سي، وريمي زاجاك. "قواعد توحيد الكتابة المؤرشفة في 2018-02-05 على موقع واي باك مشين ." وقائع المؤتمر الثالث عشر حول اللغويات الحاسوبية - المجلد 3. جمعية اللغويات الحاسوبية، 1990.

[21] باريسكي، ريمو. "تحليل اللغة الطبيعية المعتمد على النوع". (1988).

[22] فيشر، كاثلين، وآخرون. "فيشر، كاثلين، وآخرون. "من التراب إلى المجارف: توليد أدوات أوتوماتيكي بالكامل من بيانات مخصصة." إشعارات ACM SIGPLAN. المجلد 43. العدد 1. ACM، 2008." إشعارات ACM SIGPLAN. المجلد 43. العدد 1. ACM، 2008.

[23] لابين، شالوم؛ شيبر، ستيوارت م. (2007). "نظرية التعلم الآلي وممارسته كمصدر للرؤية الثاقبة في القواعد النحوية الشاملة" (PDF) . مجلة اللغويات . 43 (2): 393-427. doi :10.1017/s0022226707004628. S2CID 215762538.

[Shieber1992-24] ستيوارت م. شيبر (1992). قواعد النحو القائمة على القيود: التحليل والاستدلال على النوع للغات الطبيعية والحاسوبية. مطبعة معهد ماساتشوستس للتكنولوجيا. رقم ISBN 978-0-262-19324-5.

اللغة	العربية (RTL)
روابط موسوعية	30 رابطاً
المصدر الأصلي	ويكيبيديا ↗