نظام هيندلي-ميلنر للأنواع

في حساب التفاضل والتكامل اللامدا ذي الأنواع البسيطة ، تكون الأنواع T إما ثوابت من النوع الذري أو أنواع دوال من الشكل${\displaystyle T\rightarrow T}$تُعتبر هذه الأنواع أحادية الشكل . ومن الأمثلة النموذجية عليها الأنواع المستخدمة في القيم الحسابية:

${\displaystyle {\begin{array}{ll}3&:{\mathtt {Number}}\\{\mathtt {add}}\ 3\ 4&:{\mathtt {Number}}\\{\mathtt {add}}&:{\mathtt {Number}}\rightarrow {\mathtt {Number}}\rightarrow {\mathtt {Number}}\end{array}}}$

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

${\displaystyle {\mathtt {id}}\equiv \lambda xx}$

والتي ببساطة تُعيد القيمة التي تُطبق عليها. ومن الأمثلة الأقل وضوحًا الأنواع ذات المعاملات مثل القوائم .

بينما يعني تعدد الأشكال عمومًا أن العمليات تقبل قيمًا من أكثر من نوع واحد، فإن تعدد الأشكال المستخدم هنا هو تعدد أشكال معياري. نجد في المراجع أيضًا تدوينًا لأنظمة الأنواع ، مما يؤكد الطبيعة المعيارية لتعدد الأشكال. بالإضافة إلى ذلك، يمكن تحديد أنواع الثوابت باستخدام متغيرات أنواع (مُكمَّمة). على سبيل المثال، تُكمِّم أنظمة الأنواع التالية بشكل شامل على${\displaystyle \alpha }$وهذا يعني أنها صحيحة لجميع الاحتمالات الممكنة${\displaystyle \alpha }$:

${\displaystyle {\begin{array}{ll}{\mathtt {cons}}&:\forall \alpha .\alpha \rightarrow {\mathtt {List}}\ \alpha \rightarrow {\mathtt {List}}\ \alpha \\{\mathtt {nil}}&:\forall \alpha .{\mathtt {List}}\ \alpha \\{\mathtt {id}}&:\forall \alpha .\alpha \rightarrow \alpha \end{array}}}$

يمكن تحويل الأنواع متعددة الأشكال إلى أنواع أحادية الشكل عن طريق الاستبدال المتسق لمتغيراتها. ومن أمثلة الأنواع أحادية الشكل ما يلي:

${\displaystyle {\begin{array}{ll}{\mathtt {id}}'&:{\mathtt {String}}\rightarrow {\mathtt {String}}\\{\mathtt {nil}}'&:{\mathtt {List}}\ {\mathtt {Number}}\end{array}}}$

وبشكل عام، تكون الأنواع متعددة الأشكال عندما تحتوي على متغيرات النوع، بينما تكون الأنواع التي لا تحتوي عليها أحادية الشكل.

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

عند توسيع نطاق استنتاج النوع لحساب لامدا ذي النوع البسيط ليشمل تعدد الأشكال، يجب تحديد ما إذا كان من المقبول إسناد نوع متعدد الأشكال ليس فقط كنوع للتعبير، بل أيضًا كنوع لمتغير مرتبط بـ λ. وهذا من شأنه أن يسمح بإسناد نوع الهوية العام للمتغير 'id' في:

(λ id . ... (id 3) ... (id "text") ... ) (λ x . x)

يؤدي السماح بذلك إلى ظهور حساب لامدا متعدد الأشكال ؛ ومع ذلك، فإن استنتاج النوع في هذا النظام غير قابل للتقرير. ^{[ 5 ]} بدلاً من ذلك، يميز HM بين المتغيرات المرتبطة مباشرةً بتعبير ما والمتغيرات الأكثر عمومية المرتبطة بـ λ، ويطلق على الأولى اسم المتغيرات المرتبطة بـ let، ويسمح بتعيين أنواع متعددة الأشكال لهذه المتغيرات فقط. يؤدي هذا إلى تعدد الأشكال let حيث يأخذ المثال أعلاه الشكل التالي:

let id = λ x . x in ... (id 3) ... (id "text") ...

والتي يمكن تحديد نوعها بنوع متعدد الأشكال لـ 'id'. وكما هو موضح، تم توسيع صيغة التعبير لجعل المتغيرات المرتبطة بـ let صريحة، ومن خلال تقييد نظام النوع للسماح فقط للمتغيرات المرتبطة بـ let بأن يكون لها أنواع متعددة الأشكال، بينما يجب أن تحصل المعلمات في تجريدات lambda على نوع أحادي الشكل، يصبح استنتاج النوع قابلاً للتقرير.

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

تنقسم الأنواع نحويًا إلى مجموعتين، الأنواع الأحادية والأنواع المتعددة. ^{[ ملاحظة 2 ]}

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

على سبيل المثال، الهوية${\displaystyle \lambda x.x}$يمكن أن يكون${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$وكذلك نوعها ${\displaystyle {\texttt {string}}\rightarrow {\texttt {string}}}$أو${\displaystyle {\texttt {int}}\rightarrow {\texttt {int}}}$وغيرهم كثيرون، ولكن ليس${\displaystyle {\texttt {int}}\rightarrow {\texttt {string}}}$النوع الأكثر عمومية لهذه الدالة هو ${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$أما الأنواع الأخرى فهي أكثر تحديدًا ويمكن اشتقاقها من النوع العام عن طريق استبدال نوع آخر بمعامل النوع بشكل متسق ، أي المتغير الكمي${\displaystyle \alpha }$يفشل المثال المضاد لأن الاستبدال غير متسق.

يمكن إضفاء الطابع الرسمي على الاستبدال المتسق من خلال تطبيق عملية استبدال${\displaystyle S=\left\{\ a_{i}\mapsto \tau _{i},\ \dots \ \right\}}$إلى مصطلح نوع${\displaystyle \tau }$، مكتوب${\displaystyle S\tau }$وكما يوحي المثال، فإن الاستبدال لا يرتبط ارتباطًا وثيقًا بالترتيب فحسب، والذي يعبر عن أن نوعًا ما خاص إلى حد ما، ولكن أيضًا بالتحديد الكمي الكامل الذي يسمح بتطبيق الاستبدال.

رسميًا، في HM، نوع${\displaystyle \sigma '}$هو أكثر عمومية من${\displaystyle \sigma }$رسميًا${\displaystyle \sigma '\sqsubseteq \sigma }$، إذا كان هناك متغير كمي في${\displaystyle \sigma '}$يتم استبدالها باستمرار بحيث يحصل المرء على${\displaystyle \sigma }$كما هو موضح في الشريط الجانبي. هذا الترتيب جزء من تعريف نوع نظام النوع.

في مثالنا السابق، بتطبيق الاستبدال${\displaystyle S=\left\{\alpha \mapsto {\texttt {string}}\right\}}$سيؤدي ذلك إلى${\displaystyle \forall \alpha .\alpha \rightarrow \alpha \sqsubseteq {\texttt {string}}\rightarrow {\texttt {string}}}$.

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

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

العلاقة${\displaystyle \sqsubseteq }$هو ترتيب جزئي و ${\displaystyle \forall \alpha .\alpha }$هو أصغر عنصر فيه.

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

البرهان باستخدام القواعد هو سلسلة من الأحكام بحيث تُذكر جميع المقدمات قبل النتيجة. تُظهر الأمثلة أدناه شكلاً محتملاً للبراهين. من اليسار إلى اليمين، يُظهر كل سطر النتيجة، و${\displaystyle [{\mathtt {Name}}]}$من القاعدة المطبقة والمقدمات، إما بالإشارة إلى سطر سابق (رقم) إذا كانت المقدمة حكماً أو بجعل المسند صريحاً.

لا يظهر ذلك على الفور، لكن مجموعة القواعد تُشفّر لائحةً تحدد الظروف التي قد يتم بموجبها تعميم نوع ما أو عدم تعميمه، وذلك من خلال استخدام متفاوت قليلاً للأنواع الأحادية والمتعددة في القواعد.${\displaystyle [{\mathtt {Abs}}]}$و${\displaystyle [{\mathtt {Let}}]}$تذكر ذلك${\displaystyle \sigma }$و${\displaystyle \tau }$تشير إلى الأنماط المتعددة والأنماط الأحادية على التوالي.

في القاعدة${\displaystyle [{\mathtt {Abs}}]}$، قيمة المتغير الخاص بمعامل الدالة${\displaystyle \lambda x.e}$يُضاف إلى السياق بنوع أحادي الشكل من خلال الفرضية${\displaystyle \Gamma ,\ x:\tau \vdash _{D}e:\tau '}$بينما في القاعدة ${\displaystyle [{\mathtt {Let}}]}$، يدخل المتغير إلى البيئة في شكل متعدد الأشكال${\displaystyle \Gamma ,\ x:\sigma \vdash _{D}e_{1}:\tau }$على الرغم من أن وجود${\displaystyle x}$يمنع هذا السياق استخدام قاعدة التعميم لأي متغير حر في عملية التخصيص، ويفرض هذا التنظيم نوع المعلمة.${\displaystyle x}$في${\displaystyle \lambda }$-التعبير يبقى أحادي الشكل، بينما في تعبير let، يمكن إدخال المتغير متعدد الأشكال، مما يجعل التخصيصات ممكنة.

ونتيجةً لهذا التنظيم،${\displaystyle \lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})}$لا يمكن تحديد نوعها، لأن المعامل${\displaystyle f}$وهو في وضع أحادي الشكل، بينما${\displaystyle {\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})}$له نوع${\displaystyle (bool,int)}$، لأن${\displaystyle f}$تم إدخالها في تعبير let، وبالتالي يتم التعامل معها على أنها متعددة الأشكال.

تستحق قاعدة التعميم أيضًا نظرة فاحصة. هنا، التكميم الشامل الضمني في الفرضية${\displaystyle \Gamma \vdash _{D}e:\sigma }$يتم نقلها ببساطة إلى الجانب الأيمن من${\displaystyle \vdash _{D}}$في الختام، مقيدًا بمُكمِّم كلي صريح. وهذا ممكن، لأن${\displaystyle \alpha }$لا يحدث ذلك بحرية في هذا السياق. ومرة ​​أخرى، مع أن هذا يجعل قاعدة التعميم معقولة، إلا أنها ليست نتيجةً حتمية. بل على العكس، تُعد قاعدة التعميم جزءًا من تعريف نظام أنواع HM، والتكميم الضمني الشامل نتيجةً حتمية.

عند عزل النقاط في البرهان، حيث لا يكون اتخاذ أي قرار ممكنًا على الإطلاق، فإن المجموعة الأولى من القواعد التي تتمحور حول بناء الجملة لا تترك أي خيار، حيث أن لكل قاعدة نحوية قاعدة تصنيف فريدة، تحدد جزءًا من البرهان، بينما بين النتيجة ومقدمات هذه الأجزاء الثابتة سلاسل من${\displaystyle [{\mathtt {Inst}}]}$و${\displaystyle [{\mathtt {Gen}}]}$ قد يحدث ذلك. ويمكن أن توجد سلسلة مماثلة بين نتيجة البرهان وقاعدة التعبير العلوي. يجب أن تتخذ جميع البراهين الشكل الموضح.

لأن الخيار الوحيد في البرهان فيما يتعلق باختيار القاعدة هو ${\displaystyle [{\mathtt {Inst}}]}$و${\displaystyle [{\mathtt {Gen}}]}$تُثير السلاسل، في شكل البرهان، تساؤلاً حول إمكانية جعله أكثر دقة، حيث قد لا تكون هذه السلاسل ضرورية. وهذا في الواقع ممكن، ويؤدي إلى صيغة بديلة لنظام القواعد تخلو من هذه القواعد.

يستخدم أحد المعالجات المعاصرة لـ HM نظام قواعد موجه نحو بناء الجملة فقط، والذي وضعه كليمنت ^{[ 6 ]،} كخطوة وسيطة. في هذا النظام، يقع التخصيص مباشرة بعد الأصل.${\displaystyle [{\mathtt {Var}}]}$وتم دمج القاعدة فيها، بينما أصبح التعميم جزءًا من${\displaystyle [{\mathtt {Let}}]}$القاعدة. هناك، يتم تحديد التعميم أيضًا لإنتاج النوع الأكثر عمومية دائمًا عن طريق إدخال الدالة${\displaystyle {\bar {\Gamma }}(\tau )}$، الذي يحدد كمياً جميع متغيرات النمط الأحادي غير المرتبطة في${\displaystyle \Gamma }$.

رسميًا، للتحقق من صحة نظام القواعد الجديد هذا${\displaystyle \vdash _{S}}$يعادل الأصل${\displaystyle \vdash _{D}}$يجب على المرء أن يثبت ذلك${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma }$، والتي تنقسم إلى برهانين فرعيين:

• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma }$( تناسق )
• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma }$( الشمولية )

