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

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

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

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

يرجع الأصل إلى خوارزمية استدلال النوع لحساب لامبدا البسيط التي صاغها هاسكل كاري وروبرت فايس عام 1958.

في عام 1969، قام ج. روجر هندلي بتوسيع هذا العمل وأثبت أن خوارزميتهم تستنتج دائمًا النوع الأعمّ.

وفي عام 1978، قدم روبن ميلنر — بشكل مستقل عن عمل هندلي — خوارزمية مكافئة تُعرف بالخوارزمية W.

وفي عام 1982، أثبت لويس داماس أخيرًا أن خوارزمية ميلنر كاملة، ووسّعها لتدعم الأنظمة التي تحتوي على مراجع متعددة الأشكال .

### الأُحاديات الشكل مقابل التعدد الشكلي

في حساب لامبدا البسيط الترتيب، الأنواع  إما أن تكون ثوابت نوع ذرية أو أنواع دوال من الشكل 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 في لغة هاسكل.

### التعدد الشكلي مع let

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

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

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

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

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

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

## نظرة عامة
تمضي بقية هذه المقالة على النحو التالي:
* يُعرّف نظام الأنواع في هندلي–ميلنر (HM). ويتم ذلك من خلال وصف نظام استنتاج يحدد بدقة ما إذا كانت التعبيرات تملك نوعًا معينًا، وإن كانت كذلك، فما هو هذا النوع.
* ومن هناك، يتم التدرج نحو تنفيذ طريقة استدلال النوع. بعد تقديم صيغة مستندة إلى البنية النحوية للنظام الاستنتاجي المذكور أعلاه، يتم عرض تصور أولي لتنفيذ فعّال (الخوارزمية J)، بالاعتماد بشكل كبير على حدس القارئ الميتا-منطقي.
* وبما أن بقاء توافق الخوارزمية J مع نظام الاستنتاج الأصلي غير محسوم، يتم تقديم تنفيذ أقل كفاءة (الخوارزمية W)، ويُلمح إلى استخدامه في إثبات منطقي.
* وأخيرًا، تُناقش مواضيع إضافية ذات صلة بالخوارزمية.

يُستخدم نفس الوصف لنظام الاستنتاج في جميع المراحل، بما في ذلك عند عرض الخوارزميتين، لجعل الأشكال المختلفة التي يُقدّم بها منهج HM قابلة للمقارنة المباشرة.

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

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

### البنية الصرفية

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

تنقسم الأنواع من الناحية الصرفية إلى مجموعتين: الأنواع الأحادية والأنواع المتعددة.

#### الأنواع الأحادية
الأنواع الأحادية تشير دائماً إلى نوع معين. يُمثّل النوع الأحادي \tau صرفياً كحد.

من أمثلة الأنواع الأحادية أنواع البيانات الأولية مثل \mathtt{int} أو \mathtt{string}، والأنواع المُعلَّمة (البارامترية) مثل \mathtt{Map\ (Set\ string)\ int}. النوع الأخير مثال على *تطبيق* دوال نوعية مثل تلك الموجودة في المجموعة:
 \{ \mathtt{Map^2,\ Set^1,\ string^0,\ int^0},\ \rightarrow^2 \} ،
حيث يشير الرقم الأعلى إلى عدد الوسيطات النوعية. المجموعة الكاملة لدوال الأنواع C يمكن أن تكون اعتباطية في نظام HM،، على أن تحتوي على الأقل على \rightarrow^2، وهو نوع الدوال. وغالباً ما يُكتب بصيغة موضعية (infix) للراحة. على سبيل المثال، الدالة التي تُحوّل أعداداً صحيحة إلى سلاسل لها النوع \mathtt{int}\rightarrow \mathtt{string}. مرة أخرى، يمكن استخدام الأقواس لتوضيح تعبير نوعي. التطبيق يرتبط أقوى من السهم المُوضع، والذي يرتبط يمينياً.

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

يُعتبر نوعان أحاديان متساويين إذا كانت عباراتهما متطابقة تماماً.

#### الأنواع المتعددة

*الأنواع المتعددة* (أو *مخططات الأنواع*) هي أنواع تحتوي على متغيرات مُقيَّدة بواحد أو أكثر من كمّيات "لكل"، مثل \forall\alpha.\alpha\rightarrow\alpha.

دالة ذات النوع \forall\alpha.\alpha\rightarrow\alpha يمكنها تحويل أي قيمة من نفس النوع إلى نفسها، ودالة مطابقة تمثل قيمة لهذا النوع.

