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

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

 3       : Number  
 add 3 4 : Number  
 add     : Number -> Number -> Number  

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

id ≡ λx . x

والتي تُرجع ببساطة القيمة التي تُطبّق عليها. وهناك أمثلة أقل بساطة تشمل الأنواع البارامترية مثل القائمة.

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

 cons : forall a . a -> List a -> List a  
 nil  : forall a . List a  
 id   : forall a . a -> a  

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

 id'  : String -> String  
 nil' : List Number  

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

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

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

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

السماح بذلك يؤدي إلى حساب لامبدا متعدد الأشكال؛ غير أن استدلال النوع في هذا النظام للأسف غير قابل للقرار.^[6]

بدلًا من ذلك، يميز النظام بين المتغيرات المرتبطة مباشرة بتعبير "let-bound variables"، والمتغيرات العامة المرتبطة بـλ، ويسمح فقط للنوع المتعدد الشكل بأن يُسند إلى الأولى. وهذا يؤدي إلى ما يسمى بـالتعدد الشكلي باستخدام let "let-polymorphism"، حيث تأخذ الحالة السابقة الشكل التالي:

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

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

التعبيرات

${\displaystyle {\begin{array}{lrll}\\e&=&x&{\textrm {variable}}\\&\vert &e_{1}\ e_{2}&{\textrm {application}}\\&\vert &\lambda \ x\ .\ e&{\textrm {abstraction}}\\&\vert &{\mathtt {let}}\ x=e_{1}\ {\mathtt {in}}\ e_{2}&\\\\\end{array}}}$

الأنواع

${\displaystyle {\begin{array}{llrll}\\{\textrm {mono}}&\tau &=&\alpha &\ {\textrm {variable}}\\&&\vert &C\ \tau \dots \tau &\ {\textrm {application}}\\{\textrm {poly}}&\sigma &=&\tau \\&&\vert &\forall \ \alpha \ .\ \sigma &\ {\textrm {quantifier}}\\\\\end{array}}}$

السياق والتحقيق النحوي للأنواع

${\displaystyle {\begin{array}{llrl}\\{\text{Context}}&\Gamma &=&\epsilon \ {\mathtt {(empty)}}\\&&\vert &\Gamma ,\ x:\sigma \\{\text{Typing}}&&=&\Gamma \vdash e:\sigma \\\\\end{array}}}$

متغيرات الأنواع الحرة

