استنتاج النوع

الموسوعة الحرة

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

يُستخدم مصطلح "قابلية الكتابة" أحيانًا بشكل شبه مرادف لمصطلح "استدلال النوع"، إلا أن بعض المؤلفين يميزون بين قابلية الكتابة كمشكلة قرار (ذات إجابة بنعم/لا) واستدلال النوع كحساب نوع فعلي لمصطلح ما. [ 2 ]

شرح غير تقني

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

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

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

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

هناك عدة طرق يمكن من خلالها تحديد نوع المصطلح:

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

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

التحقق من النوع مقابل استنتاج النوع

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

في هذا السياق، تكتسب الأسئلة التالية أهمية خاصة:

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

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

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

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

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

int increment ( int x ) { int result ; // تعريف متغير عددي resultresult = x + 1 ; return result ; }

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

زيادة ( x ) { متغير النتيجة ؛ // متغير النتيجة من النوع المُستنتج متغير النتيجة2 ؛ // متغير النتيجة2 من النوع المُستنتجresult = x + 1 ; result2 = x + 1.0 ; // هذا السطر لن يعمل (في اللغة المقترحة) return result ; }

هذا مطابق لطريقة كتابة الكود في لغة دارت ، باستثناء أنه يخضع لبعض القيود الإضافية كما هو موضح أدناه. من الممكن استنتاج أنواع جميع المتغيرات أثناء الترجمة. في المثال أعلاه، سيستنتج المترجم أن المتغيرين ` resulta` و` xb` من النوع `integer` لأن الثابت `a` 1من النوع `integer`، وبالتالي فإن ` increment()b` دالة int -> int. أما المتغير ` result2a` فلم يُستخدم بطريقة صحيحة، لذا لن يكون له نوع.

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

مع ذلك، في السطر التالي، result2يتم حساب القيمة بإضافة عدد عشري 1.0باستخدام حسابات الفاصلة العائمة ، مما يُسبب تعارضًا في استخدام النوع xلكل من تعابير الأعداد الصحيحة والفاصلة العائمة. وقد عُرفت خوارزمية استنتاج النوع الصحيحة لمثل هذه الحالة منذ عام ١٩٥٨، وثبتت صحتها منذ عام ١٩٨٢. تعتمد هذه الخوارزمية على الاستنتاجات السابقة وتستخدم النوع الأكثر عمومية منذ البداية: في هذه الحالة، الفاصلة العائمة. لكن هذا قد يُؤدي إلى عواقب وخيمة، فعلى سبيل المثال، قد يُؤدي استخدام الفاصلة العائمة منذ البداية إلى مشاكل في الدقة لم تكن لتحدث مع نوع عدد صحيح.

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

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

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

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

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

الوصف الفني

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

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

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

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

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

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

map f [] = [] map f ( first : rest ) = f first : map f rest

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

يتم استنتاج نوع الدالة mapكما يلي. mapالدالة تأخذ وسيطين، لذا فإن نوعها مقيد بالصيغة `. في لغة هاسكل، تتطابق الأنماط ``` و``` دائمًا مع القوائم، لذا يجب أن يكون الوسيط الثاني من نوع قائمة: ``` لنوع ما `` `. يتم تطبيق وسيطها الأول على الوسيط ``` ، الذي يجب أن يكون من النوع ``` ، وهو ما يتوافق مع النوع في وسيط القائمة، لذا فإن ````` تعني "من النوع ``` لنوع ما ``` . أخيرًا، القيمة المُعادة من ``` هي قائمة من أي شيء ينتج ```` .a->b->c[](first:rest)b=[d]dffirstdf::d->e::emapff[e]

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

map :: ( a -> b ) -> [ a ] ​​-> [ b ]

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

مثال مفصل

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

map f [] = [] map f ( first : rest ) = f first : map f rest

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

مراجع

  1. 1 2 بنجامين سي. بيرس (2002). الأنواع ولغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا. ISBN 978-0-262-16209-8.
  2. ↑ بروتين، م. كلارنس؛ فيريرا، جيلدا (2022). "قابلية الكتابة واستدلال النوع في تعدد الأشكال الذرية". الأساليب المنطقية في علوم الحاسوب 7417. arXiv : 2104.13675 . doi : 10.46298/lmcs-18(3:22)2022 .
  3. ↑ "WG14-N3007: استنتاج النوع لتعريفات الكائنات" . open-std.org . 2022-06-10. مؤرشف من الأصل في 24 ديسمبر 2022.
  4. ↑ "محددات أنواع العناصر النائبة (منذ C++11) - cppreference.com" . en.cppreference.com . تم الاطلاع عليه بتاريخ 15 أغسطس 2021 .
  5. ↑ "نظام أنواع لغة دارت" . dart.dev . تم الاطلاع عليه بتاريخ 21-11-2020 .
  6. ↑ كارترمب. "استنتاج النوع - F#" . docs.microsoft.com . تم الاسترجاع في 21-11-2020 .
  7. ↑ "الاستدلال · لغة جوليا" . docs.julialang.org . تم الاطلاع عليه بتاريخ 21-11-2020 .
  8. ↑ "مواصفات لغة كوتلين" . kotlinlang.org . تم الاطلاع عليه بتاريخ 28-06-2021 .
  9. ↑ "العبارات - مرجع لغة Rust" . doc.rust-lang.org . تم الاطلاع عليه بتاريخ 28-06-2021 .
  10. ↑ "استنتاج النوع" . وثائق سكالا . تم الاطلاع عليه بتاريخ 21-11-2020 .
  11. ↑ "الأساسيات - لغة برمجة سويفت (سويفت 5.5)" . docs.swift.org . تم الاطلاع عليه بتاريخ 28-06-2021 .
  12. ↑ "التوثيق - استنتاج النوع" . www.typescriptlang.org . تم الاطلاع عليه بتاريخ 21-11-2020 .
  13. ↑ "Projects/Vala/Tutorial - GNOME Wiki!" . wiki.gnome.org . تم الاطلاع عليه بتاريخ 28-06-2021 .
  14. ↑ كاثلين دولارد. "استنتاج النوع المحلي - فيجوال بيسك" . docs.microsoft.com . تم الاسترجاع في 28-06-2021 .
  15. ↑ برايان أوسوليفان؛ دون ستيوارت؛ جون غورزن (2008). "الفصل 25. تحليل الأداء والتحسين" . هاسكل في العالم الحقيقي . أورايلي.
  16. ↑ تالبين، جان بيير، وبيير جوفيلو. " النوع متعدد الأشكال، والمنطقة، والاستدلال على التأثير ". مجلة البرمجة الوظيفية 2.3 (1992): 245-271.
  17. ↑ حسن، مصطفى؛ أوربان، كاترينا؛ إيلرز، ماركو؛ مولر، بيتر (2018). "استدلال النوع القائم على MaxSMT للغة بايثون 3" . التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 10982. الصفحات 12-19 . doi : 10.1007/978-3-319-96142-2_2 . ISBN   978-3-319-96141-5.
  18. 1 2 داماس، لويس؛ ميلنر، روبن ( 1982)، "مخططات الأنواع الرئيسية للبرامج الوظيفية"، POPL '82: وقائع الندوة التاسعة لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة (PDF) ، ACM، الصفحات 207-212 
  19. ↑ ميلنر، روبن (1978)، "نظرية تعدد الأشكال في البرمجة"، مجلة علوم الحاسوب والنظم ، 17 (3): 348-375 ، doi : 10.1016/0022-0000(78)90014-4 ، hdl : 20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66
  20. ↑ مركز الذكاء الاصطناعي. تحليل وتفسير أنواع اللغات الطبيعية ولغات الحاسوب . مؤرشف بتاريخ 4 يوليو 2012 في أرشيف الإنترنت . أطروحة دكتوراه، جامعة ستانفورد، 1989.
  21. ↑ إيميلي، مارتن سي، وريمي زاجاك. " قواعد التوحيد المكتوبة " مؤرشفة في 2018-02-05 على Wayback Machine . وقائع المؤتمر الثالث عشر حول اللغويات الحاسوبية - المجلد 3. رابطة اللغويات الحاسوبية، 1990.
  22. ↑ باريسكي، ريمو. " تحليل اللغة الطبيعية الموجه بالنوع ." (1988).
  23. ↑ فيشر، كاثلين، وآخرون. " من التراب إلى المجارف: توليد أدوات تلقائي بالكامل من بيانات مخصصة ." إشعارات ACM SIGPLAN. المجلد 43. العدد 1. ACM، 2008.
  24. ↑ لابين، شالوم؛ شيبر، ستيوارت م. (2007). "نظرية وتطبيق التعلم الآلي كمصدر لفهم القواعد النحوية العالمية" (ملف PDF) . مجلة اللغويات . 43 (2): 393-427 . doi : 10.1017/s0022226707004628 . S2CID 215762538 . 
  25. ↑ ستيوارت م. شيبر (1992). قواعد نحوية رسمية قائمة على القيود: تحليل نحوي واستنتاج أنواع للغات الطبيعية ولغات الحاسوب . مطبعة معهد ماساتشوستس للتكنولوجيا. ISBN 978-0-262-19324-5.

!-- فئات مخفية أدناه -->