كمثال آخر، \forall\alpha.(\mathtt{Set}\ \alpha)\rightarrow \mathtt{int} هو نوع دالة تحوّل كل المجموعات المنتهية إلى أعداد صحيحة. الدالة التي تُعيد حجم مجموعة هي قيمة لهذا النوع.

يمكن للكمّيات أن تظهر فقط في المستوى الأعلى. على سبيل المثال، النوع \forall\alpha.\alpha\rightarrow\forall\alpha.\alpha مستبعد صرفياً. أيضاً الأنواع الأحادية مشمولة ضمن الأنواع المتعددة، وبالتالي الشكل العام لنوع متعدد هو \forall\alpha_1\dots\forall\alpha_n.\tau، حيث  n\geq0 و \tau نوع أحادي.

تُقاس مساواة الأنواع المتعددة بترتيب الكمّيات وتغيير أسماء المتغيرات المُقيدة (\alpha-تحويل). علاوة على ذلك، يمكن حذف المتغيرات المُقيدة غير الموجودة في النوع الأحادي.

#### السياق والإسناد

لربط الأجزاء الثلاثة: التعبيرات الصرفية والأنواع، نحتاج إلى عنصر ثالث هو السياق. من الناحية الصرفية، السياق هو قائمة من الأزواج x:\sigma، وتُسمى إسنادات أو افتراضات أو روابط، كل زوج يُصرّح أن المتغير x_i له النوع \sigma_i. هذه الأجزاء الثلاثة تُشكّل معاً "حكم الإسناد" بالشكل \Gamma\ \vdash\ e:\sigma، ويعني أنه تحت الافتراضات \Gamma، التعبير e له النوع \sigma.

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

في النوع \forall\alpha_1\dots\forall\alpha_n.\tau، الرمز \forall هو الكمي الذي يُقيد المتغيرات النوعية \alpha_i في النوع الأحادي \tau. تُسمى هذه المتغيرات "مقيدة"، وأي ظهور لها في \tau يُعد "مقيداً"، وكل المتغيرات النوعية غير المقيدة في \tau تُعد "حرة". إضافة إلى التقييد بالـ\forall في الأنواع المتعددة، يمكن تقييد المتغيرات أيضاً عند ظهورها في السياق، ولكن بتأثير معاكس في الجهة اليمنى من \vdash. مثل هذه المتغيرات تتصرف كأنها ثوابت نوعية هناك. وأخيراً، يمكن أن يظهر متغير نوعي بشكل حر في إسناد، وفي هذه الحالة يُعتبر ضمنياً مُقيداً بـ"لكل".

وجود كل من المتغيرات المقيدة والحرة في نفس النوع غير شائع في لغات البرمجة. في الغالب، تُعامل جميع المتغيرات النوعية كأنها مُقيدة ضمناً. مثلاً، لا توجد عبارات بمتغيرات حرة في برولوغ. وكذلك في هاسكل، حيث تُعتبر جميع المتغيرات النوعية مُقيدة ضمناً، أي أن النوع `a -> a` في هاسكل يعني \forall\alpha.\alpha\rightarrow\alpha. ومن الأمور غير الشائعة أيضاً تأثير التقييد في الجهة اليمنى \sigma في الإسنادات.

عادةً ما ينشأ اختلاط المتغيرات المقيدة والحرة من استخدام متغيرات حرة في تعبير. مثال على ذلك دالة الثابت **K** = \lambda x.\lambda y. x، التي لها النوع الأحادي \alpha\rightarrow\beta\rightarrow\alpha. يمكن فرض التعددية في الأنواع عبر التعبير:
\mathbf{let}\ k = \lambda x. (\mathbf{let}\ f = \lambda y.x\ \mathbf{in}\ f)\ \mathbf{in}\ k.

هنا، f لها النوع \forall \gamma.\gamma\rightarrow\alpha. المتغير النوعي الحر \alpha جاء من النوع المرتبط بالمتغير x في السياق المحيط. k له النوع \forall\alpha\forall\beta.\alpha\rightarrow\beta\rightarrow\alpha. يمكن تخيّل أن المتغير النوعي الحر \alpha في نوع f تم تقييده عبر \forall\alpha في نوع k. لكن مثل هذا المجال لا يمكن التعبير عنه في نظام HM. بل يُعبَّر عنه من خلال السياق.