${\displaystyle {\begin{array}{ll}\\{\text{free}}(\ \alpha \ )&=\ \left\{\alpha \right\}\\{\text{free}}(\ C\ \tau _{1}\dots \tau _{n}\ )&=\ \bigcup \limits _{i=1}^{n}{{\text{free}}(\ \tau _{i}\ )}\\{\text{free}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{free}}(\ \sigma \ )\\\\{\text{free}}(\ \forall \ \alpha \ .\ \sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ \left\{\alpha \right\}\\{\text{free}}(\ \Gamma \vdash e:\sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ {\text{free}}(\ \Gamma \ )\\\\\end{array}}}$

التعبيرات التي تُسند لها الأنواع هي نفسها تعبيرات تكامل لامدا مع توسيع يتضمن تعبير let كما هو موضح في الجدول المجاور. يمكن استخدام الأقواس لإزالة الغموض من تعبير ما. التطبيق يرتبط يسارياً ويرتبط بشكل أقوى من التجريد أو بنية let-in.

تنقسم الأنواع من الناحية الصرفية إلى مجموعتين: الأنواع الأحادية والأنواع المتعددة.^{[note 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 }$. كما يُشير المثال، فإن الاستبدال لا يرتبط فقط ارتباطًا وثيقًا بعلاقة ترتيب تُعبّر عن كون نوع ما أكثر أو أقل تخصيصًا، بل يرتبط أيضًا بعملية التكميم الكلي التي تسمح بتطبيق الاستبدال.

قاعدة التخصيص

${\displaystyle \displaystyle {\frac {\tau '=\left\{\alpha _{i}\mapsto \tau _{i}\right\}\tau \quad \beta _{i}\not \in {\textrm {free}}(\forall \alpha _{1}...\forall \alpha _{n}.\tau )}{\forall \alpha _{1}...\forall \alpha _{n}.\tau \sqsubseteq \forall \beta _{1}...\forall \beta _{m}.\tau '}}}$

بشكل رسمي، في نظام Hindley–Milner، يكون النوع ${\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 }$ هو أصغر عنصر فيها.

نظام القواعد التصريحية

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma }{\Gamma \vdash _{D}x:\sigma }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{D}e:\tau '}{\Gamma \vdash _{D}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau }}&[{\mathtt {Let}}]\\\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma '\quad \sigma '\sqsubseteq \sigma }{\Gamma \vdash _{D}e:\sigma }}&[{\mathtt {Inst}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma \quad \alpha \notin {\text{free}}(\Gamma )}{\Gamma \vdash _{D}e:\forall \ \alpha \ .\ \sigma }}&[{\mathtt {Gen}}]\\\\\end{array}}}$

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

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

قواعد الكتابة النوعية

قواعد النحو

${\displaystyle {\begin{array}{lrl}{\text{Predicate}}&=&\sigma \sqsubseteq \sigma '\\&\vert \ &\alpha \not \in free(\Gamma )\\&\vert \ &x:\alpha \in \Gamma \\\\{\text{Judgment}}&=&{\text{Typing}}\\{\text{Premise}}&=&{\text{Judgment}}\ \vert \ {\text{Predicate}}\\{\text{Conclusion}}&=&{\text{Judgment}}\\\\{\text{Rule}}&=&\displaystyle {\frac {{\textrm {Premise}}\ \dots }{\textrm {Conclusion}}}\quad [{\mathtt {Name}}]\end{array}}}$

يعرض الصندوق الجانبي قواعد الاستنتاج الخاصة بنظام الأنواع لهندلي-ميلنر. يمكن تقسيم القواعد تقريبًا إلى مجموعتين:

المجموعة الأولى تشمل القواعد الأربع ${\displaystyle [{\mathtt {Var}}]}$ (الوصول إلى متغير أو دالة)، و${\displaystyle [{\mathtt {App}}]}$ (تطبيق، أي استدعاء دالة بمعطى)، و${\displaystyle [{\mathtt {Abs}}]}$ (تجريد، أي تعريف دالة)، و${\displaystyle [{\mathtt {Let}}]}$ (تعريف متغير). تركز هذه القواعد على البنية النحوية، حيث تقدم قاعدة واحدة لكل شكل من أشكال التعبيرات. وهي سهلة الفهم لأنها تُفكك كل تعبير، وتثبت صحة التعبيرات الفرعية، وتجمع بين الأنواع الناتجة في المقدمات للحصول على النوع في النتيجة.

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

فيما يلي مثالان يوضحان تطبيق نظام القواعد. وبما أن التعبير والنوع معطيان، فإن الحالة هنا هي تحقق من النوع باستخدام القواعد.

مثال: إثبات أن ${\displaystyle \Gamma \vdash _{D}id(n):int}$ حيث ${\displaystyle \Gamma =id:\forall \alpha .\alpha \rightarrow \alpha ,\ n:int}$:

${\displaystyle {\begin{array}{llll}1:&\Gamma \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \Gamma )\\2:&\Gamma \vdash _{D}id:int\rightarrow int&[{\mathtt {Inst}}]&(1),\ (\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\3:&\Gamma \vdash _{D}n:int&[{\mathtt {Var}}]&(n:int\in \Gamma )\\4:&\Gamma \vdash _{D}id(n):int&[{\mathtt {App}}]&(2),\ (3)\\\end{array}}}$

مثال: لإثبات التعميم، ${\displaystyle \vdash _{D}\ {\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha }$:

${\displaystyle {\begin{array}{llll}1:&x:\alpha \vdash _{D}x:\alpha &[{\mathtt {Var}}]&(x:\alpha \in \left\{x:\alpha \right\})\\2:&\vdash _{D}\lambda x.x:\alpha \rightarrow \alpha &[{\mathtt {Abs}}]&(1)\\3:&id:\alpha \rightarrow \alpha \vdash _{D}id:\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\alpha \rightarrow \alpha \in \left\{id:\alpha \rightarrow \alpha \right\})\\4:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\alpha \rightarrow \alpha &[{\mathtt {Let}}]&(2),\ (3)\\5:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Gen}}]&(4),\ (\alpha \not \in free(\epsilon ))\\\end{array}}}$

رغم أن ذلك لا يظهر بشكل مباشر، فإن مجموعة القواعد تُشفّر تنظيمًا يحدد في أي ظروف يمكن تعميم نوع ما أو عدم تعميمه، وذلك من خلال اختلاف طفيف في استخدام الأنواع الأحادية (monotypes) والأنواع متعددة الأشكال (polytypes) في القاعدتين ${\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 }$ لا تظهر بشكل حر في السياق. ومرة أخرى، رغم أن هذا يجعل قاعدة التعميم تبدو معقولة، إلا أنها ليست نتيجة منطقية مستخلصة من القواعد الأخرى، بل على العكس، فإن قاعدة التعميم تُعد جزءًا من تعريف نظام الأنواع لهندلي-ميلنر، بينما يكون التكميم الكلي الضمني نتيجة ناتجة عنها.

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

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

نظام القواعد النحوية

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \sigma \sqsubseteq \tau }{\Gamma \vdash _{S}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{S}e_{1}:\tau }{\Gamma \vdash _{S}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{S}e:\tau '}{\Gamma \vdash _{S}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{S}e_{1}:\tau '}{\Gamma \vdash _{S}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}}$