بينما يمكن ملاحظة الاتساق من خلال تحليل القواعد${\displaystyle [{\mathtt {Let}}]}$و${\displaystyle [{\mathtt {Var}}]}$ ل${\displaystyle \vdash _{S}}$إلى البراهين في${\displaystyle \vdash _{D}}$من المرجح أن يكون واضحًا أن${\displaystyle \vdash _{S}}$غير مكتمل، إذ لا يمكن للمرء أن يُظهر${\displaystyle \lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha }$في${\displaystyle \vdash _{S}}$على سبيل المثال، ولكن فقط ${\displaystyle \lambda \ x.x:\alpha \rightarrow \alpha }$ومع ذلك ، يمكن إثبات نسخة أضعف قليلاً من الاكتمال ^{[ 7 ]} ، وهي:

• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma }$

وبالتالي، يمكن للمرء أن يستنتج النوع الرئيسي للتعبير في${\displaystyle \vdash _{S}}$مما يسمح لنا بتعميم البرهان في النهاية.

مقارنة${\displaystyle \vdash _{D}}$و${\displaystyle \vdash _{S}}$الآن، لا تظهر في أحكام جميع القواعد إلا الأنماط الأحادية. بالإضافة إلى ذلك، أصبح شكل أي برهان ممكن باستخدام نظام الاستدلال مطابقًا لشكل التعبير (كلاهما يُنظر إليهما على أنهما شجرتان ). وبالتالي، يُحدد التعبير شكل البرهان بشكل كامل.${\displaystyle \vdash _{D}}$من المرجح أن يتم تحديد الشكل وفقًا لجميع القواعد باستثناء${\displaystyle [{\mathtt {Inst}}]}$و${\displaystyle [{\mathtt {Gen}}]}$، والتي تسمح ببناء فروع (سلاسل) طويلة بشكل تعسفي بين العقد الأخرى.

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