### رتبة النوع
تُشير *تعددية الأشكال* إلى أن تعبيرًا واحدًا نفسه يمكن أن يكون له (وربما عدد لا نهائي) من الأنواع. ولكن في نظام الأنواع هذا، لا تكون هذه الأنواع غير مترابطة تمامًا، بل يتم تنظيمها بواسطة التعدد الشكلي المعلمي.

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

يمكن التعبير عن الاستبدال المتسق رسميًا من خلال تطبيق استبدال S = \left\{ a_i \mapsto \tau_i, \dots \right\} على تعبير من نوع \tau، ويُكتب S\tau. كما يُشير المثال، فإن الاستبدال لا يرتبط فقط ارتباطًا وثيقًا بعلاقة ترتيب تُعبّر عن كون نوع ما أكثر أو أقل تخصيصًا، بل يرتبط أيضًا بعملية التكميم الكلي التي تسمح بتطبيق الاستبدال.

بشكل رسمي، في نظام Hindley–Milner، يكون النوع \sigma' أكثر عمومية من النوع \sigma، ويُكتب ذلك على الشكل \sigma' \sqsubseteq \sigma، إذا تم استبدال بعض المتغيرات المُكمَّمة في \sigma' بطريقة متسقة بحيث نحصل على \sigma، كما هو موضح في الجدول الجانبي. تُشكّل هذه العلاقة جزءًا من تعريف النوع في نظام الأنواع.

في مثالنا السابق، فإن تطبيق الاستبدال S = \left\{\alpha \mapsto \texttt{string} \right\} سينتج عنه:

\forall \alpha . \alpha \rightarrow \alpha \sqsubseteq \texttt{string} \rightarrow \texttt{string}

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

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

العلاقة \sqsubseteq تُشكّل مجموعة مرتبة جزئيًا، والنوع \forall \alpha . \alpha هو أصغر عنصر فيها.

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

#### الاستبدال في السياقات النوعية

يمكن توسيع علاقة ترتيب الأنواع المحددة أعلاه لتشمل **السياقات النوعية (typings)**، لأن التكميم الكلي الضمني في السياقات يتيح الاستبدال المتسق:

:\Gamma \vdash e : \sigma \quad\Longrightarrow\quad S\Gamma \vdash e : S\sigma

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

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

سيناقش هذا المقال أربع مجموعات مختلفة من قواعد الأنواع:

:# \vdash_D النظام الإعلاني (Declarative system)
:# \vdash_S النظام الصياغي (Syntactic system)
:# \vdash_J الخوارزمية J
:# \vdash_W الخوارزمية W

### نظام الاستنتاج

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

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

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

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

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

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

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

**مثال**: إثبات أن \Gamma \vdash_D id(n):int حيث \Gamma = id:\forall \alpha . \alpha\rightarrow\alpha,\ n:int:

: \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}


**مثال**: لإثبات التعميم،
\vdash_D\ \textbf{let}\, id = \lambda x . x\ \textbf{in}\ id\, :\, \forall\alpha.\alpha\rightarrow\alpha:

: 
\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) في القاعدتين [\mathtt{Abs}] و[\mathtt{Let}]. تذكَّر أن الرمزين \sigma و\tau يدلان على الأنواع المتعددة الأشكال والأحادية على الترتيب.

في القاعدة [\mathtt{Abs}]، تُضاف متغيرات القيمة الخاصة بمعامل الدالة \lambda x.e إلى السياق بنوع أحادي عبر المسلّمة \Gamma,\ x:\tau \vdash_D e:\tau'، في حين أنه في القاعدة [\mathtt{Let}]، يُدخل المتغير في البيئة بنوع متعدد الأشكال \Gamma,\ x:\sigma \vdash_D e_1:\tau. رغم أن وجود x في السياق في كلا الحالتين يمنع استخدام قاعدة التعميم لأي متغير حر في التعريف، إلا أن هذا التنظيم يُجبر نوع المعامل x في تعبير \lambda على أن يبقى أحاديًا، بينما في تعبير ليت "let" يمكن إدخال المتغير كنوع متعدد الأشكال، مما يجعل التخصيصات ممكنة.

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

### قاعدة التعميم

تستحق قاعدة التعميم هي الأخرى نظرة أدق. في هذه القاعدة، يتم ببساطة نقل التكميم الكلي الضمني في المسلّمة \Gamma \vdash_D e : \sigma إلى الجانب الأيمن من \vdash_D في الاستنتاج، ليصبح مرتبطًا بكمّ شامل صريح. ويُسمح بذلك لأن \alpha لا تظهر بشكل حر في السياق. ومرة أخرى، رغم أن هذا يجعل قاعدة التعميم تبدو معقولة، إلا أنها ليست نتيجة منطقية مستخلصة من القواعد الأخرى، بل على العكس، فإن قاعدة التعميم تُعد جزءًا من تعريف نظام الأنواع لهندلي-ميلنر، بينما يكون التكميم الكلي الضمني نتيجة ناتجة عنها.