التعميم

${\displaystyle {\bar {\Gamma }}(\tau )=\forall \ {\hat {\alpha }}\ .\ \tau \quad \quad {\hat {\alpha }}={\textrm {free}}(\tau )-{\textrm {free}}(\Gamma )}$

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

لإثبات أن هذا النظام الجديد ${\displaystyle \vdash _{S}}$ مكافئ للنظام الأصلي ${\displaystyle \vdash _{D}}$، يجب إثبات التالي:

• ${\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 \lambda \ x.x:\alpha \rightarrow \alpha }$. إلا أن نسخة أضعف قليلًا من الاكتمال يمكن إثباتها^[8]، وهي:

• ${\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}}$:

• [Abs]: الخيار الحاسم هو ${\displaystyle \tau }$. في هذه النقطة، لا يُعرف شيء عن ${\displaystyle \tau }$، لذا يمكن فقط افتراض النوع الأكثر عمومية وهو ${\displaystyle \forall \alpha .\alpha }$. الخطة هي تخصيص النوع إذا أصبح ذلك ضروريًا. ولكن، لا يُسمح بنوع متعدد في هذا الموضع، لذا يجب استخدام متغير نوع ${\displaystyle \alpha }$ لم يُستخدم بعد في البرهان كخيار آمن. يجب أيضًا تذكّر أن هذا النوع الأحادي لم يُثبت بعد، وقد يُعدّل لاحقًا.

• [Var]: الخيار هنا هو كيفية تحسين ${\displaystyle \sigma }$. نظرًا لأن أي اختيار لنوع ${\displaystyle \tau }$ هنا يعتمد على استخدام المتغير، وهو أمر غير معروف محليًا، فإن الخيار الأكثر أمانًا هو الأكثر عمومية. باستخدام نفس الطريقة كما في السابق، يمكن استبدال جميع المتغيرات المُكمّمة في ${\displaystyle \sigma }$ بمتغيرات نوعية جديدة (fresh)، مع إبقائها قابلة للتعديل لاحقًا.

• [Let]: هذه القاعدة لا تترك مجالًا للاختيار. انتهى الأمر.

• [App]: قاعدة التطبيق فقط قد تُجبر على تعديل المتغيرات "المفتوحة" حتى الآن، كما تتطلبه المسلّمتان.
  1. المسلمة الأولى تُجبر النتيجة على أن تكون من الشكل ${\displaystyle \tau \rightarrow \tau '}$.
     • إذا كانت كذلك، فلا بأس. يمكن لاحقًا اختيار ${\displaystyle \tau '}$ للنتيجة.
     • إذا لم تكن كذلك، فقد تكون متغيرًا مفتوحًا. يمكن إذًا تعديلها للشكل المطلوب باستخدام متغيرين جديدين كما في السابق.
     • أما إذا لم تكن كذلك ولا يمكن تعديلها إلى نوع دالي (تابعي)، يفشل التحقق من النوع.
  2. المسلمة الثانية تتطلب أن يكون النوع المُستنتج مساويًا لـ ${\displaystyle \tau }$ في المسلمة الأولى. يوجد الآن نوعان مختلفان محتملان، ربما بهما متغيرات نوع مفتوحة، ويجب مقارنتهما وجعلهما متساويين إن أمكن. إذا أمكن، يكون التعديل قد تم بنجاح، وإن لم يكن، يتم كشف خطأ في النوع. هناك طريقة فعالة معروفة لـ"جعل مصطلحين متساويين" عن طريق الاستبدال، وهي التوحيد كما قدمه جون ألان روبنسون بالاقتران مع خوارزمية هيكلة بيانات المجموعات المنفصلة.

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

unify(ta, tb):   ta = find(ta)   tb = find(tb)   إذا كان كلٌّ من ta وtb على شكل D p1..pn بنفس D وn فإننا     نقوم بـ unify(ta[i], tb[i]) لكل عنصر مطابق i   وإلا   إذا كان على الأقل أحد ta أو tb متغير نوع فإننا     نقوم بـ union(ta, tb)   وإلا     خطأ 'الأنواع غير متطابقة'

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

الخوارزمية J

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{J}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau _{0}\quad \Gamma \vdash _{J}e_{1}:\tau _{1}\quad \tau '={\mathit {newvar}}\quad {\mathit {unify}}(\tau _{0},\ \tau _{1}\rightarrow \tau ')}{\Gamma \vdash _{J}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{J}e:\tau '}{\Gamma \vdash _{J}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{J}e_{1}:\tau '}{\Gamma \vdash _{J}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}}$