هنا، يبرز دور ترتيب الاستبدال (التخصيص). فرغم أنه لا يمكن تحديد الأنواع محليًا للوهلة الأولى، إلا أن الأمل معقود على إمكانية تحسينها باستخدام هذا الترتيب أثناء اجتياز شجرة البرهان، مع افتراض إضافي، نظرًا لأن الخوارزمية الناتجة ستصبح طريقة استدلال، أن النوع في أي فرضية سيُحدد على أنه الأفضل. وفي الواقع، يمكن ذلك، بالنظر إلى قواعد${\displaystyle \vdash _{S}}$يقترح:

• [ ملخص ] : الخيار الحاسم هو τ . في هذه المرحلة، لا يُعرف شيء عن τ ، لذا لا يمكن إلا افتراض النوع الأكثر عمومية، وهو${\displaystyle \forall \alpha .\alpha }$الخطة هي تخصيص النوع إذا دعت الحاجة. لا يُسمح باستخدام نوع متعدد في هذا الموضع، لذا يكفي استخدام قيمة α مؤقتًا. لتجنب عمليات الاستحواذ غير المرغوب فيها، يُعد استخدام متغير نوع غير موجود في البرهان خيارًا آمنًا. إضافةً إلى ذلك، يجب الأخذ في الاعتبار أن هذا النوع الأحادي ليس نهائيًا بعد، بل قد يخضع لمزيد من التحسين.
• [ المتغير ] : يكمن الخيار في كيفية تحسين σ . ولأن أي اختيار لنوع τ هنا يعتمد على استخدام المتغير، وهو أمر غير معروف محليًا، فإن الخيار الأكثر أمانًا هو الأكثر عمومية. باستخدام الطريقة نفسها المذكورة أعلاه، يمكن إنشاء جميع المتغيرات الكمية في σ بمتغيرات أحادية النوع جديدة ، مما يتيح إمكانية تحسينها لاحقًا.
• [ Let ] : القاعدة لا تترك أي خيار. انتهى.
• [ التطبيق ] : قد تفرض قاعدة التطبيق فقط تحسينًا على المتغيرات "المفتوحة" حتى الآن، كما هو مطلوب من كلا المقدمتين.
  1. تُجبر الفرضية الأولى نتيجة الاستدلال على أن تكون على الشكل التالي:${\displaystyle \tau \rightarrow \tau '}$.
     • إذا كان الأمر كذلك، فلا بأس. يمكن للمرء لاحقاً اختيار قيمة τ ' للنتيجة.
     • وإلا، فقد يكون متغيرًا مفتوحًا. عندئذٍ يمكن تحسينه إلى الشكل المطلوب باستخدام متغيرين جديدين كما في السابق.
     • وإلا، فإن فحص النوع يفشل لأن الفرضية الأولى استنتجت نوعًا ليس نوعًا دالة ولا يمكن تحويله إليه .
  2. يشترط الشرط الثاني أن يكون النوع المُستنتج مساويًا لـ τ في الشرط الأول. الآن، لدينا نوعان قد يكونان مختلفين، وربما يحتويان على متغيرات مفتوحة النوع، للمقارنة والمساواة بينهما إن أمكن. إذا كان ذلك ممكنًا، يتم التوصل إلى تحسين، وإذا لم يكن كذلك، يتم اكتشاف خطأ في النوع مرة أخرى. من المعروف أن هناك طريقة فعالة لـ "مساواة حدين" عن طريق الاستبدال، وهي توحيد روبنسون بالاشتراك مع ما يُسمى بخوارزمية الاتحاد والبحث .

باختصار، تُمكّن خوارزمية الاتحاد والبحث، عند إعطاء مجموعة جميع الأنواع في برهان، من تجميعها في فئات تكافؤ باستخدام إجراء الاتحاد ، ثم اختيار ممثل لكل فئة باستخدام إجراء البحث . وبالتأكيد، فإن كلمة " إجراء" هنا تعني " أثر جانبي" ، مما يعني الخروج عن نطاق المنطق لإعداد خوارزمية فعّالة. ممثل لـ${\displaystyle {\mathtt {union}}(a,b)}$يُحدد ذلك بحيث إذا كان كل من a و b متغيرين من نوع معين، فإن المتغير المُمثل يكون أحدهما بشكل عشوائي، ولكن عند دمج متغير ومصطلح، يصبح المصطلح هو المتغير المُمثل. بافتراض وجود تطبيق لخوارزمية الاتحاد والبحث، يمكن صياغة دمج نوعين أحاديين على النحو التالي:

unify(ta, tb): ta = find(ta) tb = find(tb) إذا كان كل من ta و tb حدين من الشكل D p1..pn مع D و n متطابقين، فقم بتوحيد (ta[i]، tb[i]) لكل معامل i متناظر ، وإلا إذا كان أحد ta أو tb على الأقل متغيرًا من نوع معين ، الاتحاد (ta، tb) وإلا سيظهر خطأ "الأنواع غير متطابقة".

بعد أن تعرفنا على مخطط خوارزمية الاستدلال، سنقدم عرضًا أكثر تفصيلًا في القسم التالي. وقد وُصفت هذه الخوارزمية في كتاب ميلنر ^{[ 2 ]} ، الصفحات 370 وما بعدها، باسم الخوارزمية J.

يُعدّ عرض الخوارزمية J إساءة استخدام لترميز القواعد المنطقية، إذ يتضمن آثارًا جانبية ولكنه يسمح بمقارنة مباشرة مع${\displaystyle \vdash _{S}}$مع التعبير عن تنفيذ فعال في الوقت نفسه. تحدد القواعد الآن إجراءً بمعلمات${\displaystyle \Gamma ,e}$الاستسلام${\displaystyle \tau }$في الخاتمة حيث يتم تنفيذ المقدمات من اليسار إلى اليمين.

الإجراء${\displaystyle inst(\sigma )}$متخصص في النمط المتعدد${\displaystyle \sigma }$عن طريق نسخ المصطلح واستبدال متغيرات النوع المرتبط بشكل متسق بمتغيرات أحادية النوع جديدة.${\displaystyle newvar}$ينتج متغيرًا أحادي النمط جديدًا. على الأرجح،${\displaystyle {\bar {\Gamma }}(\tau )}$يجب نسخ النوع الذي يُدخل متغيرات جديدة للقياس الكمي لتجنب عمليات الاستحواذ غير المرغوب فيها. بشكل عام، تعمل الخوارزمية الآن من خلال اتخاذ الخيار الأكثر عمومية دائمًا، تاركةً التخصيص للتوحيد، الذي ينتج في حد ذاته النتيجة الأكثر عمومية. كما ذُكر أعلاه ، فإن النتيجة النهائية${\displaystyle \tau }$يجب تعميم ذلك على${\displaystyle {\bar {\Gamma }}(\tau )}$في النهاية، للحصول على النوع الأكثر عمومية لتعبير معين.

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

تنخفض الكفاءة قليلاً لأن ربط متغيرات النوع في السياق يجب الحفاظ عليه للسماح بحساب${\displaystyle {\bar {\Gamma }}(\tau )}$وتفعيل فحص "يحدث" لمنع إنشاء أنواع متكررة أثناء${\displaystyle {\mathit {unify}}(\alpha ,\tau )}$ومن الأمثلة على ذلك${\displaystyle \lambda \ x.(x\ x)}$والتي لا يمكن اشتقاق أي نوع لها باستخدام HM. عمليًا، الأنواع عبارة عن حدود صغيرة فقط ولا تُشكل هياكل متوسعة. لذا، في تحليل التعقيد، يمكن التعامل مع مقارنتها كثابت، مع الحفاظ على تكاليف O(1).

ومن ثم، يؤدي إثبات الخوارزمية J إلى الخوارزمية W، التي لا تفعل سوى الآثار الجانبية التي تفرضها العملية.${\displaystyle {\textit {union}}}$صريح من خلال التعبير عن تركيبه التسلسلي عن طريق الاستبدالات ${\displaystyle S_{i}}$لا يزال عرض الخوارزمية W في الشريط الجانبي يستخدم التأثيرات الجانبية في العمليات المكتوبة بخط مائل، ولكنها تقتصر الآن على توليد رموز جديدة. شكل الحكم هو${\displaystyle \Gamma \vdash e:\tau ,S}$، مما يشير إلى دالة ذات سياق وتعبير كمعامل ينتج عنه نمط أحادي مع استبدال.${\displaystyle {\textsf {mgu}}}$هو نسخة خالية من الآثار الجانبية من${\displaystyle {\textit {union}}}$إنتاج بديل هو الموحد الأكثر عمومية .

بينما تُعتبر الخوارزمية W عادةً خوارزمية HM وغالبًا ما يتم تقديمها مباشرةً بعد نظام القواعد في الأدبيات، فإن الغرض منها موصوف من قبل ميلنر ^{[ 2 ]} في الصفحة 369 على النحو التالي:

في وضعها الحالي، لا تُعدّ الخوارزمية W فعّالة بالقدر الكافي؛ إذ تُطبّق عمليات الاستبدال بكثرة. وقد صُمّمت هذه الخوارزمية للمساعدة في إثبات صحتها. ونقدّم الآن خوارزمية أبسط J تُحاكي الخوارزمية W بدقة.

رغم أنه اعتبر W أكثر تعقيدًا وأقل كفاءة، إلا أنه قدمه في منشوره قبل J. وله مزاياه عندما تكون الآثار الجانبية غير متوفرة أو غير مرغوب فيها. كما أن W ضروري لإثبات الاكتمال، وهو ما أخذه في الاعتبار عند إثبات سلامة النتائج.

قبل صياغة التزامات الإثبات، يجب التأكيد على وجود اختلاف بين أنظمة القواعد D و S والخوارزميات المعروضة.

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

وجود سياق${\displaystyle 1:int,\ f:\alpha }$، التعبير${\displaystyle f\ 1}$ لا يمكن كتابتها في أي من${\displaystyle \vdash _{D}}$أو${\displaystyle \vdash _{S}}$لكن الخوارزميات تتوصل إلى النوع${\displaystyle \beta }$، حيث يقوم W أيضًا بتقديم الاستبدال${\displaystyle \left\{\alpha \mapsto int\rightarrow \beta \right\}}$وهذا يعني أن الخوارزمية تفشل في اكتشاف جميع أخطاء النوع. ويمكن معالجة هذا القصور بسهولة من خلال التمييز بدقة أكبر بين متغيرات الإثبات ومتغيرات النوع الأحادي.

كان المؤلفون على دراية تامة بالمشكلة، لكنهم قرروا عدم حلها. قد يُفترض وجود سبب عملي وراء ذلك. فبينما كان من شأن تطبيق استنتاج النوع بشكل أكثر دقة أن يمكّن الخوارزمية من التعامل مع الأنماط الأحادية المجردة، إلا أنها لم تكن ضرورية للتطبيق المقصود حيث لا تحتوي أي من العناصر في سياق موجود مسبقًا على متغيرات حرة. في ضوء ذلك، تم التخلي عن التعقيد غير الضروري لصالح خوارزمية أبسط. أما الجانب السلبي المتبقي فهو أن برهان الخوارزمية فيما يتعلق بنظام القواعد أقل عمومية، ولا يمكن إجراؤه إلا في سياقات تحتوي على${\displaystyle free(\Gamma )=\emptyset }$كشرط جانبي.

${\displaystyle {\begin{array}{lll}{\text{(Correctness)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\{\text{(Completeness)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{forall}}\ \tau \ {\text{where}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}}$

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

لإثبات الالتزامات بشكل صحيح، يجب أولاً تعزيزها للسماح بتفعيل مبرهنة الاستبدال.${\displaystyle S}$خلال${\displaystyle \vdash _{S}}$و${\displaystyle \vdash _{W}}$ومن ثم، يتم تقديم البراهين عن طريق الاستقراء على التعبير.

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

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

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

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

quickSort :: Ord a => [ a ] ​​-> [ a ]

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

بما أن "الفئات" لا تسمح إلا بنوع واحد كمعامل لها، فإن نظام الأنواع الناتج لا يزال بإمكانه توفير الاستدلال. بالإضافة إلى ذلك، يمكن تزويد فئات الأنواع بنوع من ترتيب التحميل الزائد، مما يسمح بترتيب الفئات على شكل شبكة .

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

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

تُقدّم لغة هاسكل مستوىً أعلى يُسمى النوع (kind ). في هاسكل القياسية، تُستنتج الأنواع وتُستخدم لوصف عدد عناصر مُنشئات الأنواع. على سبيل المثال، يُنظر إلى مُنشئ نوع القائمة على أنه يُحوّل نوعًا (نوع عناصره) إلى نوع آخر (نوع القائمة التي تحتوي على تلك العناصر)؛ ويُعبّر عن ذلك كتابيًا كما يلي:${\displaystyle *\to *}$تتوفر امتدادات للغة تعمل على توسيع الأنواع لمحاكاة ميزات نظام الأنواع التابع . ^{[ 8 ]}

لقد تسببت محاولات الجمع بين تحديد الأنواع الفرعية واستنتاج الأنواع في إحباط كبير. من السهل تجميع قيود تحديد الأنواع الفرعية ونشرها (على عكس قيود تساوي الأنواع)، مما يجعل القيود الناتجة جزءًا من مخططات تحديد الأنواع المستنتجة، على سبيل المثال.${\displaystyle \forall \alpha .\ (\alpha \leq T)\Rightarrow \alpha \rightarrow \alpha }$، أين${\displaystyle \alpha \leq T}$يمثل قيدًا على متغير النوع${\displaystyle \alpha }$مع ذلك، ولأن متغيرات النوع لم تعد تُوحّد بشكل فوري في هذا النهج، فإنه يميل إلى توليد مخططات تصنيف كبيرة ومعقدة تحتوي على العديد من متغيرات النوع والقيود غير الضرورية، مما يجعل قراءتها وفهمها صعبًا. لذلك، بُذلت جهود كبيرة لتبسيط مخططات التصنيف هذه وقيودها، باستخدام تقنيات مشابهة لتلك المستخدمة في تبسيط الأوتوماتون المحدود غير الحتمي (NFA) (المفيد في وجود أنواع تكرارية مستنتجة). ^{[ 9 ]} ومؤخرًا، قام دولان ومايكروفت ^{[ 10 ]} بصياغة العلاقة بين تبسيط مخططات التصنيف وتبسيط الأوتوماتون المحدود غير الحتمي، وأظهرا أن اتباع نهج جبري في صياغة التصنيف الفرعي يسمح بتوليد مخططات تصنيف رئيسية مضغوطة للغة شبيهة بلغة ML (تُسمى MLsub). والجدير بالذكر أن مخطط التصنيف المقترح استخدم شكلًا مقيدًا من أنواع الاتحاد والتقاطع بدلًا من القيود الصريحة. ادعى بارو لاحقًا ^{[ 11 ]} أن هذه الصياغة الجبرية كانت مكافئة لخوارزمية بسيطة نسبيًا تشبه الخوارزمية W، وأن استخدام أنواع الاتحاد والتقاطع لم يكن ضروريًا.

من ناحية أخرى، أثبت استنتاج الأنواع صعوبة أكبر في سياق لغات البرمجة كائنية التوجه، لأن أساليب الكائنات تميل إلى اشتراط تعدد الأشكال من الدرجة الأولى على غرار نظام F (حيث يكون استنتاج الأنواع غير قابل للتقرير) وبسبب ميزات مثل تعدد الأشكال المحدود بنظام F. ونتيجة لذلك، فإن أنظمة الأنواع التي تدعم البرمجة كائنية التوجه، مثل نظام كارديلي ، تستخدم أنواعًا فرعية.${\displaystyle F_{<:}}$[ ^{12 ]} لا تدعم استنتاج النوع على نمط HM ^.

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