## خوارزمية الاستنتاج

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

### درجات الحرية في اختيار القواعد

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

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

### نظام قواعد موجه نحويًا

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

لإثبات أن هذا النظام الجديد \vdash_S مكافئ للنظام الأصلي \vdash_D، يجب إثبات التالي:

* \Gamma \vdash_D\ e:\sigma \Leftarrow \Gamma \vdash_S\ e:\sigma (اتساق)
* \Gamma \vdash_D\ e:\sigma \Rightarrow \Gamma \vdash_S\ e:\sigma (اكتمال)

بينما يمكن ملاحظة الاتساق من خلال تحليل قواعد [\mathtt{Let}] و[\mathtt{Var}] في \vdash_S إلى براهين في \vdash_D، فإنه من الواضح أن \vdash_S غير مكتمل، إذ لا يمكن على سبيل المثال إثبات \lambda\ x.x:\forall\alpha.\alpha\rightarrow\alpha فيه، بل فقط \lambda\ x.x:\alpha\rightarrow\alpha. إلا أن نسخة أضعف قليلًا من الاكتمال يمكن إثباتها، وهي:

* \Gamma \vdash_D\ e:\sigma \Rightarrow \Gamma \vdash_S\ e:\tau \wedge \bar{\Gamma}(\tau)\sqsubseteq\sigma

مما يعني أنه يمكن اشتقاق النوع الرئيسي للتعبير في \vdash_S مما يسمح لنا بتعميم البرهان في النهاية.

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

### درجات الحرية في تفعيل القواعد

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

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

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

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

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

* : قاعدة التطبيق فقط قد تُجبر على تعديل المتغيرات "المفتوحة" حتى الآن، كما تتطلبه المسلّمتان.
*# المسلمة الأولى تُجبر النتيجة على أن تكون من الشكل \tau \rightarrow \tau'.
*#* إذا كانت كذلك، فلا بأس. يمكن لاحقًا اختيار \tau' للنتيجة.
*#* إذا لم تكن كذلك، فقد تكون متغيرًا مفتوحًا. يمكن إذًا تعديلها للشكل المطلوب باستخدام متغيرين جديدين كما في السابق.
*#* أما إذا لم تكن كذلك ولا يمكن تعديلها إلى نوع دالي (تابعي)، يفشل التحقق من النوع.
*# المسلمة الثانية تتطلب أن يكون النوع المُستنتج مساويًا لـ \tau في المسلمة الأولى. يوجد الآن نوعان مختلفان محتملان، ربما بهما متغيرات نوع مفتوحة، ويجب مقارنتهما وجعلهما متساويين إن أمكن. إذا أمكن، يكون التعديل قد تم بنجاح، وإن لم يكن، يتم كشف خطأ في النوع. هناك طريقة فعالة معروفة لـ"جعل مصطلحين متساويين" عن طريق الاستبدال، وهي التوحيد كما قدمه جون ألان روبنسون بالاقتران مع خوارزمية هيكلة بيانات المجموعات المنفصلة.

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

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

### الخوارزمية J

عرض الخوارزمية J يعدّ استخدامًا غير دقيق لرموز القواعد المنطقية، نظرًا لاشتماله على تأثيرات جانبية، إلا أنه يسمح بالمقارنة المباشرة مع \vdash_S مع التعبير في الوقت ذاته عن تطبيق فعال. تحدد القواعد الآن إجراءً بالمعاملين \Gamma, e ويُنتج \tau في النتيجة، حيث تُنفذ المقدمات من اليسار إلى اليمين.

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

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

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

## إثبات صحة الخوارزمية

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

النقطة الأكثر إشكالية في الحجة السابقة هي تنقيح متغيرات النمط الأحادي المرتبطة بالسياق. فعلى سبيل المثال، تقوم الخوارزمية بتغيير السياق بشكل مباشر أثناء استنتاج التعبير \lambda f . (f\ 1)، لأن متغير النمط الأحادي الذي أُضيف إلى السياق للوسيط f يحتاج لاحقًا إلى تنقيح إلى int \rightarrow \beta عند التعامل مع التطبيق. المشكلة أن قواعد الاستنتاج لا تسمح بمثل هذا التنقيح. والقول بأن النوع المنقح كان من الممكن إضافته مسبقًا بدلاً من متغير النمط الأحادي هو مجرد تسهيل ظرفي.

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