عرض الخوارزمية 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 صعبة، إن لم تكن معضلة غير قابلة للقرار من حيث إنهاء التنفيذ. وهكذا فإن خوارزمية HM تحقق كفاءة توازي أفضل خوارزميات التحقق من النوع عند توافر جميع المعلومات. علمًا أن "التحقق من النوع" هنا يعني أن الخوارزمية لا تحتاج إلى العثور على إثبات، بل فقط التحقق من صحة إثبات معطى.

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

الخوارزمية W

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{W}x:\tau ,\emptyset }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\begin{array}{ll}\Gamma \vdash _{W}e_{0}:\tau _{0},S_{0}&S_{0}\Gamma \vdash _{W}e_{1}:\tau _{1},S_{1}\\\tau '={\mathit {newvar}}&S_{2}={\mathsf {mgu}}(S_{1}\tau _{0},\ \tau _{1}\rightarrow \tau ')\end{array}}{\Gamma \vdash _{W}e_{0}\ e_{1}:S_{2}\tau ',S_{2}S_{1}S_{0}}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{W}e:\tau ',S}{\Gamma \vdash _{W}\lambda \ x\ .\ e:S\tau \rightarrow \tau ',S}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{W}e_{0}:\tau ,S_{0}\quad S_{0}\Gamma ,\,x:{\overline {S_{0}\Gamma }}(\tau )\vdash _{W}e_{1}:\tau ',S_{1}}{\Gamma \vdash _{W}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau ',S_{1}S_{0}}}&[{\mathtt {Let}}]\end{array}}}$

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

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

كما هي، فإن 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{(الصحة)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\[4pt]{\text{(الإتمام)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{لكل}}\ \tau \ {\text{حيث}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}}$

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

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

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

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

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

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

يستخدم مثال الترتيب السريع المذكور في المقدمة التحميل الزائد في علاقات الترتيب، مع التعليق النمطي التالي في هاسكل:

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

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

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

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

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

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

تسببت محاولات الجمع بين التصنيف الفرعي واستدلال الأنواع في قدر كبير من الإحباط. من السهل إلى حد ما تجميع ونشر قيود التصنيف الفرعي (على عكس قيود تساوي الأنواع)، مما يجعل القيود الناتجة جزءًا من مخططات الأنواع المستنتجة، على سبيل المثال: ∀α. (α ≤ T) ⇒ α → α، حيث α ≤ T هو قيد على متغير النوع α. ومع ذلك، ونظرًا لأن متغيرات النوع لم تعد تُوحَّد بسرعة في هذا النهج، فإنه يميل إلى إنتاج مخططات أنواع كبيرة وصعبة التعامل تحتوي على العديد من متغيرات النوع والقيود غير المفيدة، مما يجعلها صعبة القراءة والفهم. لذلك، بُذل جهد كبير لتبسيط مثل هذه المخططات والقيود باستخدام تقنيات مشابهة لتبسيط الأتمتة المنتهية غير الحتمية (NFA)، وهو أمر مفيد في حال وجود أنواع استنتاجية متكررة.^[10]

مؤخرًا، قام دولان ومايكروفت^[11] بتأصيل العلاقة بين تبسيط مخططات الأنواع وتبسيط الأتمتة المنتهية غير الحتمية (NFA)، وبيّنا أن الطرح الجبري لتأصيل التصنيف الفرعي يسمح بإنتاج مخططات أنواع رئيسية مدمجة للغة شبيهة بـML (سُميت MLsub). ومن الجدير بالذكر أن المخطط المقترح استخدم شكلًا مقيدًا من أنواع الاتحاد والتقاطع بدلًا من القيود الصريحة.

لاحقًا، ادعى بارّو^[12] أن هذا الطرح الجبري يعادل خوارزمية بسيطة نسبيًا تُشبه خوارزمية W، وأن استخدام أنواع الاتحاد والتقاطع لم يكن ضروريًا.

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

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