:\Gamma \vdash_S e : \tau \quad\Longrightarrow\quad S \Gamma \vdash_S e : S \tau

وبالتالي فإن تنقيح المتغيرات الحرة يعني تنقيح الاستنتاج بأكمله.

### الخوارزمية W

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

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

:*كما هي، فإن W ليست خوارزمية فعالة حقًا؛ إذ تُطبق الاستبدالات كثيرًا جدًا. لقد صيغت لتسهيل إثبات الصحة. وسنقدم الآن خوارزمية أبسط (الخوارزمية J) تحاكي W بطريقة دقيقة.*

ورغم أنه اعتبر أن W أكثر تعقيدًا وأقل كفاءة، فقد قدمها في منشوره قبل J. وتكمن أهميتها عندما تكون التأثيرات الجانبية غير متاحة أو غير مرغوبة. كما أن W ضرورية لإثبات الإتمام، وهو ما فصله ميلنر ضمن إثبات الصحة.

### التزامات الإثبات

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

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

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

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


\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}


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

ولإثبات هذه الالتزامات بشكل صحيح، لا بد أولًا من تقويتها للسماح بتفعيل مبرهنة الاستبدال التي تمرر الاستبدال S عبر \vdash_S و\vdash_W. ومن هناك، تُبنى الإثباتات بالاستقراء على بنية التعبير.

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

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

#### قاعدة الإسناد النمطي

تُظهر الورقة الأصلية أن العودية يمكن تحقيقها بواسطة مركب:

\mathit{fix}:\forall\alpha.(\alpha\rightarrow\alpha)\rightarrow\alpha.

وبالتالي يمكن صياغة تعريف عودي محتمل كالتالي:

\mathtt{rec}\ v = e_1\ \mathtt{in}\ e_2\ ::=\mathtt{let}\ v = \mathit{fix}(\lambda v.e_1)\ \mathtt{in}\ e_2.

وبديلًا عن ذلك، يمكن توسيع صياغة التعبير وإضافة قاعدة نمطية إضافية:

:\displaystyle\frac{
\Gamma, \Gamma' \vdash e_1:\tau_1\quad\dots\quad\Gamma, \Gamma' \vdash e_n:\tau_n\quad\Gamma, \Gamma* \vdash e:\tau
}{
\Gamma\ \vdash\ \mathtt{rec}\ v_1 = e_1\ \mathtt{and}\ \dots\ \mathtt{and}\ v_n = e_n\ \mathtt{in}\ e:\tau
}\quad[\mathtt{Rec}]</math>

حيث:
* <math>\Gamma' = v_1:\tau_1,\ \dots,\ v_n:\tau_n</math>
* <math>\Gamma* = v_1:\bar\Gamma(\ \tau_1\ ),\ \dots,\ v_n:\bar\Gamma(\ \tau_n\ )

وهذا يدمج بشكل أساسي بين [\mathtt{Abs}] و[\mathtt{Let}] مع تضمين المتغيرات المعرفة عوديًا في مواضع النمط الأحادي عندما تظهر على يسار \mathtt{in}، ولكن كنمط متعدد عندما تكون على يمينها.

#### العواقب

رغم أن ما سبق يبدو مباشرًا، إلا أن له ثمنًا.

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

* يتم إبطال خاصية التطبيع القوي، لأنه يمكن صياغة عبارات غير منتهية.
* يُمسّ المنطق والاتساق، لأن النمط \forall a. a يصبح مُسكنًا.

### التحميل الزائد

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

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

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


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


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

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

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

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

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

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

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

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

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

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

## ملاحظات

## المراجع

* 
* 

## روابط خارجية
* تنفيذ بلغة هاسكل موضح خطوة بخطوة لخوارزمية W مع الشيفرة المصدرية على GitHub.
* تنفيذ بسيط لخوارزمية هندلي-ميلنر بلغة بايثون.

تصنيف:أنظمة أنواع
تصنيف:نظرية النمط
تصنيف:حسابات اللامدا
تصنيف:علم الحاسوب النظري
تصنيف:طرق شكلية
تصنيف:علم الحاسوب في 1969
تصنيف:علم الحاسوب في 1978
تصنيف:علم الحاسوب في 1985
تصنيف:خوارزميات