المفسّرات

10. المفسّرات

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

يتطلب الفهم الكامل للتصريف مقررًا كاملًا أو مقررين. لذا سنلقي هنا نظرة موجزة بالضرورة على كيفية تنفيذ لغات البرمجة. والهدف فهم بعض تقنيات التنفيذ الأساسية، لإزالة الغموض عن الأدوات التي تستخدمها. فرغم أنك قد لا تحتاج أبدًا إلى تنفيذ لغة برمجة عامة الغرض كاملة، فمن المرجح جدًا أنك ستريد في مرحلة ما من مسيرتك تصميم لغة صغيرة خاصة الغرض وتنفيذها. ويُسمى ذلك أحيانًا اللغات الخاصة بمجال (domain-specific languages, DSLs). وما نغطيه هنا ينبغي أن يساعدك في تلك المهمة.

المصرّف (compiler) برنامج ينفّذ لغة برمجة. وكذلك المفسّر (interpreter). لكنهما يختلفان في استراتيجية التنفيذ.

المهمة الأساسية للمصرّف هي الترجمة (translation). فهو يأخذ كمدخل برنامجًا مصدريًا (source program) وينتج كمخرج برنامجًا هدفًا (target program). والبرنامج المصدري يُعبَّر عنه عادةً بلغة عالية المستوى، مثل Java أو OCaml. والبرنامج الهدف يُعبَّر عنه عادةً بلغة منخفضة المستوى، مثل لغة تجميع MIPS أو x86. وعندها تنتهي مهمة المصرّف، ولا تبقى حاجة إليه. ويساعد نظام التشغيل لاحقًا في تحميل البرنامج الهدف وتنفيذه. وعادةً ما ينتج عن المصرّف تنفيذات أعلى أداءً.

أما المهمة الأساسية للمفسّر فهي التنفيذ (execution). فهو يأخذ كمدخل برنامجًا مصدريًا وينفّذ ذلك البرنامج مباشرةً دون إنتاج أي برنامج هدف. ونظام التشغيل هو الذي يحمّل المفسّر وينفّذه فعلًا، ثم يكون المفسّر مسؤولًا عن تنفيذ البرنامج. وعادةً ما يكون تنفيذ المفسّر أسهل من تنفيذ المصرّف.

ومن الممكن أيضًا تنفيذ لغة بمزيج من التصريف والتفسير. وأكثر مثال شائع على ذلك الآلات الافتراضية (virtual machines) التي تنفّذ شيفرة البايت (bytecode)، مثل آلة Java الافتراضية (JVM) أو آلة OCaml الافتراضية (التي كانت تُسمى آلة الزنك). وبهذه الاستراتيجية، يترجم المصرّف اللغة المصدرية إلى شيفرة البايت، وتفسّر الآلة الافتراضية شيفرة البايت.

وتذهب الآلات الافتراضية عالية الأداء، مثل HotSpot في Java، خطوة أبعد وتضمّن مصرّفًا داخل الآلة الافتراضية. فعندما تلاحظ الآلة أن قطعة من شيفرة البايت تُفسَّر كثيرًا، تستخدم المصرّف لترجمة تلك الشيفرة إلى لغة الآلة التي تعمل عليها الآلة (مثل x86). ويُسمى ذلك التصريف في الوقت المناسب (just-in-time compilation, JIT)، لأن الشيفرة تُصرَّف قبيل تنفيذها مباشرةً.

يمرّ المصرّف بعدة مراحل وهو يترجم برنامجًا:

التحليل المعجمي (Lexing). يحوّل المصرّف أثناء التحليل المعجمي شيفرة البرنامج المصدرية الأصلية من متتالية من المحارف إلى متتالية من الوحدات المعجمية (tokens). والوحدات المعجمية محارف متجاورة يكون لاجتماعها معنى. ويمكنك التفكير فيها على أنها نظير الكلمات في اللغة الطبيعية. بل إن الكلمات المفتاحية مثل if وmatch وحدات معجمية في OCaml. وكذلك الثوابت مثل 42 و"hello"، وأسماء المتغيرات مثل x وlst، وعلامات الترقيم مثل ( و) و->. ويزيل التحليل المعجمي عادةً المسافات البيضاء، لأنها لا تلزم بعد تحديد الوحدات المعجمية. (وإن كان يجب الحفاظ عليها في لغة حساسة للمسافات البيضاء مثل Python.)

التحليل النحوي (Parsing). يحوّل المصرّف أثناء التحليل النحوي متتالية الوحدات المعجمية إلى شجرة تُسمى شجرة الصياغة المجرّدة (abstract syntax tree, AST). وكما يوحي الاسم، تجرّد هذه الشجرة من الصياغة الملموسة (concrete syntax) للغة. تذكّر أن التجريد قد يعني «نسيان التفاصيل». وتنسى الشجرة عادةً التفاصيل الملموسة. فمثلًا:

في 1 + (2 + 3) تجمع الأقواس عملية الجمع اليمنى، مما يشير إلى أنه ينبغي تقييمها أولًا. ويمكن لشجرة تمثيل ذلك كما يلي:

   +
  / \
 1   +
    / \
   2   3

لم تعد الأقواس لازمة، لأن بنية الشجرة تُضمّنها.

وفي [1; 2; 3]، تحدّد الأقواس المربعة بداية القائمة ونهايتها، وتفصل الفواصل المنقوطة عناصر القائمة. ويمكن لشجرة تمثيل ذلك كعقدة لها عدة أبناء:

   list
  /  |  \
 1   2   3

لم تعد الأقواس والفواصل المنقوطة لازمة.

وفي fun x -> 42، تفصل الكلمة المفتاحية fun وعلامة الترقيم -> وسائط الدالة وجسمها عن الشيفرة المحيطة. ويمكن لشجرة تمثيل ذلك كعقدة لها ابنان:

  function
  /     \
 x       42

لم تعد الكلمة المفتاحية وعلامة الترقيم لازمتين.

وهكذا تمثل شجرة الصياغة المجرّدة بنية البرنامج على مستوى يسهل على كاتب المصرّف التعامل معه.

التحليل الدلالي (Semantic analysis). يتحقق المصرّف أثناء التحليل الدلالي مما إذا كان البرنامج ذا معنى وفق قواعد اللغة التي ينفّذها المصرّف. وأكثر أنواع التحليل الدلالي شيوعًا فحص الأنواع (type checking): فيحلل المصرّف أنواع جميع التعبيرات التي تظهر في البرنامج لمعرفة ما إذا كان هناك خطأ نوعي. ويتطلب فحص الأنواع عادةً إنتاج بنية بيانات تُسمى جدول الرموز (symbol table) تربط المعرّفات (مثل أسماء المتغيرات) بأنواعها. وعند الدخول في نطاق جديد، يُمتد جدول الرموز بارتباطات جديدة قد تحجب ارتباطات قديمة؛ وعند الخروج من النطاق، تُزال الارتباطات الجديدة، فتستعاد الارتباطات القديمة. لذا يمزج جدول الرموز سمات القاموس وسمات بنية بيانات المكدس.

وعلاوة على فحص الأنواع، ثمة أنواع أخرى من التحليل الدلالي. ومن الأمثلة على ذلك:

• التحقق مما إذا كانت فروع مطابقة الأنماط في OCaml شاملة،
• والتحقق مما إذا كانت الكلمة المفتاحية break في C تقع داخل جسم حلقة، و
• والتحقق مما إذا كان حقل في Java موسومًا بـ final قد هُيّئ قبل نهاية مُنشئ.

ويمكنك التفكير في التحليل النحوي على أنه «التحقق مما إذا كان البرنامج ذا معنى»—وهو تعريفنا للتحليل الدلالي قبل قليل. لذا فالتمييز بين التحليل النحوي والتحليل الدلالي يتعلق بالملاءمة أكثر: فالتحليل النحوي يؤدي عملًا كافيًا لتنفيذ إنتاج شجرة الصياغة المجرّدة، ويتولى التحليل الدلالي بقية العمل.

بل إن التحليل الدلالي ضروري أحيانًا لتحديد ما ينبغي أن تكون عليه شجرة الصياغة المجرّدة تحديدًا كاملًا! تأمل مثلًا التعبير (foo) - bar في لغة شبيهة بـ C. فقد يكون:

• نفيًا أحاديًا لمتغير bar محوّلًا إلى النوع foo، أو
• عملية طرح ثنائية بمعاملين هما foo وbar، كانت الأقواس حولها زائدة.

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

الترجمة إلى تمثيل وسيط. بعد التحليل الدلالي، يمكن للمصرّف أن يترجم شجرة الصياغة المجرّدة (معزّزة بجداول الرموز) فورًا إلى اللغة الهدف. لكن لو أراد المصرّف نفسه إنتاج مخرجات لأهداف متعددة (مثل x86 وARM وMIPS)، فسيقتضي ذلك تعريف ترجمة من الشجرة إلى كل هدف من الأهداف. وعمليًا لا يفعل المصرّفات ذلك عادةً. بل تترجم الشجرة أولًا إلى تمثيل وسيط (IR). فكّر في التمثيل الوسيط كنوع من تجريد كثير من لغات التجميع. فيمكن ترجمة لغات مصدرية كثيرة (مثل C وJava وOCaml) إلى التمثيل الوسيط نفسه، ومن ذلك التمثيل يمكن إنتاج مخرجات لغات هدف كثيرة (مثل x86 وARM وMIPS).

وتحتوي لغة التمثيل الوسيط عادةً تعليمات آلة مجرّدة (abstract machine instructions) تؤدي مهام بسيطة مفهوميًا: التحميل من الذاكرة أو التخزين فيها، وإجراء عمليات ثنائية، والاستدعاء والعودة، والقفز إلى تعليمات أخرى. وتحتوي الآلة المجرّدة عادةً عددًا غير محدود من السجلات المتاحة للاستخدام، كثيرًا مثل قدرة البرنامج المصدري على امتلاك عدد غير محدود من المتغيرات. أما الآلات الحقيقية فلها عدد منتهٍ من السجلات، وهو أحد أوجه كون التمثيل الوسيط تجريدًا.

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

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

مجموعات المراحل. يمكن تجميع مراحل التصريف في جزأين أو ثلاثة:

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

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

وسنركز في بقية هذا الكتاب على المفسّرات. وسنغفل التمثيلات الوسيطة وتوليد الشيفرة، وندرس بدلًا من ذلك كيفية تنفيذ شجرة الصياغة المجرّدة مباشرةً.

ملاحظة

بسبب الأدوات الإضافية المطلوبة، لا يمكن تشغيل شيفرة هذا الفصل في متصفح كما في الفصول السابقة. لكننا نوفر شيفرة قابلة للتنزيل لكل مفسّر منفَّذ هنا.

10.1. مثال: الآلة الحاسبة

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

10.2. التحليل النحوي

يمكن أن تكتب محلّلك المعجمي ومحلّلك النحوي بنفسك من الصفر. لكن لغات كثيرة تتضمن أدوات لتوليد المحلّلات المعجمية والنحوية تلقائيًا من أوصاف صورية لصياغة اللغة. وأسلاف كثير من تلك الأدوات هما lex وyacc، اللذان يولّدان المحلّلات المعجمية والنحوية على الترتيب؛ وقد طوّر lex وyacc في السبعينيات لـ C.

وتوفر OCaml، كجزء من التوزيع القياسي، مولّدي محلّلات معجمية ونحوية يُسميان ocamllex وocamlyacc. وهناك مولّد محلّلات نحوية أحدث يُسمى menhir متاح عبر opam؛ وهو «متوافق بنسبة 90%» مع ocamlyacc ويوفر دعمًا محسّنًا محسّنًا كثيرًا لتنقيح المحلّلات النحوية المولَّدة.

10.2.1. المحلّلات المعجمية

يُبنى مولّدو المحلّلات المعجمية مثل lex وocamllex على نظرية الآلات المحدودة الحتمية، التي تُدرس عادةً في مقرر الرياضيات المتقطعة أو نظرية الحوسبة. وتقبل تلك الآلات اللغات المنتظمة (regular languages)، التي يمكن وصفها بـالتعبيرات النمطية (regular expressions). لذا فمدخل مولّد المحلّل المعجمي مجموعة من التعبيرات النمطية التي تصف الوحدات المعجمية للغة. ومخرجه آلة منفَّذة بلغة عالية المستوى، مثل C (لـ lex) أو OCaml (لـ ocamllex).

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

10.2.2. المحلّلات النحوية

يُبنى مولّدو المحلّلات النحوية مثل yacc وmenhir بالمثل على نظرية الآلات. لكنها تستخدم آلات الدفع السفلي (pushdown automata)، وهي مثل الآلات المحدودة لكنها تحتفظ أيضًا بمكدس يمكنها الدفع إليه بسحب الرموز منه. ويمكّنها المكدس من قبول صنف أكبر من اللغات، تُعرف بـاللغات الحرة السياق (context-free languages, CFLs). ومن التحسينات الكبيرة التي أحدثتها اللغات الحرة السياق على اللغات المنتظمة قدرتها على التعبير عن فكرة وجوب توازن الفواصل—فمثلًا أن يكون كل قوس فتح موازنًا بقوس إغلاق.

وكما يمكن التعبير عن اللغات المنتظمة بترميز خاص (التعبيرات النمطية)، يمكن التعبير عن اللغات الحرة السياق كذلك. وتُستخدم القواعد الحرة السياق (context-free grammars) لوصف اللغات الحرة السياق. والقاعدة الحرة السياق مجموعة من قواعد الإنتاج (production rules) تصف كيف يمكن استبدال رمز برموز أخرى. فمثلًا، لغة الأقواس المتوازنة، التي تتضمن سلاسل مثل (()) و()() و(()())، لكن ليس سلاسل مثل ) أو (()، تولّدها هذه القواعد:

• $S \rightarrow (S)$
• $S \rightarrow SS$
• $S \rightarrow \epsilon$

والرموز الظاهرة في تلك القواعد هي $S$ و$($ و$)$. و$\epsilon$ يرمز إلى السلسلة الفارغة. وكل رمز إما غير طرفي (nonterminal) وإما طرفي (terminal)، حسب ما إذا كان وحدة معجمية في اللغة الموصوفة. و$S$ غير طرفي في المثال أعلاه، والقوسان ( و) طرفيان.

وسندرس في القسم التالي صيغة باكوس-ناور (Backus-Naur Form, BNF)، وهي ترميز قياسي للقواعد الحرة السياق. ومدخل مولّد المحلّل النحوي وصف BNF لصياغة اللغة عادةً. ومخرج مولّد المحلّل النحوي برنامج يتعرف على لغة القواعد. ويتوقع ذلك البرنامج، كمدخل، مخرجات المحلّل المعجمي. وينتج، كمخرج، قيمة من نوع شجرة الصياغة المجرّدة تمثل السلسلة التي قُبلت. وهكذا يعتمد البرنامجان اللذان يولّدهما مولّد المحلّل النحوي ومولّد المحلّل المعجمي كل منهما على الآخر وعلى نوع شجرة الصياغة المجرّدة.

10.2.3. صيغة باكوس-ناور

الطريقة القياسية لوصف صياغة لغة هي ترميز رياضي يُسمى صيغة باكوس-ناور (BNF)، منسوبًا إلى مخترعيها John Backus و Peter Naur. وثمة صيغ كثيرة لـ BNF. ولن نكون هنا شديدي التمسك بصيغة بعينها دون أخرى. وهدفنا مجرد امتلاك ترميز جيد بدرجة معقولة لوصف صياغة اللغات.

يستخدم BNF مجموعة من قواعد الاشتقاق (derivation rules) لوصف صياغة لغة. ولنبدأ بمثال. إليك وصف BNF للغة صغيرة من التعبيرات تتضمن الأعداد الصحيحة والجمع فحسب:

e ::= i | e + e
i ::= <integers>

تقول هذه القواعد إن التعبير e إما عدد صحيح i، وإما تعبيران يظهر بينهما الرمز +. أما صياغة «الأعداد الصحيحة» فتتركها هذه القواعد غير محددة.

ولكل قاعدة الشكل

metavariable ::= symbols | ... | symbols

والمتغير الفوقي (metavariable) متغير يُستخدم في قواعد BNF، لا متغير في اللغة الموصوفة. أما ::= و| الظاهران في القواعد فهما صياغة فوقية (metasyntax): صياغة BNF المستخدمة لوصف صياغة اللغة. والرموز (symbols) متتاليات يمكن أن تتضمن متغيرات فوقية (مثل i وe) ووحدات معجمية في اللغة (مثل +). ولا تلزم المسافات البيضاء في هذه القواعد.

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

e ::= i | e1 + e2

أو

e ::= i | e + e'

الآن يمكننا الحديث عن e2 أو e' بدلًا من الاضطرار إلى القول «الـ e في الطرف الأيمن من +».

وإذا كانت اللغة نفسها تحتوي أيًا من الوحدتين المعجميتين ::= أو |—وOCaml تحتوي الثانية—فقد تصير كتابة BNF مربكة قليلًا. وتحاول بعض ترميزات BNF معالجة ذلك باستخدام فواصل إضافية لتمييز الصياغة من الصياغة الفوقية. وسنكون أكثر تسامحًا ونفترض أن القارئ يستطيع تمييزها.

10.2.4. مثال: SimPL

ولنستعمل كمثال جارٍ لغة برمجة بسيطة جدًا نسميها SimPL. وإليك صياغتها في BNF:

e ::= x | i | b | e1 bop e2
    | if e1 then e2 else e3
    | let x = e1 in e2

bop ::= + | * | <=

x ::= <identifiers>

i ::= <integers>

b ::= true | false

من الواضح أن هذا اللغة ينقصها الكثير، ولا سيما الدوال. لكن فيها ما يكفي لدراسة المفاهيم المهمة للمفسّرات دون أن تشتتنا ميزات لغوية كثيرة. وسننظر لاحقًا في جزء أكبر من OCaml.

وسنطوّر مفسّرًا كاملًا لـ SimPL. ويمكنك تنزيل المفسّر المكتمل هنا: simpl.zip. أو تابع معنا ونحن نبني كل جزء منه.

10.2.4.1. شجرة الصياغة المجرّدة

بما أن شجرة الصياغة المجرّدة أهم بنية بيانات في المفسّر، فلنصممها أولًا. وسنضع هذه الشيفرة في ملف باسم ast.ml:

type bop =
  | Add
  | Mult
  | Leq
type expr =
  | Var of string
  | Int of int
  | Bool of bool
  | Binop of bop * expr * expr
  | Let of string * expr * expr
  | If of expr * expr * expr

يوجد منشئ واحد لكل شكل من أشكال التعبيرات النحوية في BNF. وللأصناف النحوية الأولية الأساسية، أي المعرّفات والأعداد الصحيحة والقيم المنطقية، نستخدم أنواع OCaml نفسها: string وint وbool.

وبدلًا من تعريف نوع bop ومنشئ واحد Binop، كان يمكننا تعريف ثلاثة منشئات منفصلة للعوامل الثنائية الثلاثة:

type expr =
  ...
  | Add of expr * expr
  | Mult of expr * expr
  | Leq of expr * expr
  ...

لكن باستخلاص نوع bop سنتمكن من تفادي كثير من تكرار الشيفرة لاحقًا في تنفيذنا.

10.2.4.2. محلّل Menhir النحوي

لنبدأ بالتحليل النحوي، ثم نعود إلى التحليل المعجمي لاحقًا. وسنضع كل شيفرة Menhir التي نكتبها أدناه في ملف باسم parser.mly. وامتداد .mly يشير إلى أن هذا الملف مقصود كمدخل إلى Menhir. (وحرف ‘y’ تلميح إلى yacc.) ويحتوي هذا الملف على تعريف القواعد (grammar definition) للغة التي نريد تحليلها. وسيوصف تركيب تعريفات القواعد بالأمثلة أدناه. وكن على حذر، فهو غريب قليلًا ربما، لكن ذلك لأنه قائم على أدوات (مثل yacc) طُوّرت منذ زمن بعيد. وسيعالج Menhir ذلك الملف وينتج ملفًا باسم parser.ml كمخرج؛ يحتوي برنامج OCaml يحلّل اللغة نحويًا. (ولا شيء مميز في اسم parser هنا؛ إنه وصفي فحسب.)

ولتعريف القواعد أربعة أجزاء: الترويسة، والإعلانات، والقواعد، والذيل.

الترويسة (Header). تظهر الترويسة بين %{ و%}. وهي شيفرة ستُنسخ حرفيًا إلى الملف parser.ml المولَّد. ونستخدمها هنا فقط لفتح وحدة Ast بحيث يمكننا، لاحقًا في تعريف القواعد، كتابة تعبيرات مثل Int i بدلًا من Ast.Int i. ولو أردنا، أمكننا أيضًا تعريف بعض دوال OCaml في الترويسة.

%{
open Ast
%}

الإعلانات (Declarations). يبدأ قسم الإعلانات ببيان الوحدات المعجمية للغة. وإليك إعلانات الوحدات المعجمية لـ SimPL:

%token <int> INT
%token <string> ID
%token TRUE
%token FALSE
%token LEQ
%token TIMES
%token PLUS
%token LPAREN
%token RPAREN
%token LET
%token EQUALS
%token IN
%token IF
%token THEN
%token ELSE
%token EOF

كل واحد منها مجرد اسم وصفي للوحدة المعجمية. ولا شيء حتى الآن يقول إن LPAREN يقابل ( فعلًا، مثلًا. وسنتولى ذلك عندما نعرّف المحلّل المعجمي.

ووحدة EOF وحدة معجمية خاصة هي نهاية الملف (end-of-file) يعيدها المحلّل المعجمي عند وصوله إلى نهاية تيار المحارف. وعندها نعرف أن البرنامج كله قد قُرئ.

والوحدات المعجمية التي يظهر فيها توسيم `` تعلن أنها ستحمل معها بعض البيانات الإضافية. وفي حالة INT تكون تلك البيانات int في OCaml. وفي حالة ID تكون string في OCaml.

وبعد إعلان الوحدات المعجمية، علينا تقديم بعض المعلومات الإضافية عن الأسبقية (precedence) والتجميعية (associativity). وتقول الإعلانات التالية إن PLUS تجميعي يساري، وIN غير تجميعي، وPLUS له أسبقية أعلى من IN (لأن PLUS يظهر في سطر بعد IN).

%nonassoc IN
%nonassoc ELSE
%left LEQ
%left PLUS
%left TIMES

ولأن PLUS تجميعي يساري، سيُحلَّل 1 + 2 + 3 نحويًا كـ (1 + 2) + 3 لا كـ 1 + (2 + 3). ولأن PLUS له أسبقية أعلى من IN، سيُحلَّل التعبير let x = 1 in x + 2 نحويًا كـ let x = 1 in (x + 2) لا كـ (let x = 1 in x) + 2. وللإعلانات الأخرى تأثيرات مشابهة.

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

وبعد إعلان التجميعية والأسبقية، علينا إعلان نقطة البداية لتحليل اللغة نحويًا. ويقول الإعلان التالي إن نبدأ بقاعدة (معرَّفة أدناه) اسمها prog. ويقول الإعلان أيضًا إن تحليل prog نحويًا سيعيد قيمة OCaml من النوع Ast.expr.

%start <Ast.expr> prog

وأخيرًا، تُنهي %% قسم الإعلانات.

%%

القواعد (Rules). يحتوي قسم القواعد قواعد إنتاج تشبه BNF، وإن كانت هذه القواعد تكتب «:» ببساطة حيث نكتب «::=» في BNF. وصيغة القاعدة هي

name:
  | production1 { action1 }
  | production2 { action2 }
  | ...
  ;

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

القاعدة الأولى، المسماة prog، لها إنتاج واحد فقط. وتقول إن prog هو expr يتبعه EOF. والجزء الأول من الإنتاج، e=expr، يقول بمطابقة expr وربط القيمة الناتجة بـ e. ويقول الإجراء ببساطة بإعادة تلك القيمة e.

prog:
  | e = expr; EOF { e }
  ;

والقاعدة الثانية والأخيرة، المسماة expr، لها إنتاجات لجميع التعبيرات في SimPL.

expr:
  | i = INT { Int i }
  | x = ID { Var x }
  | TRUE { Bool true }
  | FALSE { Bool false }
  | e1 = expr; LEQ; e2 = expr { Binop (Leq, e1, e2) }
  | e1 = expr; TIMES; e2 = expr { Binop (Mult, e1, e2) }
  | e1 = expr; PLUS; e2 = expr { Binop (Add, e1, e2) }
  | LET; x = ID; EQUALS; e1 = expr; IN; e2 = expr { Let (x, e1, e2) }
  | IF; e1 = expr; THEN; e2 = expr; ELSE; e3 = expr { If (e1, e2, e3) }
  | LPAREN; e=expr; RPAREN {e}
  ;

• الإنتاج الأول، i = INT، يقول بمطابقة وحدة معجمية INT، وربط قيمة int الناتجة في OCaml بـ i، وإعادة عقدة شجرة الصياغة المجرّدة Int i.
• والإنتاج الثاني، x = ID، يقول بمطابقة وحدة ID، وربط قيمة string الناتجة في OCaml بـ x، وإعادة عقدة شجرة الصياغة المجرّدة Var x.
• ويطابق الإنتاجان الثالث والرابع وحدة TRUE أو FALSE ويعيدان عقدة شجرة الصياغة المجرّدة المقابلة.
• وتعالج الإنتاجات الخامس والسادس والسابع العوامل الثنائية. فمثلًا، e1 = expr; PLUS; e2 = expr يقول بمطابقة expr يتبعه وحدة PLUS يتبعها expr آخر. ويُربط التعبير الأول expr بـ e1 والثاني بـ e2. وعقدة شجرة الصياغة المجرّدة المعادة هي Binop (Add, e1, e2).
• والإنتاج الثامن، LET; x = ID; EQUALS; e1 = expr; IN; e2 = expr، يقول بمطابقة وحدة LET تتبعها وحدة ID تتبعها وحدة EQUALS يتبعها expr تتبعها وحدة IN يتبعها expr آخر. وتُربط السلسلة التي تحملها ID بـ x، ويُربط التعبيران بـ e1 وe2. وعقدة شجرة الصياغة المجرّدة المعادة هي Let (x, e1, e2).
• والإنتاج الأخير، LPAREN; e = expr; RPAREN، يقول بمطابقة وحدة LPAREN يتبعها expr تتبعها RPAREN. ويُربط التعبير بـ e ويُعاد.

وقد يثير الإنتاج الأخير الدهشة، لأنه لم يكن مدرجًا في BNF التي كتبناها لـ SimPL. فقد كانت تلك BNF مقصودًا بها وصف الصياغة المجرّدة للغة، فلم تتضمن التفاصيل الملموسة لكيفية تجميع التعبيرات بالأقواس. أما تعريف القواعد الذي كنا نكتبه فيجب أن يصف الصياغة الملموسة، بما في ذلك تفاصيل مثل الأقواس.

وقد يوجد أيضًا قسم ذيل (trailer) بعد القواعد، وهو مثل الترويسة شيفرة OCaml تُنسخ مباشرةً إلى ملف المخرج parser.ml.

10.2.4.3. محلّل Ocamllex المعجمي

ولنرَ الآن كيف يُستخدم مولّد المحلّل المعجمي. سيبدو كثير منه مألوفًا من نقاشنا لمولّد المحلّل النحوي. وسنضع كل شيفرة ocamllex التي نكتبها أدناه في ملف باسم lexer.mll. وامتداد .mll يشير إلى أن هذا الملف مقصود كمدخل إلى ocamllex. (وحرف ‘l’ تلميح إلى التحليل المعجمي.) ويحتوي هذا الملف على تعريف المحلّل المعجمي للغة التي نريد تحليلها معجميًا. وسيعالج Menhir ذلك الملف وينتج ملفًا باسم lexer.ml كمخرج؛ يحتوي برنامج OCaml يحلّل اللغة معجميًا. (ولا شيء مميز في اسم lexer هنا؛ إنه وصفي فحسب.)

ولتعريف المحلّل المعجمي أربعة أجزاء: الترويسة، والمعرّفات، والقواعد، والذيل.

الترويسة (Header). تظهر الترويسة بين { و}. وهي شيفرة ستُنسخ حرفيًا ببساطة إلى الملف lexer.ml المولَّد.

{
open Parser
}

هنا فتحنا وحدة Parser، وهي الشيفرة في parser.ml التي أنتجها Menhir من parser.mly. وسبب فتحها أن نتمكن من استخدام أسماء الوحدات المعجمية المعلنة فيها، مثل TRUE وLET وINT، داخل تعريف محلّلنا المعجمي. وإلا لاضطررنا إلى كتابة Parser.TRUE وما إلى ذلك.

المعرّفات (Identifiers). يحتوي القسم التالي من تعريف المحلّل المعجمي على معرّفات (identifiers)، وهي تعبيرات نمطية مسماة. وستُستخدم في قسم القواعد بعد ذلك.

وإليك المعرّفات التي سنستخدمها مع SimPL:

let white = [' ' '\t']+
let digit = ['0'-'9']
let int = '-'? digit+
let letter = ['a'-'z' 'A'-'Z']
let id = letter+

التعبيرات النمطية أعلاه للمسافات البيضاء (المسافات وأحرف الجدولة)، والأرقام (0 حتى 9)، والأعداد الصحيحة (متتاليات غير فارغة من الأرقام، تسبقها اختياريًا إشارة ناقص)، والأحرف (a حتى z، و A حتى Z)، وأسماء متغيرات SimPL (متتاليات غير فارغة من الأحرف)، أي ما يُعرف بالمعرّفات أو «identifiers»—وإننا نستخدم الكلمة الآن بمعنيين مختلفين.

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

وقسم المعرّفات غير مطلوب فعلًا؛ فبدلًا من كتابة white في القواعد، كان يمكننا كتابة التعبير النمطي لها مباشرةً. لكن المعرّفات تساعد في جعل تعريف المحلّل المعجمي أكثر توثيقًا لذاته.

القواعد (Rules). يُكتب قسم القواعد في تعريف المحلّل المعجمي بترميز يشبه BNF أيضًا. وللقاعدة الشكل

rule name =
  parse
  | regexp1 { action1 }
  | regexp2 { action2 }
  | ...

هنا، rule وparse كلمتان مفتاحيتان. وسيحاول المحلّل المعجمي المولَّد المطابقة مع التعبيرات النمطية بالترتيب المذكورة فيه. وعندما يطابق تعبير نمطي، ينتج المحلّل الوحدة المعجمية التي يحددها action الخاص بها.

وإليك القاعدة (الوحيدة) لمحلّل SimPL المعجمي:

rule read =
  parse
  | white { read lexbuf }
  | "true" { TRUE }
  | "false" { FALSE }
  | "<=" { LEQ }
  | "*" { TIMES }
  | "+" { PLUS }
  | "(" { LPAREN }
  | ")" { RPAREN }
  | "let" { LET }
  | "=" { EQUALS }
  | "in" { IN }
  | "if" { IF }
  | "then" { THEN }
  | "else" { ELSE }
  | id { ID (Lexing.lexeme lexbuf) }
  | int { INT (int_of_string (Lexing.lexeme lexbuf)) }
  | eof { EOF }

معظم التعبيرات النمطية والإجراءات بديهية، لكن اثنين منها ليسا كذلك:

• الأول، white { read lexbuf }، يعني أنه إذا طوبقت مسافة بيضاء، فعلى المحلّل المعجمي، بدلًا من إعادة وحدة معجمية، أن يستدعي قاعدة read مرة أخرى ويعيد أي وحدة معجمية تنتج. وبعبارة أخرى، ستُتجاهل المسافات البيضاء.
• والاثنان الخاصان بالمعرّفات والأعداد الصحيحة يستخدمان التعبير Lexing.lexeme lexbuf. وهذا يستدعي دالة lexeme المعرَّفة في وحدة Lexing، ويعيد السلسلة التي طابقها التعبير النمطي. فمثلًا، في قاعدة id سيعيد متتالية الأحرف الكبيرة والصغيرة التي تشكّل اسم المتغير.
• والتعبير النمطي eof تعبير خاص يطابق نهاية الملف (أو السلسلة) التي تُحلَّل معجميًا.

ولاحظ أنه من المهم أن يقع التعبير النمطي id قبل الأخير تقريبًا في القائمة. وإلا لحُلّلت كلمات مفتاحية مثل true وif معجميًا كأسماء متغيرات لا كوحدتي TRUE وIF.

10.2.4.4. توليد المحلّل النحوي والمحلّل المعجمي

والآن بعد أن أكملنا تعريفي المحلّل النحوي والمعجمي في parser.mly وlexer.mll، يمكننا تشغيل Menhir وocamllex لتوليد المحلّل النحوي والمعجمي منهما. ولننظّم شيفرتنا هكذا:

- <some root folder>
  - dune-project
  - src
    - ast.ml
    - dune
    - lexer.mll
    - parser.mly

وفي src/dune اكتب ما يلي:

(library
 (name interp))

(menhir
 (modules parser))

(ocamllex lexer)

فينظّم ذلك مجلد src كله في مكتبة اسمها Interp. وسيكون المحلّل النحوي والمعجمي وحدتين Interp.Parser وInterp.Lexer في تلك المكتبة.

ونفّذ dune build لتصريف الشيفرة، فتُولَّد بذلك المحلّل النحوي والمعجمي. وإذا أردت رؤية الشيفرة المولَّدة، فابحث في _build/default/src/ عن parser.ml وlexer.ml.

10.2.4.5. برنامج التشغيل

وأخيرًا يمكننا جمع المحلّل المعجمي والنحوي معًا لتحويل سلسلة نصية إلى شجرة صياغة مجرّدة. وضع هذه الشيفرة في ملف باسم src/main.ml:

open Ast
let parse (s : string) : expr =
  let lexbuf = Lexing.from_string s in
  let ast = Parser.prog Lexer.read lexbuf in
  ast

تأخذ هذه الدالة سلسلة s وتستخدم وحدة Lexing في المكتبة القياسية لإنشاء مخزن محلّل معجمي (lexer buffer) منها. فكّر في ذلك المخزن كتيار الوحدات المعجمية. ثم تحلّل الدالة السلسلة معجميًا ونحويًا إلى شجرة صياغة مجرّدة، باستخدام Lexer.read وParser.prog. وتقابل الدالة Lexer.read القاعدة المسماة read في تعريف محلّلنا المعجمي، وتقابل الدالة Parser.prog القاعدة المسماة prog في تعريف محلّلنا النحوي.

ولاحظ كيف تشغّل هذه الشيفرة المحلّل المعجمي على سلسلة نصية؛ وهناك دالة مقابلة هي from_channel للقراءة من ملف.

ويمكننا الآن استخدام parse تفاعليًا لتحليل بعض السلاسل. ابدأ utop وحمّل المكتبة المعلنة في src بهذا الأمر:

$ dune utop src

الآن صار Interp.Main.parse متاحًا للاستخدام:

# Interp.Main.parse "let x = 3110 in x + x";;
- : Interp.Ast.expr =
Interp.Ast.Let ("x", Interp.Ast.Int 3110,
 Interp.Ast.Binop (Interp.Ast.Add, Interp.Ast.Var "x", Interp.Ast.Var "x"))

وبذلك يكتمل التحليل المعجمي والنحوي لـ SimPL.

10.3. نموذج الاستبدال

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

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

ويُسمى إزالة السكر النحوي إزالة السكر (desugaring). فمثلًا، نعلم أن let x = e1 in e2 و(fun x -> e2) e1 متكافئان. لذا يمكننا اعتبار تعبيرات let سكرًا نحويًا.

لنفترض أن لدينا لغة تقابل شجرة صياغتها المجرّدة هذه BNF:

e ::= x | fun x -> e | e1 e2
    | let x = e1 in e2

حينئذٍ يمكن للمفسّر أن يزيل السكر من تلك الشجرة إلى شجرة أبسط—وهي تمثيل وسيط بمعنى ما—بتحويل جميع ورود let x = e1 in e2 إلى (fun x -> e2) e1. ثم لا يحتاج المفسّر إلى تقييم إلا هذه اللغة الأصغر:

e ::= x | fun x -> e | e1 e2

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

التقييم بالخطوة الكبيرة مقابل الخطوة الصغيرة. سنعرّف التقييم بعلاقة رياضية، كما فعلنا مع فحص الأنواع. بل سنعرّف ثلاث علاقات للتقييم:

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

والأسلوب الذي نعرّف به التقييم بهذه العلاقات يُعرف بـ الدلالات التشغيلية (operational semantics)، لأننا نستخدم العلاقات لتحديد كيفية «تشغيل» الآلة وهي تقيّم البرامج. وهناك أسلوبان رئيسيان آخران، يُعرفان بـ الدلالات الإشارية (denotational semantics) والدلالات المسلّمية (axiomatic semantics)، لكننا لن نغطيهما هنا.

ويمكننا تقسيم الدلالات التشغيلية كذلك إلى أسلوبين فرعيين لتعريف التقييم: دلالات الخطوة الصغيرة (small step) مقابل الخطوة الكبيرة (big step). فالعلاقة الأولى، -->، بأسلوب الخطوة الصغيرة، لأنها تمثل التنفيذ بدلالة خطوات صغيرة فردية. والثالثة، ==>، بأسلوب الخطوة الكبيرة، لأنها تمثل التنفيذ بدلالة خطوة كبيرة من تعبير مباشرةً إلى قيمة. أما العلاقة الثانية، -->*، فتمزج الاثنين. بل إن رغبتنا أن تردم الفجوة بالمعنى التالي:

الربط بين الخطوات الكبيرة والصغيرة: لجميع التعبيرات e والقيم v، تصح e -->* v إذا وفقط إذا صحت e ==> v.

وبعبارة أخرى، إذا أخذ تعبير خطوات صغيرة كثيرة ووصل في النهاية إلى قيمة، مثل e --> e1 --> .... --> en --> v، فينبغي أن تصح e ==> v. فعلاقة الخطوة الكبيرة تجريد أمين لعلاقة الخطوة الصغيرة: فهي تنسى كل الخطوات الوسيطة فحسب.

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

نموذج الاستبدال مقابل نموذج البيئة. ثمة خيار آخر علينا اتخاذه، وهو متعامد مع اختيار الخطوة الصغيرة مقابل الكبيرة. فهناك طريقتان مختلفتان للتفكير في تنفيذ المتغيرات:

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

وتؤدي هاتان الفكرتان إلى نموذج الاستبدال (substitution model) للتقييم ونموذج البيئة (environment model) للتقييم. وكما في الخطوة الصغيرة مقابل الكبيرة، يميل نموذج الاستبدال إلى الأناقة الرياضية، بينما يميل نموذج البيئة إلى الشبه أكثر بكيفية تنفيذ المفسّر.

وستساعد أمثلة في استيعاب كل هذا. ولننظر بعد ذلك في كيفية تعريف العلاقات لـ SimPL.

10.3.1. تقييم SimPL في نموذج الاستبدال

لنبدأ بتعريف دلالات نموذج استبدال بالخطوة الصغيرة لـ SimPL. أي أننا سنعرّف علاقة --> تمثل كيفية أخذ التعبير خطوة واحدة في كل مرة، وسننفّذ المتغيرات باستبدال القيم بالأسماء.

تذكّر صياغة SimPL:

e ::= x | i | b | e1 bop e2
    | if e1 then e2 else e3
    | let x = e1 in e2

bop ::= + | * | <=

سنحتاج إلى معرفة متى ينتهي تقييم التعبيرات، أي متى تُعتبر قيمًا. وبالنسبة إلى SimPL، سنعرّف القيم كما يلي:

v ::= i | b

أي أن القيمة إما ثابت صحيح وإما ثابت منطقي.

وسنعرّف الآن، لكل شكل نحوي يمكن أن يكون عليه تعبير SimPL، بعض قواعد التقييم (evaluation rules) التي تشكّل تعريفًا استقرائيًا لعلاقة -->. وسيكون لكل قاعدة الشكل e --> e'، بمعنى أن e يأخذ خطوة واحدة إلى e'.

ورغم أن المتغيرات ترد أولًا في BNF، فلنتجاوزها الآن ونعد إليها بعد جميع الأشكال الأخرى.

الثوابت. الثوابت الصحيحة والمنطقية قيم بالفعل، فلا يمكنها أخذ خطوة. وقد يبدو ذلك مفاجئًا في البداية، لكن تذكّر أننا نعتزم تعريف علاقة -->* أيضًا تسمح بصفر خطوة أو أكثر؛ أما علاقة --> فتمثل خطوة واحدة بالضبط.

وتقنيًا، كل ما علينا فعله لتحقيق ذلك ألا نكتب أي قواعد بالشكل i --> e أو b --> e لأي e. لذا فقد انتهينا بالفعل في الواقع: فلم نعرّف أي قواعد بعد.

ولنستحدث ترميزًا آخر يُكتب e -/->، مقصودًا به أن يبدو كسهم يقطعه خط مائل، ليعني «لا يوجد e' بحيث e --> e'». وباستخدامه يمكننا كتابة:

• i -/->
• b -/->

ورغم أنهما ليسا جزءًا من تعريف --> بالمعنى الدقيق، فالقضيتان تساعداننا على تذكر أن الثوابت لا تأخذ خطوات. بل يمكننا بوجه أعم أن نكتب: «لكل v، تصح v -/->».

العوامل الثنائية. لتطبيق عامل ثنائي e1 bop e2 تعبيران فرعيان: e1 وe2. ويؤدي ذلك إلى بعض الخيارات حول كيفية تقييم التعبير:

• يمكننا تقييم الطرف الأيسر e1 أولًا، ثم الطرف الأيمن e2، ثم تطبيق العامل.
• أو يمكننا البدء بالطرف الأيمن ثم الأيسر.
• أو يمكننا تداخل التقييم، بأخذ خطوة في e1، ثم خطوة في e2، ثم خطوة في e1، ثم في e2، وهكذا.
• أو ربما كان العامل قاصرًا (short-circuit)، وفي هذه الحالة قد لا يُقيَّم أحد التعبيرين الفرعيين أبدًا.

وثمة استراتيجيات أخرى كثيرة قد تستطيع اختراعها.

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

وسيتوقع كثيرون التقييم من اليسار إلى اليمين، فلنعرّف علاقة --> وفق ذلك. نبدأ بالقول إن الطرف الأيسر يمكنه أخذ خطوة:

e1 bop e2 --> e1' bop e2
  if e1 --> e1'

ومثل نظام الأنواع لـ SimPL، تقول هذه القاعدة إن تعبيرين في علاقة --> إذا كان تعبيران فرعيان آخران (أبسط) في علاقة --> أيضًا. وهذا ما يجعلها تعريفًا استقرائيًا.

وإذا انتهى تقييم الطرف الأيسر، جاز للطرف الأيمن أن يبدأ أخذ الخطوات:

v1 bop e2 --> v1 bop e2'
  if e2 --> e2'

وأخيرًا، عندما يصل الطرفان إلى قيمة، يمكن تطبيق العامل الثنائي:

v1 bop v2 --> v
  if v is the result of primitive operation v1 bop v2

ونعني بـالعملية الأولية (primitive operation) وجود تصور أساسي لما يعنيه bop فعلًا. فمثلًا، المحرف + مجرد قطعة صياغة، لكننا معتادون على فهم معناه كعملية جمع حسابية. والعملية الأولية عادةً شيء ينفّذه العتاد (مثل رمز عملية ADD)، أو مكتبة وقت التشغيل (مثل دالة pow).

وبالنسبة إلى SimPL، لنوكل جميع العمليات الأولية إلى OCaml. أي أن عامل + في SimPL سيكون هو نفسه عامل + في OCaml، وكذلك * و<=.

وإليك مثالًا على استخدام قاعدة العامل الثنائي:

    (3*1000) + ((1*100) + ((1*10) + 0))
--> 3000 + ((1*100) + ((1*10) + 0))
--> 3000 + (100 + ((1*10) + 0))
--> 3000 + (100 + (10 + 0))
--> 3000 + (100 + 10)
--> 3000 + 110
--> 3110

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

أولًا، يُقيَّم الشرط إلى قيمة:

if e1 then e2 else e3 --> if e1' then e2 else e3
  if e1 --> e1'

ثم، بناءً على الشرط، يُبسَّط تعبير if إلى أحد الفرعين فحسب:

if true then e2 else e3 --> e2

if false then e2 else e3 --> e3

تعبيرات let. لنجعل تعبيرات let في SimPL تُقيَّم بالطريقة نفسها التي تُقيَّم بها تعبيرات let في OCaml: تعبير الارتباط أولًا، ثم الجسم.

والقاعدة التي تأخذ خطوة في تعبير الارتباط هي:

let x = e1 in e2 --> let x = e1' in e2
  if e1 --> e1'

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

let x = v1 in e2 --> e2 with v1 substituted for x

فمثلًا، ينبغي أن يأخذ let x = 42 in x + 1 خطوة إلى 42 + 1، لأن استبدال 42 بـ x في x + 1 يعطي 42 + 1.

وبالطبع، الطرف الأيمن من تلك القاعدة ليس تعبيرًا حقًا. إنه يعطي حدسًا فحسب عن التعبير الذي نريده فعلًا. ونحتاج إلى تعريف صوري لمعنى «الاستبدال». ويتبين أنه دقيق إلى حد ما. لذا، بدلًا من الانحراف به الآن، لنفترض ترميزًا جديدًا: e'{e/x}، ويعني «التعبير e' مع استبدال e بـ x». وسنعود إلى ذلك الترميز في القسم التالي ونعطيه تعريفًا دقيقًا.

وإلى ذلك الحين، يمكننا إضافة هذه القاعدة:

let x = v1 in e2 --> e2{v1/x}

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

تأمل OCaml: إذا حاولنا تقييم تعبير فيه متغير غير مرتبط، فماذا يحدث؟ لنتحقق في utop:

# x;;
Error: Unbound value x

# let y = x in y;;
Error: Unbound value x

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

ولذا لا نحتاج، كما في الثوابت، إلى إضافة أي قواعد للمتغيرات. لكن للوضوح يمكننا أن نقرر أن x -/->.

10.3.2. تنفيذ علاقة الخطوة الواحدة

من السهل تحويل التعريفات أعلاه لـ --> إلى دالة OCaml تطابق الأنماط على عقد شجرة الصياغة المجرّدة. وفي الشيفرة أدناه، تذكّر أننا لم ننتهِ بعد من تعريف الاستبدال (أي subst)؛ وسنعود إلى ذلك في القسم التالي.

(** [is_value e] is whether [e] is a value. *)
let is_value : expr -> bool = function
  | Int _ | Bool _ -> true
  | Var _ | Let _ | Binop _ | If _ -> false
(** [subst e v x] is [e{v/x}]. *)
let subst _ _ _ =
  failwith "See next section"
(** [step] is the [-->] relation, that is, a single step of
    evaluation. *)
let rec step : expr -> expr = function
  | Int _ | Bool _ -> failwith "Does not step"
  | Var _ -> failwith "Unbound variable"
  | Binop (bop, e1, e2) when is_value e1 && is_value e2 ->
    step_bop bop e1 e2
  | Binop (bop, e1, e2) when is_value e1 ->
    Binop (bop, e1, step e2)
  | Binop (bop, e1, e2) -> Binop (bop, step e1, e2)
  | Let (x, e1, e2) when is_value e1 -> subst e2 e1 x
  | Let (x, e1, e2) -> Let (x, step e1, e2)
  | If (Bool true, e2, _) -> e2
  | If (Bool false, _, e3) -> e3
  | If (Int _, _, _) -> failwith "Guard of if must have type bool"
  | If (e1, e2, e3) -> If (step e1, e2, e3)
(** [step_bop bop v1 v2] implements the primitive operation
    [v1 bop v2].  Requires: [v1] and [v2] are both values. *)
and step_bop bop e1 e2 = match bop, e1, e2 with
  | Add, Int a, Int b -> Int (a + b)
  | Mult, Int a, Int b -> Int (a * b)
  | Leq, Int a, Int b -> Bool (a <= b)
  | _ -> failwith "Operator and operand type mismatch"

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

10.3.3. علاقة الخطوات المتعددة

والآن بعد أن عرّفنا -->، لم يبقَ في الحقيقة ما نفعله لتعريف -->*. فهي مجرد الإغلاق الانعكاسي التعدي لـ -->. وبعبارة أخرى، يمكن تعريفها بهاتين القاعدتين فحسب:

e -->* e

e -->* e''
  if e --> e' and e' -->* e''

وبالطبع، ما نريده فعلًا عند تنفيذ مفسّر هو أخذ أكبر عدد ممكن من الخطوات حتى يصل التعبير إلى قيمة. أي أننا مهتمون بالعلاقة الجزئية e -->* v التي يكون طرفها الأيمن ليس مجرد تعبير، بل قيمة. ويسهل تنفيذ ذلك:

(** [eval_small e] is the [e -->* v] relation.  That is,
    keep applying [step] until a value is produced.  *)
let rec eval_small (e : expr) : expr =
  if is_value e then e
  else e |> step |> eval_small

10.3.4. تعريف علاقة الخطوة الكبيرة

تذكّر أن هدفنا من تعريف علاقة الخطوة الكبيرة ==> هو التأكد من توافقها مع علاقة الخطوات المتعددة -->*.

الثوابت سهلة، لأنها تصل بالخطوة الكبيرة إلى نفسها:

i ==> i

b ==> b

أما العوامل الثنائية فتصل بالخطوة الكبيرة عبر تعبيريها الفرعيين، ثم تطبّق العملية الأولية أيًا كانت:

e1 bop e2 ==> v
  if e1 ==> v1
  and e2 ==> v2
  and v is the result of primitive operation v1 bop v2

وتصل تعبيرات if بالخطوة الكبيرة عبر الشرط، ثم عبر أحد الفرعين:

if e1 then e2 else e3 ==> v2
  if e1 ==> true
  and e2 ==> v2

if e1 then e2 else e3 ==> v3
  if e1 ==> false
  and e3 ==> v3

وتصل تعبيرات let بالخطوة الكبيرة عبر تعبير الارتباط، وتجري استبدالًا، ثم تصل بالخطوة الكبيرة عبر نتيجة الاستبدال:

let x = e1 in e2 ==> v2
  if e1 ==> v1
  and e2{v1/x} ==> v2

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

x =/=>

10.3.5. تنفيذ علاقة الخطوة الكبيرة

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

(** [eval_big e] is the [e ==> v] relation. *)
let rec eval_big (e : expr) : expr = match e with
  | Int _ | Bool _ -> e
  | Var _ -> failwith "Unbound variable"
  | Binop (bop, e1, e2) -> eval_bop bop e1 e2
  | Let (x, e1, e2) -> subst e2 (eval_big e1) x |> eval_big
  | If (e1, e2, e3) -> eval_if e1 e2 e3
(** [eval_bop bop e1 e2] is the [e] such that [e1 bop e2 ==> e]. *)
and eval_bop bop e1 e2 = match bop, eval_big e1, eval_big e2 with
  | Add, Int a, Int b -> Int (a + b)
  | Mult, Int a, Int b -> Int (a * b)
  | Leq, Int a, Int b -> Bool (a <= b)
  | _ -> failwith "Operator and operand type mismatch"
(** [eval_if e1 e2 e3] is the [e] such that [if e1 then e2 else e3 ==> e]. *)
and eval_if e1 e2 e3 = match eval_big e1 with
  | Bool true -> eval_big e2
  | Bool false -> eval_big e3
  | _ -> failwith "Guard of if must have type bool"

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

10.3.6. الاستبدال في SimPL

افترضنا في القسم السابق ترميزًا جديدًا هو e'{e/x}، بمعنى «التعبير e' مع استبدال e بـ x». والحدس أنه في أي موضع يظهر فيه x في e'، ينبغي أن نستبدل x بـ e.

ولنعطِ تعريفًا دقيقًا للاستبدال في SimPL. وهو ليس بالغ الصعوبة في معظمه.

الثوابت لا تظهر فيها متغيرات (فمثلًا لا يمكن أن يوجد x نحويًا في 42)، لذا يتركها الاستبدال دون تغيير:

i{e/x} = i
b{e/x} = b

وبالنسبة إلى العوامل الثنائية وتعبيرات if، كل ما يحتاج الاستبدال إلى فعله هو التعاود داخل التعبيرات الفرعية:

(e1 bop e2){e/x} = e1{e/x} bop e2{e/x}
(if e1 then e2 else e3){e/x} = if e1{e/x} then e2{e/x} else e3{e/x}

أما المتغيرات فتبدأ في أن تصير أدق قليلًا. وثمة احتمالان: إما أن نصادف المتغير x، وهو ما يعني أننا ينبغي أن نجري الاستبدال، وإما أن نصادف متغيرًا آخر باسم مختلف، لنقل y، وفي هذه الحالة ينبغي ألا نجري الاستبدال:

x{e/x} = e
y{e/x} = y

ومن المهم ملاحظة الحالة الأولى من هاتين، x{e/x} = e: فهي موضع إجراء عملية الاستبدال أخيرًا. فمثلًا، لنفترض أننا نحاول معرفة نتيجة (x + 42){1/x}. وباستخدام التعريفات أعلاه،

  (x + 42){1/x}
= x{1/x} + 42{1/x}   by the bop case
= 1 + 42{1/x}        by the first variable case
= 1 + 42             by the integer case

لاحظ أننا لا نعرّف علاقة --> الآن. أي أن أيا من هذه التساويات لا يمثل خطوة تقييم. ولتجسيد ذلك، لنفترض أننا نقيّم let x = 1 in x + 42:

    let x = 1 in x + 42
--> (x + 42){1/x}
  = 1 + 42
--> 43

ثمة خطوتان مفردتان هنا، واحدة لـ let والأخرى لـ +. لكننا نعتبر الاستبدال يحدث دفعة واحدة، كجزء من الخطوة التي تأخذها let. ولهذا نكتب (x + 42){1/x} = 1 + 42، لا (x + 42){1/x} --> 1 + 42.

وأخيرًا، لـتعبيرات let حالتان أيضًا، حسب اسم المتغير المرتبط:

(let x = e1 in e2){e/x}  =  let x = e1{e/x} in e2
(let y = e1 in e2){e/x}  =  let y = e1{e/x} in e2{e/x}

تستبدل الحالتان معًا e بـ x داخل تعبير الارتباط e1. وذلك لضمان تقييم تعبيرات مثل let x = 42 in let y = x in y تقييمًا صحيحًا: إذ يجب أن يكون x في النطاق داخل الارتباط y = x، لذا علينا إجراء استبدال هناك بصرف النظر عن الاسم المرتبط.

لكن الحالة الأولى لا تجري استبدالًا داخل e2، بينما الحالة الثانية تجريه. وذلك لكي نتوقف عن الاستبدال عندما نصل إلى اسم محجوب. تأمل let x = 5 in let x = 6 in x. نعلم أنه سيُقيَّم إلى 6 في OCaml بسبب الحجب. وإليك كيف سيُقيَّم بتعريفات SimPL لدينا:

    let x = 5 in let x = 6 in x
--> (let x = 6 in x){5/x}
  = let x = 6{5/x} in x      ***
  = let x = 6 in x
--> x{6/x}
  = 6

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

    let x = 5 in let x = 6 in x
--> (let x = 6 in x){5/x}
  = let x = 6{5/x} in x{5/x}      ***WRONG***
  = let x = 6 in 5
--> 5{6/x}
  = 5

المثال 1:

let x = 2 in x + 1
--> (x + 1){2/x}
  = 2 + 1
--> 3

المثال 2:

    let x = 0 in (let x = 1 in x)
--> (let x = 1 in x){0/x}
  = (let x = 1{0/x} in x)
  = (let x = 1 in x)
--> x{1/x}
  = 1

المثال 3:

    let x = 0 in x + (let x = 1 in x)
--> (x + (let x = 1 in x)){0/x}
  = x{0/x} + (let x = 1 in x){0/x}
  = 0 + (let x = 1{0/x} in x)
  = 0 + (let x = 1 in x)
--> 0 + x{1/x}
  = 0 + 1
--> 1

10.3.7. تنفيذ الاستبدال

يسهل تحويل التعريفات أعلاه إلى شيفرة OCaml. ولاحظ أنه، رغم أننا نكتب v أدناه، فالدالة قادرة فعلًا على استبدال أي تعبير بمتغير، لا قيمة فقط. لكن المفسّر لن يستدعي هذه الدالة إلا على قيمة.

(** [subst e v x] is [e] with [v] substituted for [x], that
    is, [e{v/x}]. *)
let rec subst e v x = match e with
  | Var y -> if x = y then v else e
  | Bool _ -> e
  | Int _ -> e
  | Binop (bop, e1, e2) -> Binop (bop, subst e1 v x, subst e2 v x)
  | Let (y, e1, e2) ->
    let e1' = subst e1 v x in
    if x = y
    then Let (y, e1', e2)
    else Let (y, e1', subst e2 v x)
  | If (e1, e2, e3) ->
    If (subst e1 v x, subst e2 v x, subst e3 v x)

10.3.8. اكتمل مفسّر SimPL

أكملنا تطوير مفسّر SimPL. تذكّر أنه يمكن تنزيل المفسّر المكتمل هنا: simpl.zip. وهو يتضمن بعض حالات الاختبار البدائية، وكذلك أهداف makefile ستجدها مفيدة.

10.3.9. الاستبدال المانع للالتقاط

كان تعريف الاستبدال في SimPL دقيقًا قليلًا لكنه ليس معقدًا كثيرًا. غير أنه يتبين أن التعريف يصير أعقد عمومًا.

لننظر في هذه اللغة الصغيرة:

e ::= x | e1 e2 | fun x -> e
v ::= fun x -> e
x ::= <identifiers>

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

وثمة طرق عدة لتعريف دلالات تقييم لحساب لامبدا. ولعل أبسط طريقة—وهي الأقرب إلى OCaml أيضًا—تستخدم القاعدة التالية:

e1 e2 ==> v
  if e1 ==> fun x -> e
  and e2 ==> v2
  and e{v2/x} ==> v

هذه القاعدة هي القاعدة الوحيدة التي نحتاجها: فلا تلزم أي قواعد أخرى. وتُعرف هذه القاعدة أيضًا بدلالات النداء بالقيمة (call by value)، لأنها تشترط اختزال الوسائط إلى قيم قبل تطبيق الدالة. وإن بدا ذلك واضحًا، فذلك لأنك اعتدته من OCaml.

لكن دلالات أخرى ممكنة بالتأكيد. فمثلًا، تستخدم Haskell صيغة تُسمى النداء بالاسم (call by name)، بقاعدة واحدة:

e1 e2 ==> v
  if e1 ==> fun x -> e
  and e{e2/x} ==> v

وفي النداء بالاسم، لا يلزم اختزال e2 إلى قيمة؛ وقد يؤدي ذلك إلى كفاءة أكبر إذا لم تكن هناك حاجة إلى قيمة e2 أبدًا.

والآن نحتاج إلى تعريف عملية الاستبدال لحساب لامبدا. ونريد تعريفًا يعمل مع النداء بالاسم أو النداء بالقيمة معًا. ومستلهمين تعريفنا لـ SimPL، إليك بداية تعريف:

x{e/x} = e
y{e/x} = y
(e1 e2){e/x} = e1{e/x} e2{e/x}

السطران الأولان هما بالضبط كيفية تعريفنا استبدال المتغيرات في SimPL. أما السطر التالي فيشبه كيفية تعريفنا استبدال العوامل الثنائية؛ فنحن نتعاود داخل التعبيرات الفرعية فحسب.

وماذا عن الاستبدال داخل دالة؟ في SimPL توقفنا عن الاستبدال عندما وصلنا إلى متغير مرتبط بالاسم نفسه؛ وإلا واصلنا. وفي حساب لامبدا تُصاغ تلك الفكرة كما يلي:

(fun x -> e'){e/x} = fun x -> e'
(fun y -> e'){e/x} = fun y -> e'{e/x}

لعلها مفاجأة أن ذلك التعريف غير صحيح. والسبب: أنه يخالف مبدأ عدم اكتراث الأسماء (Principle of Name Irrelevance). لنفترض أننا نحاول هذا الاستبدال:

(fun z -> x){z/x}

ستكون النتيجة:

  fun z -> x{z/x}
= fun z -> z

وإذا بدالة لم تكن دالة الهوية تصير فجأة دالة الهوية. بينما لو حاولنا هذا الاستبدال:

(fun y -> x){z/x}

ستكون النتيجة:

  fun y -> x{z/x}
= fun y -> z

وهي ليست دالة الهوية. فتعريفنا للاستبدال داخل الدوال المجهولة غير صحيح، لأنه يلتقط (captures) المتغيرات. فقد يُلتقط اسم متغير يُستبدل داخل دالة مجهولة بالخطأ باسم وسيطة الدالة.

لاحظ أننا لم نواجه هذه المشكلة قط في SimPL، جزئيًا لأنها كانت مصنّفة الأنواع. فالدالة fun y -> z إذا طُبّقت على أي وسيطة فلن تعيد إلا z، وهو متغير غير مرتبط. لكن حساب لامبدا غير مصنّف الأنواع، فلا يمكننا الاعتماد على الأنواع هنا لاستبعاد ذلك الاحتمال.

فيصير السؤال: كيف نعرّف الاستبدال بحيث يعطي الجواب الصحيح دون التقاط المتغيرات؟ ويُسمى الجواب الاستبدال المانع للالتقاط (capture-avoiding substitution)، وقد أفلت تعريفه الصحيح من الرياضيين قرونًا.

والتعريف الصحيح كما يلي:

(fun x -> e'){e/x} = fun x -> e'
(fun y -> e'){e/x} = fun y -> e'{e/x}  if y is not in FV(e)

حيث FV(e) تعني «المتغيرات الحرة (free variables)» في e، أي المتغيرات غير المرتبطة فيه، وهي معرَّفة كما يلي:

FV(x) = {x}
FV(e1 e2) = FV(e1) + FV(e2)
FV(fun x -> e) = FV(e) - {x}

و+ تعني اتحاد المجموعات، و- تعني فرق المجموعات.

ويمنع ذلك التعريف حدوث الاستبدال (fun z -> x){z/x}، لأن z في FV(z).

وللأسف، بسبب الشرط الجانبي y is not in FV(e)، صارت عملية الاستبدال جزئية الآن: فهناك أوقات، مثل المثال الذي قدمناه للتو، لا يمكن تطبيقها فيها.

ويمكن حل تلك المشكلة بتغيير أسماء المتغيرات: فإذا اكتشفنا أننا واجهنا حالة جزئية، أمكننا تغيير اسم وسيطة الدالة. فمثلًا، عند مصادفة (fun z -> x){z/x}، يمكن استبدال وسيطة الدالة باسم جديد w لا يظهر في أي موضع آخر، فنحصل على (fun w -> x){z/x}. (وإذا ظهر z في أي موضع من الجسم، فسيُستبدل بـ w أيضًا.) وهذا إحلال (replacement)، لا استبدال: ففي كل موضع نرى فيه z على الإطلاق، نستبدله بـ w. ثم يمكن للاستبدال أن يمضي ويعطي fun w -> z على نحو صحيح.

والجزء الدقيق في ذلك هو كيفية اختيار اسم جديد لا يظهر في أي موضع آخر، أي كيفية اختيار اسم طازج (fresh). وإليك ثلاث استراتيجيات:

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

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

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

let gensym =
  let counter = ref 0 in
  fun () -> incr counter; "$x" ^ string_of_int !counter

والاسم gensym تقليدي لهذا النوع من الدوال. وهو يأتي من LISP، ويظهر في جميع تنفيذات المصرّفات. ويعني توليد رمز طازج.

وهناك تنفيذ كامل لمفسّر حساب لامبدا، بما في ذلك الاستبدال المانع للالتقاط، يمكنك تنزيله: lambda-subst.zip. ويستخدم استراتيجية gensym أعلاه لتوليد أسماء طازجة. وفيه تعريف باسم strategy في main.ml يمكنك استخدامه للتنقل بين النداء بالقيمة والنداء بالاسم.

10.3.10. نواة OCaml

ولنرتقي الآن من SimPL وحساب لامبدا إلى لغة أكبر نسميها Core OCaml. وإليك صياغتها في BNF:

e ::= x | e1 e2 | fun x -> e
    | i | b | e1 bop e2
    | (e1, e2) | fst e | snd e
    | Left e | Right e
    | match e with Left x1 -> e1 | Right x2 -> e2
    | if e1 then e2 else e3
    | let x = e1 in e2

bop ::= + | - | * | <=

x ::= <identifiers>

i ::= <integers>

b ::= true | false

v ::= fun x -> e | i | b | (v1, v2) | Left v | Right v

العوامل الثنائية التي حددناها في bop مقصود بها أن تكون تمثيلية لا شاملة. ويمكننا إضافة < و= وغيرهما.

ولإبقاء الأزواج بسيطة في هذا النموذج النووي، نمثلها بمكوّنين اثنين فقط (أي أنها أزواج). ويمكن برمجة زوج أطول بأزواج متداخلة. فمثلًا، يمكن أن يكون (1, 2, 3) في OCaml هو (1, (2, 3)) في هذه اللغة النووية.

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

وثمة بعض البنى المهمة في OCaml محذوفة من هذه اللغة النووية، منها الدوال التعاودية والاستثناءات والقابلية للتغيير والوحدات. والأنواع مفقودة أيضًا؛ فـ Core OCaml ليس فيها أي فحص للأنواع. ومع ذلك، فيها ما يكفي لإبقائنا مستمتعين.

10.3.11. تقييم Core OCaml في نموذج الاستبدال

لنعرّف علاقتي الخطوة الصغيرة والخطوة الكبيرة لـ Core OCaml. ولنكن صادقين: لن يكون هناك كثير مما يفاجئ في هذه المرحلة؛ فقد رأينا كل شيء تقريبًا في SimPL وفي حساب لامبدا.

علاقة الخطوة الصغيرة. إليك جزء Core OCaml الذي نعرفه بالفعل من SimPL:

e1 bop e2 --> e1' bop e2
	if e1 --> e1'

v1 bop e2 --> v1 bop e2'
	if e2 --> e2'

v1 bop v2 --> v3
	where v3 is the result of applying primitive operation bop
	to v1 and v2

if e1 then e2 else e3 --> if e1' then e2 else e3
	if e1 --> e1'

if true then e2 else e3 --> e2

if false then e2 else e3 --> e3

let x = e1 in e2 --> let x = e1' in e2
	if e1 --> e1'

let x = v in e2 --> e2{v/x}

وإليك جزء Core OCaml الذي يقابل حساب لامبدا:

e1 e2 --> e1' e2
	if e1 --> e1'

v1 e2 --> v1 e2'
	if e2 --> e2'

(fun x -> e) v2 --> e{v2/x}

وإليك الأجزاء الجديدة في Core OCaml. أولًا، تقيّم الأزواج مكوّنها الأول، ثم مكوّنها الثاني:

(e1, e2) --> (e1', e2)
	if e1 --> e1'

(v1, e2) --> (v1, e2')
	if e2 --> e2'

fst e --> fst e'
  if e --> e'

snd e --> snd e'
  if e --> e'

fst (v1, v2) --> v1

snd (v1, v2) --> v2

وتقيّم المنشئات التعبير الذي تحمله:

Left e --> Left e'
	if e --> e'

Right e --> Right e'
	if e --> e'

وتقيّم مطابقة الأنماط التعبير المُطابَق عليه، ثم تختزل إلى أحد الفرعين:

match e with Left x1 -> e1 | Right x2 -> e2
--> match e' with Left x1 -> e1 | Right x2 -> e2
	if e --> e'

match Left v with Left x1 -> e1 | Right x2 -> e2
--> e1{v/x1}

match Right v with Left x1 -> e1 | Right x2 -> e2
--> e2{v/x2}

الاستبدال. نحتاج أيضًا إلى تعريف عملية الاستبدال لـ Core OCaml. وإليك ما نعرفه بالفعل من SimPL وحساب لامبدا:

i{v/x} = i

b{v/x} = b

(e1 bop e2) {v/x} = e1{v/x} bop e2{v/x}

(if e1 then e2 else e3){v/x}
 = if e1{v/x} then e2{v/x} else e3{v/x}

(let x = e1 in e2){v/x} = let x = e1{v/x} in e2

(let y = e1 in e2){v/x} = let y = e1{v/x} in e2{v/x}
  if y not in FV(v)

x{v/x} = v

y{v/x} = y

(e1 e2){v/x} = e1{v/x} e2{v/x}

(fun x -> e'){v/x} = (fun x -> e')

(fun y -> e'){v/x} = (fun y -> e'{v/x})
  if y not in FV(v)

لاحظ أننا أضفنا الآن شرط الاستبدال المانع للالتقاط إلى تعريفَي let وfun: فكلاهما يشترط ألا يكون y في المتغيرات الحرة لـ v. ولذا نحتاج إلى تعريف المتغيرات الحرة لتعبير:

FV(x) = {x}
FV(e1 e2) = FV(e1) + FV(e2)
FV(fun x -> e) = FV(e) - {x}
FV(i) = {}
FV(b) = {}
FV(e1 bop e2) = FV(e1) + FV(e2)
FV((e1,e2)) = FV(e1) + FV(e2)
FV(fst e1) = FV(e1)
FV(snd e2) = FV(e2)
FV(Left e) = FV(e)
FV(Right e) = FV(e)
FV(match e with Left x1 -> e1 | Right x2 -> e2)
 = FV(e) + (FV(e1) - {x1}) + (FV(e2) - {x2})
FV(if e1 then e2 else e3) = FV(e1) + FV(e2) + FV(e3)
FV(let x = e1 in e2) = FV(e1) + (FV(e2) - {x})

وأخيرًا، نعرّف الاستبدال للأشكال النحوية الجديدة في Core OCaml. والتعبيرات التي لا تربط متغيرات يسهل التعامل معها:

(e1,e2){v/x} = (e1{v/x}, e2{v/x})

(fst e){v/x} = fst (e{v/x})

(snd e){v/x} = snd (e{v/x})

(Left e){v/x} = Left (e{v/x})

(Right e){v/x} = Right (e{v/x})

وتتطلب تعبيرات match عملًا أكثر قليلًا، مثل تعبيرات let والدوال المجهولة، للتأكد من صحة منع الالتقاط:

(match e with Left x1 -> e1 | Right x2 -> e2){v/x}
 = match e{v/x} with Left x1 -> e1{v/x} | Right x2 -> e2{v/x}
     if ({x1,x2} intersect FV(v)) = {}

(match e with Left x -> e1 | Right x2 -> e2){v/x}
 = match e{v/x} with Left x -> e1 | Right x2 -> e2{v/x}
     if ({x2} intersect FV(v)) = {}

(match e with Left x1 -> e1 | Right x -> e2){v/x}
 = match e{v/x} with Left x1 -> e1{v/x} | Right x -> e2
      if ({x1} intersect FV(v)) = {}

(match e with Left x -> e1 | Right x -> e2){v/x}
 = match e{v/x} with Left x -> e1 | Right x -> e2

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

10.3.12. علاقة الخطوة الكبيرة

في هذه المرحلة لم تبقَ أي مفاهيم جديدة علينا تقديمها. يمكننا ببساطة أن نعطي القواعد:

e1 e2 ==> v
  if e1 ==> fun x -> e
  and e2 ==> v2
  and e{v2/x} ==> v
fun x -> e ==> fun x -> e
i ==> i
b ==> b
e1 bop e2 ==> v
  if e1 ==> v1
  and e2 ==> v2
  and v is the result of primitive operation v1 bop v2
(e1, e2) ==> (v1, v2)
  if e1 ==> v1
  and e2 ==> v2
fst e ==> v1
  if e ==> (v1, v2)
snd e ==> v2
  if e ==> (v1, v2)
Left e ==> Left v
  if e ==> v
Right e ==> Right v
  if e ==> v
match e with Left x1 -> e1 | Right x2 -> e2 ==> v
  if e ==> Left v1
  and e1{v1/x1} ==> v
match e with Left x1 -> e1 | Right x2 -> e2 ==> v
  if e ==> Right v2
  and e2{v2/x2} ==> v
if e1 then e2 else e3 ==> v
  if e1 ==> true
  and e2 ==> v
if e1 then e2 else e3 ==> v
  if e1 ==> false
  and e3 ==> v
let x = e1 in e2 ==> v
  if e1 ==> v1
  and e2{v1/x} ==> v

10.4. نموذج البيئة

كنا حتى الآن نستخدم نموذج الاستبدال لتقييم البرامج. وهو نموذج ذهني رائع للتقييم، ويُستخدم كثيرًا في نظرية لغات البرمجة.

لكنه ليس الخيار الأفضل عند التنفيذ. فهو متلهف أكثر مما ينبغي: إذ يستبدل كل ورود لمتغير، حتى لو لم تكن هناك حاجة إلى ذلك الورود أبدًا. فمثلًا، سيتطلب let x = 42 in e الزحف على كل e، وقد يكون تعبيرًا كبيرًا جدًا، حتى لو لم يظهر x في e أبدًا، أو حتى لو ظهر x فقط داخل فرع من تعبير if لا يُقيَّم أبدًا.

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

ولأخذ البيئة في الحساب، تحتاج علاقة التقييم إلى التغير. فبدلًا من e --> e' أو e ==> v، وكلتاهما علاقة ثنائية، نحتاج الآن إلى علاقة ثلاثية، هي إما

• --> e'، أو
• ==> v،

حيث تشير env إلى البيئة، وتُسمى `` تهيئة الآلة (machine configuration). وتمثل تلك التهيئة حالة الحاسوب وهو يقيّم برنامجًا: فـ env تمثل جزءًا من ذاكرة الحاسوب (ارتباط المتغيرات بالقيم)، وe يمثل البرنامج.

وكتدوين، لنكن:

• {} يمثل البيئة الفارغة،
• {x1:v1, x2:v2, ...} يمثل البيئة التي تربط x1 بـ v1، وهكذا،
• env[x -> v] يمثل البيئة env مع ربط المتغير x إضافةً بالقيمة v، و
• env(x) يمثل ارتباط x في env.

ولو أردنا ترميزًا رياضيًا أكثر لكتبنا $\mapsto$ بدلًا من -> في env[x -> v]، لكننا نستهدف ترميزًا يسهل كتابته على لوحة مفاتيح قياسية.

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

10.4.1. تقييم حساب لامبدا في نموذج البيئة

تذكّر أن حساب لامبدا هو الجزء من لغة وظيفية المتعلق بالدوال والتطبيق:

e ::= x | e1 e2 | fun x -> e

v ::= fun x -> e

ولنستكشف كيفية تعريف علاقة تقييم بالخطوة الكبيرة لحساب لامبدا في نموذج البيئة. والقاعدة الخاصة بالمتغيرات تقول ببساطة بالبحث عن اسم المتغير في البيئة:

<env, x> ==> env(x)

وتقول هذه القاعدة الخاصة بالدوال إن الدالة المجهولة تُقيَّم إلى نفسها فحسب. فالدوال قيم بعد كل شيء:

<env, fun x -> e> ==> fun x -> e

وأخيرًا، تقول هذه القاعدة الخاصة بالتطبيق بتقييم الطرف الأيسر e1 إلى دالة fun x -> e، والطرف الأيمن إلى قيمة v2، ثم تقييم جسم الدالة e في بيئة ممتدة تربط وسيطة الدالة x بـ v2:

<env, e1 e2> ==> v
  if <env, e1> ==> fun x -> e
  and <env, e2> ==> v2
  and <env[x -> v2], e> ==> v

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

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

<env, i> ==> i

وأما تعبيرات let، فتذكّر أننا لا نحتاج إليها فعلًا، لأن let x = e1 in e2 يمكن إعادة كتابته كـ (fun x -> e2) e1. ومع ذلك، ستكون دلالاتها:

<env, let x = e1 in e2> ==> v
  if <env, e1> ==> v1
  and <env[x -> v1], e2> ==> v

وهي قاعدة تتبع في الحقيقة من القواعد الأخرى أعلاه فحسب، باستخدام إعادة الكتابة تلك.

فإلى ماذا سيُقيَّم هذا التعبير؟

let x = 1 in
let f = fun y -> x in
let x = 2 in
f 0

وفق دلالاتنا حتى الآن، سيُقيَّم كما يلي:

سينتج let x = 1 البيئة {x:1}.

وسينتج let f = fun y -> x البيئة {x:1, f:(fun y -> x)}.

وسينتج let x = 2 البيئة {x:2, f:(fun y -> x)}. لاحظ كيف يحجب الارتباط الجديد ارتباط x بـ 1.

والآن سنقيّم x)}, f 0>:

<{x:2, f:(fun y -> x)}, f 0> ==> 2
  because <{x:2, f:(fun y -> x)}, f> ==> fun y -> x
  and <{x:2, f:(fun y -> x)}, 0> ==> 0
  and <{x:2, f:(fun y -> x)}[y -> 0], x> ==> 2
    because <{x:2, f:(fun y -> x), y:0}, x> ==> 2

فالنتيجة إذن 2.

لكن وفق utop (ونموذج الاستبدال)، يُقيَّم كما يلي:

# let x = 1 in
  let f = fun y -> x in
  let x = 2 in
  f 0;;
- : int = 1

والنتيجة إذن 1. ومن الواضح أن 1 و2 جوابان مختلفان!

فماذا سار على غير ما يرام؟؟ الأمر يتعلق بالنطاق.

10.4.2. النطاق المعجمي مقابل النطاق الديناميكي

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

• وفق قاعدة النطاق الديناميكي (dynamic scope)، يُقيَّم جسم الدالة في البيئة الديناميكية الحالية وقت تطبيق الدالة، لا في البيئة الديناميكية القديمة التي كانت موجودة وقت تعريف الدالة.
• ووفق قاعدة النطاق المعجمي (lexical scope)، يُقيَّم جسم الدالة في البيئة الديناميكية القديمة التي كانت موجودة وقت تعريف الدالة، لا في البيئة الحالية وقت تطبيق الدالة.

وقاعدة النطاق الديناميكي هي ما نفّذته دلالاتنا أعلاه. ولنعد إلى دلالات تطبيق الدوال:

<env, e1 e2> ==> v
  if <env, e1> ==> fun x -> e
  and <env, e2> ==> v2
  and <env[x -> v2], e> ==> v

لاحظ كيف يُقيَّم الجسم e في البيئة env نفسها التي كانت عند تطبيق الدالة. وفي البرنامج المثال

let x = 1 in
let f = fun y -> x in
let x = 2 in
f 0

فذلك يعني أن f تُقيَّم في بيئة يكون فيها x مرتبطًا بـ 2، لأن ذلك أحدث ارتباط لـ x.

لكن OCaml تنفّذ قاعدة النطاق المعجمي، التي تتوافق مع نموذج الاستبدال. وبهذه القاعدة يكون x مرتبطًا بـ 1 في جسم f عند تعريف f، ولا يغيّر الارتباط اللاحق لـ x بـ 2 تلك الحقيقة.

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

ومع ذلك، النطاق الديناميكي مفيد في بعض الحالات. فبعض اللغات تستخدمه كالقاعدة (مثل Emacs LISP وLaTeX)، وبعض اللغات لها طرق خاصة لفعله (مثل Perl وRacket). لكن معظم اللغات اليوم لا تملكه ببساطة.

وثمة ميزة لغوية واحدة تمتلكها اللغات الحديثة وتشبه النطاق الديناميكي، وهي الاستثناءات. فمعالجة الاستثناءات تشبه النطاق الديناميكي، من حيث أن رفع استثناء ينقل التحكم إلى «أحدث» مُعالِج استثناء، تمامًا كما يستخدم النطاق الديناميكي «أحدث» ارتباط للمتغير.

10.4.3. محاولة ثانية لتقييم حساب لامبدا في نموذج البيئة

فيصير السؤال: كيف ننفّذ النطاق المعجمي؟ يبدو أنه يتطلب السفر في الزمن، لأن أجسام الدوال يجب أن تُقيَّم في بيئات ديناميكية قديمة اختفت منذ زمن طويل.

والجواب أن تنفيذ اللغة يجب أن يرتب الاحتفاظ بالبيئات القديمة. وذلك فعلًا ما يجب أن تفعله OCaml وغيرها من اللغات. وهي تستخدم بنية بيانات تُسمى إغلاقًا (closure) لهذا الغرض.

وللإغلاق جزءان:

• جزء الشيفرة (code)، ويحتوي دالة fun x -> e، و
• جزء البيئة (environment)، ويحتوي البيئة env وقت تعريف تلك الدالة.

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

ولنرمز للإغلاق بـ (| fun x -> e, env |). والفاصلتان (| ... |) مقصود بهما استحضار زوج OCaml، لكنهما بالطبع ليستا صياغة OCaml مشروعة.

وباستخدام ذلك الترميز، يمكننا إعادة تعريف علاقة التقييم كما يلي:

تقول قاعدة الدوال الآن إن الدالة المجهولة تُقيَّم إلى إغلاق:

<env, fun x -> e> ==> (| fun x -> e, env |)

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

وتقول قاعدة التطبيق باستخدام ذلك الإغلاق:

<env, e1 e2> ==> v
  if <env, e1> ==> (| fun x -> e, defenv |)
  and <env, e2> ==> v2
  and <defenv[x -> v2], e> ==> v

تستخدم تلك القاعدة بيئة الإغلاق defenv (واسمها مقصود به الإيحاء بـ«بيئة التعريف») لتقييم جسم الدالة e.

وتبقى القاعدة المشتقة لتعبيرات let دون تغيير:

<env, let x = e1 in e2> ==> v
  if <env, e1> ==> v1
  and <env[x -> v1], e2> ==> v

وذلك لأن بيئة تعريف الجسم e2 هي البيئة الحالية env نفسها عند تقييم تعبير let.

10.4.4. تنفيذ حساب لامبدا في نموذج البيئة

يمكنك تنزيل تنفيذ كامل لدلالات حساب لامبدا المذكورتين أعلاه: lambda-env.zip. وفي main.ml تعريف باسم scope يمكنك استخدامه للتنقل بين النطاق المعجمي والديناميكي.

10.4.5. تقييم Core OCaml في نموذج البيئة

لا جديد في دلالات نموذج البيئة (بالخطوة الكبيرة) لـ Core OCaml، بعد أن صرنا نعرف الإغلاقات، لكن لأجل الكمال لنصغها على أي حال.

الصياغة.

e ::= x | e1 e2 | fun x -> e
    | i | b | e1 bop e2
    | (e1,e2) | fst e1 | snd e2
    | Left e | Right e
    | match e with Left x1 -> e1 | Right x2 -> e2
    | if e1 then e2 else e3
    | let x = e1 in e2

الدلالات.

رأينا بالفعل دلالات جزء حساب لامبدا من Core OCaml:

<env, x> ==> v
  if env(x) = v

<env, e1 e2> ==> v
  if  <env, e1> ==> (| fun x -> e, defenv |)
  and <env, e2> ==> v2
  and <defenv[x -> v2], e> ==> v

<env, fun x -> e> ==> (|fun x -> e, env|)

ويتجاهل تقييم الثوابت البيئة:

<env, i> ==> i

<env, b> ==> b

ويستخدم تقييم معظم الميزات اللغوية الأخرى البيئة دون تغييرها فحسب:

<env, e1 bop e2> ==> v
  if  <env, e1> ==> v1
  and <env, e2> ==> v2
  and v is the result of applying the primitive operation bop to v1 and v2

<env, (e1, e2)> ==> (v1, v2)
  if  <env, e1> ==> v1
  and <env, e2> ==> v2

<env, fst e> ==> v1
  if <env, e> ==> (v1, v2)

<env, snd e> ==> v2
  if <env, e> ==> (v1, v2)

<env, Left e> ==> Left v
  if <env, e> ==> v

<env, Right e> ==> Right v
  if <env, e> ==> v

<env, if e1 then e2 else e3> ==> v2
  if <env, e1> ==> true
  and <env, e2> ==> v2

<env, if e1 then e2 else e3> ==> v3
  if <env, e1> ==> false
  and <env, e3> ==> v3

وأخيرًا، يمدّ تقييم بنى الارتباط (أي تعبيري match وlet) البيئة بارتباط جديد:

<env, match e with Left x1 -> e1 | Right x2 -> e2> ==> v1
  if  <env, e> ==> Left v
  and <env[x1 -> v], e1> ==> v1

<env, match e with Left x1 -> e1 | Right x2 -> e2> ==> v2
  if  <env, e> ==> Right v
  and <env[x2 -> v], e2> ==> v2

<env, let x = e1 in e2> ==> v2
  if  <env, e1> ==> v1
  and <env[x -> v1], e2> ==> v2

10.5. فحص الأنواع

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

نظام الأنواع (type system) وصف رياضي لكيفية تحديد ما إذا كان التعبير سيئ الأنواع أم جيد الأنواع، وفي الحالة الأخيرة ما نوع التعبير. وفاحص الأنواع (type checker) برنامج ينفّذ نظام أنواع، أي ينفّذ الدلالات الساكنة للغة.

وتُصاغ أنظمة الأنواع عادةً كعلاقة ثلاثية $\mathit{HasType}(\Gamma, e, t)$، بمعنى أن التعبير $e$ نوعه $t$ في البيئة الساكنة $\Gamma$. والبيئة الساكنة (static environment)، أو سياق الأنواع (typing context)، تطبيق من المعرّفات إلى الأنواع. وتُستخدم البيئة الساكنة لتسجيل المتغيرات التي في النطاق وأنواعها. واستخدام الحرف اليوناني $\Gamma$ للبيئات الساكنة أمر تقليدي.

غير أن تلك العلاقة الثلاثية $\mathit{HasType}$ تُكتب عادةً بترميز بيني بالشكل $\Gamma \vdash e : t$. ويمكنك قراءة رمز البوابة $\vdash$ على أنه «يبرهن» أو «يبين»، أي أن البيئة الساكنة $\Gamma$ تبين أن $e$ نوعه $t$.

ولنجعل ذلك الترميز أوْد شيئًا بإزالة اليونانية والتنضيد الرياضي. سنكتب ببساطة env |- e : t لنعني أن البيئة الساكنة env تبين أن e نوعه t. وقد استخدمنا env سابقًا لنعني بيئة ديناميكية في علاقة الخطوة الكبيرة ==>. وبما أنه يمكن دائمًا رؤية ما إذا كنا نستخدم علاقة ==> أو |-، فمعنى env كبيئة ديناميكية أو ساكنة قابل للتمييز دائمًا.

ولنكتب {} للبيئة الساكنة الفارغة، وx:t لنعني أن x مرتبط بـ t. فمثلًا، ستكون {foo:int, bar:bool} هي البيئة الساكنة التي فيها foo نوعه int وbar نوعه bool. ويجوز للبيئة الساكنة أن تربط معرّفًا مرة واحدة على الأكثر. وسنكتب env[x -> t] لنعني بيئة ساكنة تحتوي جميع ارتباطات env، وتربط x بـ t أيضًا. وإذا كان x مرتبطًا بالفعل في env، يُستبدل ذلك الارتباط القديم بالارتباط الجديد بـ t في env[x -> t]. وكما في البيئات الديناميكية، لو أردنا ترميزًا رياضيًا أكثر لكتبنا $\mapsto$ بدلًا من -> في env[x -> v]، لكننا نستهدف ترميزًا يسهل كتابته على لوحة مفاتيح قياسية.

وبهذه الآلة كلها يمكننا أخيرًا تعريف معنى أن يكون التعبير جيد الأنواع: يكون التعبير e جيد الأنواع (well-typed) في البيئة الساكنة env إذا وُجد نوع t بحيث env |- e : t. فهدف فاحص الأنواع إذن إيجاد ذلك النوع t، انطلاقًا من بيئة ساكنة أولية ما.

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

10.5.1. نظام أنواع لـ SimPL

تذكّر صياغة SimPL:

e ::= x | i | b | e1 bop e2
    | if e1 then e2 else e3
    | let x = e1 in e2

bop ::= + | * | <=

ولنعرّف نظام أنواع env |- e : t لـ SimPL. والأنواع الوحيدة في SimPL هي الأعداد الصحيحة والقيم المنطقية:

t ::= int | bool

ولتعريف |- سنخترع مجموعة من قواعد الأنواع (typing rules) تحدد نوع التعبير بناءً على أنواع تعبيراته الفرعية. وبعبارة أخرى، |- علاقة معرَّفة استقرائيًا، كما يمكن التعلم في مقرر الرياضيات المتقطعة. فلديها إذن بعض الحالات الأساسية وبعض الحالات الاستقرائية.

وفي الحالات الأساسية، نوع الثابت الصحيح int في أي بيئة ساكنة كانت، وكذلك الثابت المنطقي نوعه دائمًا bool، والمتغير نوعه ما تقول البيئة الساكنة إنه ينبغي أن يكون. وإليك قواعد الأنواع التي تعبّر عن تلك الأفكار:

env |- i : int
env |- b : bool
{x : t, ...} |- x : t

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

Let. كما نعرف بالفعل من OCaml، نفحص أنواع جسم تعبير let باستخدام نطاق ممتد بارتباط جديد.

env |- let x = e1 in e2 : t2
  if env |- e1 : t1
  and env[x -> t1] |- e2 : t2

تقول القاعدة إن let x = e1 in e2 نوعه t2 في البيئة الساكنة env، لكن فقط إذا صحت شروط معينة. الشرط الأول أن يكون نوع e1 هو t1 في env. والثاني أن يكون نوع e2 هو t2 في بيئة ساكنة جديدة، هي env ممتدة لتربط x بـ t1.

العوامل الثنائية. سنحتاج إلى قاعدتين مختلفتين للعوامل الثنائية.

env |- e1 bop e2 : int
  if bop is + or *
  and env |- e1 : int
  and env |- e2 : int

env |- e1 <= e2 : bool
  if env |- e1 : int
  and env |- e2 : int

If. كما في OCaml، يجب أن يكون لتعير if شرط منطقي، ويجب أن يكون لفرعيه النوع نفسه.

env |- if e1 then e2 else e3 : t
  if env |- e1 : bool
  and env |- e2 : t
  and env |- e3 : t

10.5.2. فاحص أنواع لـ SimPL

لننفّذ فاحص أنواع لـ SimPL، بناءً على نظام الأنواع الذي عرّفناه في القسم السابق. ويمكنك تنزيل فاحص الأنواع المكتمل كجزء من مفسّر SimPL: simpl.zip

نحتاج إلى نوع متغاير لتمثيل الأنواع:

type typ =
  | TInt
  | TBool

كان الاسم الطبيعي لذلك النوع المتغاير سيكون «type» لا «typ» بالطبع، لكن الأول كلمة مفتاحية في OCaml بالفعل. وعلينا تسبيق المنشئات بـ«T» لتمييزها عن منشئات نوع expr، التي تشمل Int وBool.

ولنستحدث توقيعًا صغيرًا للبيئات الساكنة، بناءً على التجريدات التي قدمناها حتى الآن: البيئة الساكنة الفارغة، والبحث عن متغير، وتمديد بيئة ساكنة.

module type StaticEnvironment = sig
  (** [t] is the type of a static environment. *)
  type t
  (** [empty] is the empty static environment. *)
  val empty : t
  (** [lookup env x] gets the binding of [x] in [env].
      Raises: [Failure] if [x] is not bound in [env]. *)
  val lookup : t -> string -> typ
  (** [extend env x ty] is [env] extended with a binding
      of [x] to [ty]. *)
  val extend : t -> string -> typ -> t
end

ويسهل تنفيذ ذلك التوقيع بقائمة ترابطية.

module StaticEnvironment : StaticEnvironment = struct
  type t = (string * typ) list
  let empty = []
  let lookup env x =
    try List.assoc x env
    with Not_found -> failwith "Unbound variable"
  let extend env x ty =
    (x, ty) :: env
end

والآن يمكننا تنفيذ علاقة الأنواع |-. وسنفعل ذلك بكتابة دالة typeof : StaticEnvironment.t -> expr -> typ، بحيث typeof env e = t إذا وفقط إذا env |- e : t. لاحظ أن دالة typeof تنتج النوع كمخرج، فهي تستنتج النوع فعليًا! وهذا الاستنتاج سهل في SimPL؛ وسيكون أعقد بكثير في لغات أكبر.

ولنبدأ بالحالات الأساسية:

open StaticEnvironment
(** [typeof env e] is the type of [e] in static environment [env].
    Raises: [Failure] if [e] is not well-typed in [env]. *)
let rec typeof env = function
  | Int _ -> TInt
  | Bool _ -> TBool
  | Var x -> lookup env x
  ...

لاحظ كيف يستند تنفيذ typeof حتى الآن إلى القواعد التي عرّفناها سابقًا لـ |-. وبوجه خاص:

• typeof دالة تعاودية، كما أن |- علاقة استقرائية.
• والحالات الأساسية للتعاود في typeof هي نفسها الحالات الأساسية لـ |-.

ولاحظ أيضًا كيف يختلف تنفيذ typeof عن تعريف |- اختلافًا كبيرًا في نقطة واحدة: معالجة الأخطاء. فنظام الأنواع لم يقل ما نفعل بالأخطاء؛ بل عرّف فحسب معنى أن يكون التعبير جيد الأنواع. أما فاحص الأنواع فيحتاج إلى التصرف والإبلاغ عن البرامج سيئة الأنواع. وتفعل دالتنا typeof ذلك برفع استثناءات. ودالة lookup بوجه خاص سترفع استثناءً إذا حاولنا البحث عن متغير غير مرتبط في البيئة الساكنة.

ولنواصل الحالات التعاودية:

  ...
  | Let (x, e1, e2) -> typeof_let env x e1 e2
  | Binop (bop, e1, e2) -> typeof_bop env bop e1 e2
  | If (e1, e2, e3) -> typeof_if env e1 e2 e3

نستخلص دالة مساعدة لكل فرع لأجل إبقاء مطابقة الأنماط قابلة للقراءة. وتضمّن كل دالة مساعدة أفكار قواعد |- مباشرةً، مع إضافة معالجة الأخطاء.

and typeof_let env x e1 e2 =
  let t1 = typeof env e1 in
  let env' = extend env x t1 in
  typeof env' e2
and typeof_bop env bop e1 e2 =
  let t1, t2 = typeof env e1, typeof env e2 in
  match bop, t1, t2 with
  | Add, TInt, TInt
  | Mult, TInt, TInt -> TInt
  | Leq, TInt, TInt -> TBool
  | _ -> failwith "Operator and operand type mismatch"
and typeof_if env e1 e2 e3 =
  if typeof env e1 = TBool
  then begin
    let t2 = typeof env e2 in
    if t2 = typeof env e3 then t2
    else failwith "Branches of if must have same type"
  end
  else failwith "Guard of if must have type bool"

لاحظ كيف تقع الاستدعاءات التعاودية في تنفيذ typeof في المواضع نفسها بالضبط التي يكون فيها تعريف |- استقرائيًا.

وأخيرًا، يمكننا تنفيذ دالة للتحقق مما إذا كان تعبير جيد الأنواع:

(** [typecheck e] checks whether [e] is well-typed in
    the empty static environment. Raises: [Failure] if not. *)
let typecheck e =
  ignore (typeof empty e)

10.5.3. أمان الأنواع

ما الغرض من نظام الأنواع؟ قد تكون له أغراض كثيرة، لكن أحد الأغراض الأساسية ضمان عدم وقوع أخطاء معينة في وقت التشغيل. والآن بعد أن عرفنا كيفية صوغ أنظمة الأنواع صوريًا بعلاقة |- والتقييم بعلاقة -->، يمكننا جعل تلك الفكرة دقيقة.

وتشمل أهداف مصمم اللغة عادةً ضمان تحقق هاتين الخاصيتين، اللتين تقيمان علاقة بين |- و-->:

• التقدم (Progress): إذا كان التعبير جيد الأنواع، فهو إما قيمة بالفعل، وإما قادر على أخذ خطوة واحدة على الأقل. ويمكننا صوغ ذلك صوريًا بـ: «لكل e، إذا وُجد t بحيث {} |- e : t، فإن e قيمة، أو يوجد e' بحيث e --> e'.»
• الحفظ (Preservation): إذا كان التعبير جيد الأنواع، فإذا أخذ التعبير خطوة، يكون للتعير الجديد النوع نفسه الذي للتعير القديم. وصوريًا: «لكل e وt بحيث {} |- e : t، إذا وُجد e' بحيث e --> e'، فإن {} |- e' : t.»

ومعًا، يستلزم التقدم والحفظ أن تقييم تعبير جيد الأنواع لا يمكن أن يعلق (get stuck) أبدًا، بمعنى أنه يصل إلى غير قيمة لا تستطيع أخذ خطوة. وتُعرف هذه الخاصية بـ أمان الأنواع (type safety).

فمثلًا، سيتعلق 5 + true باستخدام علاقة تقييم SimPL، لأن العملية الأولية + لا يمكنها قبول قيمة منطقية كمعامل. لكن نظام أنواع SimPL لن يقبل ذلك البرنامج، فينجينا من الوصول إلى تلك الحالة أبدًا.

وبالعودة إلى SimPL التي كتبناها، كان كل موضع في تنفيذ step رفعنا فيه استثناءً موضعًا يعلق فيه التقييم. لكن نظام الأنواع يضمن عدم وقوع تلك الاستثناءات أبدًا.

10.6. استدلال الأنواع

OCaml وJava لغتان مصنّفتان الأنواع ساكنًا (statically typed)، بمعنى أن لكل ارتباط نوعًا يتحدد في وقت التصريف—أي قبل تنفيذ أي جزء من البرنامج. وفاحص الأنواع إجراء وقت تصريف يقبل البرنامج أو يرفضه. وفي المقابل، JavaScript وRuby لغتان مصنّفتان الأنواع ديناميكيًا؛ فلا يتحدد نوع الارتباط مسبقًا. ولذا فإن حسابات مثل ربط 42 بـ x ثم معاملة x كسلسلة نصية تؤدي إما إلى أخطاء وقت التشغيل، وإما إلى تحويل بين الأنواع في وقت التشغيل.

وخلافًا لـ Java، فإن OCaml مصنّفة الأنواع ضمنًا (implicitly typed)، بمعنى أن المبرمجين قلما يحتاجون إلى كتابة أنواع الارتباطات. وهذا مريح غالبًا، ولا سيما مع الدوال عالية الرتبة. (وإن اختلف بعضهم في ما إذا كان ذلك يجعل الشيفرة أسهل قراءة أم أصعب). لكن التصنيف الضمني لا يغيّر أبدًا حقيقة أن OCaml مصنّفة الأنواع ساكنًا. بل على العكس، يجب أن يكون فاحص الأنواع أكثر تطورًا لأنه يجب أن يستنتج ما «كانت ستكون عليه» تعليقات الأنواع لو كتبها المبرمجون كلها. ومن حيث المبدأ، يمكن أن يكون استدلال الأنواع وفحص الأنواع إجراءين منفصلين (فيستنتج المستنتِج الأنواع ثم يحدد الفاحص ما إذا كان البرنامج جيد الأنواع)، لكنهما يُدمجان عمليًا غالبًا في إجراء واحد يسمى إعادة بناء الأنواع (type reconstruction).

10.6.1. إعادة بناء الأنواع في OCaml

على مستوى عالٍ جدًا، تعمل خوارزمية إعادة بناء الأنواع في OCaml كما يلي:

• حدّد أنواع التعريفات بالترتيب، مستخدمًا أنواع التعريفات السابقة لاستنتاج أنواع التعريفات اللاحقة. (وهذا أحد أسباب عدم جواز استخدام اسم قبل أن يُربط في برنامج OCaml.)
• ولكل تعريف let، حلّل التعريف لتحديد قيود (constraints) على نوعه. فمثلًا، إذا رأى المستنتِج x + 1، استنتج أن نوع x يجب أن يكون int. ويجمع قيودًا مشابهة لتطبيقات الدوال ومطابقات الأنماط وما إلى ذلك. فكّر في هذه القيود كجملة معادلات كما تكون في الجبر.
• واستخدم جملة المعادلات تلك لحل نوع الاسم المراد تعريفه.

وتحاول خوارزمية إعادة بناء الأنواع في OCaml ألا ترفض أبدًا برنامجًا كان يمكن أن يُصرَّف لو كتب المبرمج الأنواع. كما تحاول ألا تقبل أبدًا برنامجًا لا يمكن أن يُصرَّف بحال. وقد تجعل بعض أجزاء اللغة الأكثر غموضًا تعليقات الأنواع ضرورية أحيانًا أو مفيدة على الأقل (انظر Real World OCaml، الفصل 22، «Type inference»، للأمثلة). لكن بالنسبة إلى معظم الشيفرة التي تكتبها، فتعليقات الأنواع اختيارية تمامًا حقًا.

وبما أنه سيكون مسهبًا مواصلة كتابة «خوارزمية إعادة بناء الأنواع المستخدمة في OCaml وغيرها من اللغات الوظيفية»، فسنسمي الخوارزمية HM. ويُستخدم ذلك الاسم في أدبيات لغات البرمجة كلها، لأن الخوارزمية اخترعها كل من Roger Hindley و Robin Milner مستقلًا.

وقد أُعيد اكتشاف HM مرات كثيرة من أناس كثيرين. استخدمها Curry استخدامًا غير صوري في الخمسينيات (وربما حتى الثلاثينيات). وكتبها صوريًا في 1967 (ونُشرت 1969). واكتشفها Hindley مستقلًا في 1969؛ و Morris في 1968؛ و Milner في 1978. وفي عالم المنطق، تعود أفكار مشابهة إلى عهد Tarski في العشرينيات ربما. وقد علّق Hindley على هذا التاريخ فقال،

لا بد أن يكون في قصة إعادة الاكتشاف المتواصل هذه عبرة؛ فربما كان ينبغي لأحدهم في الطريق أن يتعلم القراءة. أو لآخر أن يتعلم الكتابة.

ورغم أننا لم نر خوارزمية HM بعد، فلن تفاجئك على الأرجح معرفة أنها فعالة جدًا عادةً—فأنت لم تضطر ربما قط إلى انتظار المستوى الأعلى ليطبع الأنواع المستنتجة لبرامجك. وهي عمليًا تعمل في زمن خطي تقريبًا. لكن نظريًا توجد بعض البرامج الغريبة جدًا التي يمكن أن تفجّر زمن تشغيلها. (وتقنيًا، هو زمن أسي.) وللمتعة، جرّب كتابة الشيفرة التالية في utop:

# let b = true;;
# let f0 = fun x -> x + 1;;
# let f = fun x -> if b then f0 else fun y -> x y;;
# let f = fun x -> if b then f else fun y -> x y;;
# let f = fun x -> if b then f else fun y -> x y;;
(* keep repeating that last line *)

وسترى الأنواع تطول وتطول، وفي النهاية (عند نحو 20 تكرارًا) سيسبب استدلال الأنواع تأخيرًا كبيرًا.

10.6.2. الاستدلال القائم على القيود

ولنمهّد لخوارزمية HM لاستدلال الأنواع بالبدء بهذه اللغة الصغيرة:

e ::= x | i | b | e1 bop e2
    | if e1 then e2 else e3
    | fun x -> e
    | e1 e2

bop ::= + | * | <=

t ::= int | bool | t1 -> t2

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

وبما أن الدوال المجهولة في هذه اللغة بلا تعليقات أنواع، علينا استنتاج نوع الوسيطة x. فمثلًا،

• في fun x -> x + 1، يجب أن يكون نوع الوسيطة x هو int، ومن ثمّ نوع الدالة int -> int.
• وفي fun x -> if x then 1 else 0، يجب أن يكون نوع الوسيطة x هو bool، ومن ثمّ نوع الدالة bool -> int.
• والدالة fun x -> if x then x else 0 غير قابلة للتصنيف نوعيًا، لأنها ستتطلب أن يكون لـ x النوعان int وbool معًا، وذلك غير مسموح.

تبسيط نحوي. يمكننا معاملة e1 bop e2 كسكر نحوي لـ ( bop ) e1 e2. أي أننا نعامل العوامل البينية كتطبيق دوال سابق. ولنستحدث صنفًا نحويًا جديدًا n لـالأسماء (names)، يعمّم المعرّفات والعوامل. ويغيّر ذلك الصياغة إلى:

e ::= n | i | b
    | if e1 then e2 else e3
    | fun x -> e
    | e1 e2

n ::= x | bop

bop ::= ( + ) | ( * ) | ( <= )

t ::= int | bool | t1 -> t2

نعرف بالفعل أنواع تلك العوامل المدمجة:

( + ) : int -> int -> int
( * ) : int -> int -> int
( <= ) : int -> int -> bool

تلك الأنواع معطاة؛ فلا يلزمنا استنتاجها. وهي جزء من البيئة الساكنة الأولية. وفي OCaml يمكن لاحقًا أن تحجب أسماء تلك العوامل قيم ذات أنواع مختلفة، لكن لا يلزمنا القلق بشأن ذلك هنا لأننا لا نملك let بعد.

فكيف تستنتج أنت ذهنيًا نوع fun x -> 1 + x، أو بالأحرى fun x -> ( + ) 1 x؟ الأمر صار تلقائيًا الآن، لكن يمكننا تفكيكه إلى قطع:

• ابدأ بأن نوع x نوع مجهول t.
• لاحظ أن ( + ) معروف أن نوعه int -> (int -> int).
• لذا يجب أن يكون نوع وسيطه الأول int. وهو ما ينطبق على 1.
• ويجب أن يكون نوع وسيطه الثاني int أيضًا. إذن t = int. وهذا قيد على t.
• وأخيرًا، يجب أن يكون نوع جسم الدالة int أيضًا، لأن ذلك نوع إعادة ( + ).
• لذا يجب أن يكون نوع الدالة كلها t -> int.
• وبما أن t = int، فذلك النوع int -> int.

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

ولنستحدث علاقة رباعية جديدة env |- e : t -| C، تُقرأ كما يلي: «في البيئة env، يُستنتج أن نوع التعبير e هو t وتُولَّد مجموعة القيود C.» والقيد معادلة بالشكل t1 = t2 لأي نوعين t1 وt2.

وإذا فكرنا في العلاقة كدالة لاستدلال الأنواع، فالنقطتان في المنتصف تفصلان المدخل عن المخرج. والمدخلان هما env وe: نريد معرفة نوع e في البيئة env. وتعيد الدالة كمخرج نوعًا t وقيودًا C.

والجزء e : t في منتصف العلاقة هو تقريبًا ما تراه في المستوى الأعلى: تدخل تعبيرًا، فيخبرك بالنوع. لكن حول ذلك بيئة ومجموعة قيود env |- ... -| C غير مرئية لك. فالرمزان المحيطان يظهران أجزاء استدلال الأنواع التي لا يظهرها المستوى الأعلى.

وأسهل أجزاء الاستدلال هي الثوابت:

env |- i : int -| {}

env |- b : bool -| {}

أي ثابت صحيح i، مثل 42، معروف أن نوعه int، ولا تُولَّد قيود. وكذلك الثوابت المنطقية.

ويقتضي استدلال نوع اسم البحث عنه في البيئة:

env |- n : env(n) -| {}

ولا تُولَّد قيود.

وإذا لم يكن الاسم مرتبطًا في البيئة، فلا يمكن تصنيف التعبير نوعيًا. إنه خطأ اسم غير مرتبط.

والقواعد المتبقية هي في جوهرها القواعد نفسها التي رأيناها في فحص الأنواع، لكن كلًا منها يولّد متغير نوع (type variable) وربما بعض القيود على ذلك المتغير.

If.

وإليك قاعدة تعبيرات if:

env |- if e1 then e2 else e3 : 't -| C1, C2, C3, t1 = bool, 't = t2, 't = t3
  if fresh 't
  and env |- e1 : t1 -| C1
  and env |- e2 : t2 -| C2
  and env |- e3 : t3 -| C3

لاستدلال نوع if، نستنتج الأنواع t1 وt2 وt3 لكل من تعبيراته الفرعية، مع أي قيود عليها. ولا سيطرة لنا على ما قد تكون عليه تلك الأنواع؛ فذلك يعتمد على ما كتبه المبرمج. لكننا نعلم أن نوع الشرط يجب أن يكون bool. لذا نولّد قيدًا بأن t1 = bool.

وعلاوة على ذلك، نعلم أن كلا الفرعين يجب أن يكون له النوع نفسه—وإن كنا لا نعرف مسبقًا ما قد يكون ذلك النوع. لذا نخترع متغير نوع طازجًا (fresh) 't ليمثل ذلك النوع. ومتغير النوع طازج إذا لم يُستخدم في أي موضع آخر أثناء استدلال الأنواع. فاختيار متغير نوع طازج يعني ببساطة اختيار اسم جديد لا يمكن الخلط بينه وبين أي أسماء أخرى في البرنامج. ونعيد 't كنوع if، ونسجّل قيدين 't = t2 و't = t3 لنقول إن كلا الفرعين يجب أن يكون له ذلك النوع.

ولذا نحتاج إلى إضافة متغيرات الأنواع إلى صياغة الأنواع:

t ::= 'x | int | bool | t1 -> t2

ومن أمثلة متغيرات الأنواع 'a و'foobar و't. وفي الأخير، t معرّف، لا متغير فوقي.

وإليك مثالًا:

{} |- if true then 1 else 0 : 't -| bool = bool, 't = int
  {} |- true : bool -| {}
  {} |- 1 : int -| {}
  {} |- 0 : int -| {}

ومجموعة القيود الكاملة المولَّدة هي {}, {}, {}, bool = bool, 't = int, 't = int، لكن ذلك يبسّط بالطبع إلى bool = bool, 't = int فحسب. ومن مجموعة القيود تلك نرى أن نوع if true then 1 else 0 يجب أن يكون int.

الدوال المجهولة.

بما أنه لا يوجد تعليق نوع على x، فيجب استنتاج نوعه:

env |- fun x -> e : 't1 -> t2 -| C
  if fresh 't1
  and env, x : 't1 |- e : t2 -| C

نستحدث متغير نوع طازجًا 't1 ليمثل نوع x، ونستنتج نوع الجسم e في البيئة التي فيها x : 't1. وأينما استُخدم x في e، فقد يؤدي ذلك إلى توليد قيود تتضمن 't1. وستصير تلك القيود جزءًا من C.

وإليك دالة نرى فيها فورًا أن x : bool، لكن لنعمل على الاستدلال خطوة خطوة:

{} |- fun x -> if x then 1 else 0 : 't1 -> 't -| 't1 = bool, 't = int
  {}, x : 't1 |- if x then 1 else 0 : 't -| 't1 = bool, 't = int
    {}, x : 't1 |- x : 't1 -| {}
    {}, x : 't1 |- 1 : int -| {}
    {}, x : 't1 |- 0 : int -| {}

النوع المستنتج للدالة هو 't1 -> 't، مع القيدين 't1 = bool و't = int. وبتبسيط ذلك، نوع الدالة bool -> int.

تطبيق الدوال.

يجب استنتاج نوع التطبيق كله، لأننا لا نعرف بعد أي شيء عن نوعي أي من التعبيرين الفرعيين:

env |- e1 e2 : 't -| C1, C2, t1 = t2 -> 't
  if fresh 't
  and env |- e1 : t1 -| C1
  and env |- e2 : t2 -| C2

نستحدث متغير نوع طازجًا 't لنوع تعبير التطبيق. ونستخدم الاستدلال لتحديد أنواع التعبيرات الفرعية وأي قيود تولّدها. ونضيف قيدًا جديدًا واحدًا، t1 = t2 -> 't، يعبّر عن أن نوع الطرف الأيسر e1 يجب أن يكون دالة تأخذ وسيطة من النوع t2 وتعيد قيمة من النوع 't.

ولنكن I هي البيئة الأولية التي تربط العوامل المنطقية. ولنستنتج نوع تطبيق جزئي لـ ( + ):

I |- ( + ) 1 : 't -| int -> int -> int = int -> 't
  I |- ( + ) : int -> int -> int -| {}
  I |- 1 : int -| {}

من القيد الناتج نرى أن

int -> int -> int
=
int -> 't

وبإزالة int -> من الطرف الأيسر لكل من نوعي الدالة هذين، يتبقى لدينا

int -> int
=
't

ومن ثمّ فنوع ( + ) 1 هو int -> int.

10.6.3. حل القيود

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

5x + 2y =  9
 x -  y = -1

وبحل تلك الجملة نحصل على x = 1 وy = 2. وإذا استبدلنا 1 بـ x و2 بـ y، نحصل على:

5(1) + 2(2) =  9
  1  -   2  = -1

وهي تختزل إلى

 9 =  9
-1 = -1

وفي مصطلحات لغات البرمجة (وإن لم يكن في جبر المدرسة الثانوية ربما)، نقول إن الاستبدالين {1 / x} و{2 / y} معًا يوحّدان (unify) مجموعة المعادلات تلك، لأنهما يجعلان كل معادلة «تتوحد» بحيث يتطابق طرفها الأيسر مع طرفها الأيمن.

وحل جمل المعادلات على الأنواع مشابه. فكما وجدنا أعدادًا نستبدلها بالمتغيرات أعلاه، نريد الآن إيجاد أنواع نستبدلها بمتغيرات الأنواع، فنوحّد بذلك جملة المعادلات.

وكثيرًا مثل الاستبدالات التي عرّفناها سابقًا لنموذج الاستبدال في التقييم، سنكتب {t / 'x} لـاستبدال النوع (type substitution) الذي يربط متغير النوع 'x بالنوع t. فمثلًا، t1 {t2/'x} يعني النوع t1 مع استبدال t2 بـ 'x.

ويمكننا تعريف الاستبدال على الأنواع كما يلي:

int {t / 'x} = int
bool {t / 'x} = bool
'x {t / 'x} = t
'y {t / 'x} = 'y
(t1 -> t2) {t / 'x} =  (t1 {t / 'x} ) -> (t2 {t / 'x} )

وبالنظر إلى استبدالين S1 وS2، نكتب S1; S2 لنعني الاستبدال الذي هو تركيبهما التسلسلي (sequential composition)، المعرَّف كما يلي:

t (S1; S2) = (t S1) S2

والترتيب مهم. فمثلًا، 'x ({('y -> 'y) / 'x}; {bool / 'y}) هو bool -> bool، لا 'y -> 'y. ويمكننا بناء استبدالات أكبر وأكبر بهذه الطريقة.

ويمكن تطبيق استبدال S على قيد t = t'. والنتيجة (t = t') S معرَّفة بأنها t S = t' S. أي أننا نطبّق الاستبدال على طرفي القيد فحسب.

وأخيرًا، يمكن تطبيق استبدال على مجموعة C من القيود؛ والنتيجة C S هي نتيجة تطبيق S على كل قيد من القيود الفردية في C.

ويوحّد استبدال S قيدًا t_1 = t_2 إذا أعطى t_1 S النوع نفسه الذي يعطيه t_2 S. فمثلًا، الاستبدال S = {int -> int / 'y}; {int / 'x} يوحّد القيد 'x -> ('x -> int) = int -> 'y، لأن

('x -> ('x -> int)) S
=
int -> (int -> int)

و

(int -> 'y) S
=
int -> (int -> int)

ويوحّد استبدال S مجموعة C من القيود إذا وحّد S كل قيد في C.

وأخيرًا يمكننا أن نقول بدقة ما يعنيه حل مجموعة من القيود: يجب إيجاد استبدال يوحّد المجموعة. أي أننا نحتاج إلى إيجاد متتالية من التطبيقات من متغيرات الأنواع إلى الأنواع، بحيث تجعل المتتالية كل معادلة في مجموعة القيود «تتوحد»، أي يتطابق طرفاها الأيمن والأيسر.

ولإيجاد استبدال يوحّد مجموعة القيود C، نستخدم خوارزمية unify، المعرَّفة كما يلي:

• إذا كانت C المجموعة الفارغة، فإن unify(C) هو الاستبدال الفارغ.
• وإذا احتوت C قيدًا واحدًا على الأقل t1 = t2 وربما بعض القيود الأخرى C'، فتُعرَّف unify(C) كما يلي: إذا كان t1 وt2 كلاهما النوع البسيط نفسه—أي كلاهما متغير النوع نفسه 'x، أو كلاهما int، أو كلاهما bool—فأعد unify(C'). وفي هذه الحالة لم يحتوِ القيد على معلومات مفيدة، فنطرحه ونواصل.
• وإذا كان t1 متغير نوع 'x ولا يظهر 'x في t2، فلنكن S = {t2 / 'x}، وأعد S; unify(C' S). وفي هذه الحالة نُزيل المتغير 'x من جملة المعادلات، كثيرًا مثل الحذف الغاوسي في حل المعادلات الجبرية.
• وإذا كان t2 متغير نوع 'x ولا يظهر 'x في t1، فلنكن S = {t1 / 'x}، وأعد S; unify(C' S). وهذا إزالة مثل الحالة السابقة.
• وإذا كان t1 = i1 -> o1 وt2 = i2 -> o2، حيث i1 وi2 وo1 وo2 أنواع، فإن unify(i1 = i2, o1 = o2, C'). وفي هذه الحالة نفكك قيدًا واحدًا إلى قيدين أصغر ونعيد إضافة هذين القيدين ليوحَّدا كذلك.
• وإلا، فافشل. فلا يوجد موحِّد ممكن.

وفي الحالتين الفرعيتين الثانية والثالثة، يضمن التحقق من وجوب ألا يظهر 'x في النوع أن الخوارزمية تُزيل المتغير فعلًا. وإلا فقد تنتهي الخوارزمية إلى إعادة إدخال المتغير بدلًا من إزالته.

ومن الممكن إثبات أن خوارزمية التوحيد تنتهي دائمًا، وأنها تنتج نتيجة إذا وفقط إذا وُجد موحِّد فعلًا—أي إذا وفقط إذا كانت لمجموعة القيود حل. علاوة على ذلك، الحل الذي تنتجه الخوارزمية هو الموحِّد الأعم (most general unifier)، بمعنى أنه إذا كان S = unify(C) ووحّد S' المجموعة C أيضًا، فلا بد من وجود S'' بحيث S' = S; S''. ومثل ذلك S' أقل عمومية من S لأنه يحتوي الاستبدالات الإضافية في S''.

10.6.4. إتمام استدلال الأنواع

ولنراجع ما فعلناه حتى الآن. بدأنا بهذه اللغة:

e ::= n | i | b
    | if e1 then e2 else e3
    | fun x -> e
    | e1 e2

n ::= x | bop

bop ::= ( + ) | ( * ) | ( <= )

t ::= int | bool | t1 -> t2

ثم قدّمنا خوارزمية لاستدلال نوع تعبير. ويأتي ذلك النوع مع مجموعة من القيود. وعُبّر عن الخوارزمية بصيغة علاقة env |- e : t -| C.

وبعد ذلك قدّمنا خوارزمية التوحيد لحل مجموعات القيود. وتلك الخوارزمية تنتج كمخرج متتالية S من الاستبدالات، أو تفشل. وإن فشلت، فالتعبير e غير قابل للتصنيف نوعيًا.

ولإتمام استدلال الأنواع وإعادة بناء نوع e، نحسب t S فحسب. أي أننا نطبّق حل القيود على النوع t الناتج من توليد القيود.

ولنكن p ذلك النوع. أي p = t S. ومن الممكن إثبات أن p هو النوع الرئيسي (principal) للتعبير، بمعنى أنه إذا كان لـ e النوع t لأي t آخر، فيوجد استبدال S بحيث t = p S.

فمثلًا، النوع الرئيسي لدالة الهوية fun x -> x سيكون 'a -> 'a. لكن يمكنك أيضًا إعطاء تلك الدالة النوع الأقل نفعًا int -> int. وما نقوله إن HM ستنتج 'a -> 'a، لا int -> int. فـ HM، بمعنى ما، تستنتج النوع الأكثر «تسامحًا» الممكن لتعبير.

مثال محلول. لنستنتج نوع التعبير التالي:

fun f -> fun x -> f (( + ) x 1)

ليس كثيرًا من الشيفرة، لكن هذا سيتشعب كثيرًا!

نبدأ في البيئة الأولية I التي تربط، من بين أشياء أخرى، ( + ) بـ int -> int -> int.

I |- fun f -> fun x -> f (( + ) x 1)

نترك الآن : t -| C، لأن ذلك مخرج توليد القيود. ولم نكتشف المخرج بعد! وبما أن لدينا دالة، نستخدم قاعدة الدوال للاستدلال فنمضي بتقديم متغير نوع طازج للوسيطة:

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)  <-- Here

ومرة أخرى لدينا دالة، ومن ثمّ متغير نوع طازج:

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)  <-- Here

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

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}  <-- Here

وبعد ذلك التعبير الفرعي الثاني.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1  <-- Here

ذلك تطبيق آخر، لذا علينا معالجة تعبيريه الفرعيين. تذكّر أن ( + ) x 1 يُحلَّل نحويًا كـ (( + ) x) 1. فالتعبير الفرعي الأول هو المعقد الذي يجب معالجته.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1
        I, f : 'a, x : 'b |- ( + ) x  <-- Here

وتطبيق آخر بعد.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1
        I, f : 'a, x : 'b |- ( + ) x
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}  <-- Here

كان ذلك سهلًا، لأننا لم نحتج إلا إلى البحث عن الاسم ( + ) في البيئة. والتالي سهل أيضًا، لأننا نبحث عن x فحسب.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1
        I, f : 'a, x : 'b |- ( + ) x
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
          I, f : 'a, x : 'b |- x : 'b -| {}  <-- Here

وأخيرًا صرنا جاهزين لحل تطبيق دالة! نستحدث متغير نوع طازجًا ونضيف قيدًا. والقيد أن النوع المستنتج int -> int -> int للتعبير الفرعي الأيسر يجب أن يساوي النوع المستنتج 'b للتعبير الفرعي الأيمن مع سهم ومتغير النوع الطازج 'c، أي 'b -> 'c.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1
        I, f : 'a, x : 'b |- ( + ) x : 'c -| int -> int -> int = 'b -> 'c  <-- Here
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
          I, f : 'a, x : 'b |- x : 'b -| {}

الآن صرنا جاهزين للوسيطة التي تُمرَّر إلى تلك الدالة.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1
        I, f : 'a, x : 'b |- ( + ) x : 'c -| int -> int -> int = 'b -> 'c
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
          I, f : 'a, x : 'b |- x : 'b -| {}
        I, f : 'a, x : 'b |- 1 : int -| {}  <-- Here

ومرة أخرى يمكننا حل تطبيق دالة بمتغير نوع جديد وقيد جديد.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1)
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1 : 'd -| 'c = int -> 'd, int -> int -> int = 'b -> 'c  <-- Here
        I, f : 'a, x : 'b |- ( + ) x : 'c -| int -> int -> int = 'b -> 'c
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
          I, f : 'a, x : 'b |- x : 'b -| {}
        I, f : 'a, x : 'b |- 1 : int -| {}

ومرة أخرى، تطبيق دالة، فمتغير نوع جديد وقيد جديد.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1)
    I, f : 'a, x : 'b |- f (( + ) x 1) : 'e -| 'a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c   <-- Here
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1 : 'd -| 'c = int -> 'd, int -> int -> int = 'b -> 'c
        I, f : 'a, x : 'b |- ( + ) x : 'c -| int -> int -> int = 'b -> 'c
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
          I, f : 'a, x : 'b |- x : 'b -| {}
        I, f : 'a, x : 'b |- 1 : int -| {}

والآن نصل أخيرًا إلى إتمام دالة مجهولة. ونوعها المستنتج هو متغير النوع الطازج 'b لوسيطتها x، يليه سهم ثم النوع المستنتج e لجسمها.

I |- fun f -> fun x -> f (( + ) x 1)
  I, f : 'a |- fun x -> f (( + ) x 1) : 'b -> 'e -| 'a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c   <-- Here
    I, f : 'a, x : 'b |- f (( + ) x 1) : 'e -| 'a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c
      I, f : 'a, x : 'b |- f : 'a -| {}
      I, f : 'a, x : 'b |- ( + ) x 1 : 'd -| 'c = int -> 'd, int -> int -> int = 'b -> 'c
        I, f : 'a, x : 'b |- ( + ) x : 'c -| int -> int -> int = 'b -> 'c
          I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
          I, f : 'a, x : 'b |- x : 'b -| {}
        I, f : 'a, x : 'b |- 1 : int -| {}

ويمكن الآن إتمام الدالة المجهولة الأخيرة بالطريقة نفسها:

I |- fun f -> fun x -> f (( + ) x 1) : 'a -> 'b -> 'e -| 'a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c  <-- Here
  I, f : 'a |- fun x -> f (( + ) x 1) : 'b -> 'e -| 'a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c
    I, f : 'a, x : 'b |- f (( + ) x 1) : 'e -| 'a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c
       I, f : 'a, x : 'b |- f : 'a -| {}
       I, f : 'a, x : 'b |- ( + ) x 1 : 'd -| 'c = int -> 'd, int -> int -> int = 'b -> 'c
         I, f : 'a, x : 'b |- ( + ) x : 'c -| int -> int -> int = 'b -> 'c
           I, f : 'a, x : 'b |- ( + ) : int -> int -> int -| {}
           I, f : 'a, x : 'b |- x : 'b -| {}
         I, f : 'a, x : 'b |- 1 : int -| {}

نتيجةً لتوليد القيود، نعلم أن نوع التعبير هو 'a -> 'b -> 'e، حيث

'a = 'd -> 'e
'c = int -> 'd
int -> int -> int = 'b -> 'c

لحلّ ذلك النظام من المعادلات، نستخدم خوارزمية التوحيد (unification):

unify('a = 'd -> 'e, 'c = int -> 'd, int -> int -> int = 'b -> 'c)

يعطي القيد الأول استبدالًا {('d -> 'e) / 'a}، نسجّله كجزء من الحل، ونطبّقه أيضًا على القيود المتبقية:

...
=
{('d -> 'e) / 'a}; unify(('c = int -> 'd, int -> int -> int = 'b -> 'c) {('d -> 'e) / 'a})
=
{('d -> 'e) / 'a}; unify('c = int -> 'd, int -> int -> int = 'b -> 'c)

يتصرّف القيد الثاني تصرّفًا مشابهًا للأول:

...
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; unify((int -> int -> int = 'b -> 'c) {(int -> 'd) / 'c})
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; unify(int -> int -> int = 'b -> int -> 'd)

يتفكّك قيد الدالة إلى قيدين أصغر:

...
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; unify(int = 'b, int -> int = int -> 'd)

نحصل على استبدال آخر:

...
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; {int / 'b}; unify((int -> int = int -> 'd) {int / 'b})
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; {int / 'b}; unify(int -> int = int -> 'd)

ثم نصل إلى تفكيك قيد دالة آخر:

...
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; {int / 'b}; unify(int = int, int = 'd)

القيد الأول من القيود الجديدة الناتجة بديهي ويُطرح ببساطة:

...
=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; {int / 'b}; unify(int = 'd)

يعطينا القيد الأخير تمامًا استبدالًا آخر:

=
{('d -> 'e) / 'a}; {(int -> 'd) / 'c}; {int / 'b}; {int / 'd}

وللإنهاء، نطبّق الاستبدال الذي أخرجه التوحيد على النوع المستنتَج بتوليد القيود:

('a -> 'b -> 'e) {('d -> 'e) / 'a}; {(int -> 'd) / 'c}; {int / 'b}; {int / 'd}
=
(('d -> 'e) -> 'b -> 'e) {(int -> 'd) / 'c}; {int / 'b}; {int / 'd}
=
(('d -> 'e) -> 'b -> 'e) {int / 'b}; {int / 'd}
=
(('d -> 'e) -> int -> 'e) {int / 'd}
=
(int -> 'e) -> int -> 'e

وهذا فعلًا النوع نفسه الذي سيستنتجه OCaml للتعبير الأصلي:

# fun f -> fun x -> f (( + ) x 1);;
- : (int -> 'a) -> int -> 'a = <fun>

إلا أن OCaml يستخدم معرّف متغيّر نوع مختلفًا. فـ OCaml لطيف معنا و«يُنزل» متغيّرات النوع إلى أحرف أبجدية أصغر. ويمكننا فعل ذلك أيضًا بقليل من العمل الإضافي.

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

10.6.5. تعدّد أشكال let

الآن سنضيف تعبيرات let إلى لغتنا الصغيرة:

e ::= x | i | b | e1 bop e2
    | if e1 then e2 else e3
    | fun x -> e
    | e1 e2
    | let x = e1 in e2   (* new *)

يتّضح أن استدلال الأنواع لها أعقد بكثير مما قد يُتوقع. والنهج الساذج سيكون إضافة قاعدة توليد القيود هذه:

env |- let x = e1 in e2 : t2 -| C1, C2
  if env |- e1 : t1 -| C1
  and env, x : t1 |- e2 : t2 -| C2

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

{} |- let x = 42 in x : int -| {}
  {} |- 42 : int -| {}
  x : int |- x : int -| {}

المشكلة أنه عندما تكون القيمة المربوطة دالة متعدّدة الأشكال، تولّد تلك القاعدة قيودًا مقيِّدة أكثر من اللازم. فمثلًا، تأمّل دالة الهوية:

let id = fun x -> x in
let a = id 0 in
id true

لا يجد OCaml أي صعوبة في استنتاج نوع id بأنه 'a -> 'a والسماح بتطبيقه على int وbool معًا. لكن القاعدة أعلاه ليست بهذا التسامح بشأن التطبيق على النوعين معًا. فعندما نستخدمها، نولّد الأنواع والقيود التالية:

{} |- let id = fun x -> x in (let a = id 0 in id true) : 'c -| 'a -> 'a = int -> 'b, 'a -> 'a = bool -> 'c
  {} |- fun x -> x : 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a -> 'a |- let a = id 0 in id true : 'c -| 'a -> 'a = int -> 'b, 'a -> 'a = bool -> 'c   <--- POINT 1
    id : 'a -> 'a |- id 0 : 'b -| 'a -> 'a = int -> 'b
      id : 'a -> 'a |- id : 'a -> 'a -| {}
      id : 'a -> 'a |- 0 : int -| {}
    id : 'a -> 'a, a : 'b |- id true : 'c -| 'a -> 'a = bool -> 'c   <--- POINT 2
      id : 'a -> 'a, a : 'b |- id : 'a -> 'a -| {}
      id : 'a -> 'a, a : 'b |- true : bool -| {}

لاحظ أننا نستنتج فعلًا نوع 'a -> 'a لـ id، وهو ما تراه في البيئة في الأسطر اللاحقة من المثال. لكننا في النقطة 1 نستنتج القيد 'a -> 'a = int -> 'b، وفي النقطة 2 نستنتج 'a -> 'a = bool -> 'c. وعندما تصادف خوارزمية التوحيد هذين القيدين، ستفكّكهما إلى 'a = int و'a = 'b و'a = bool و'a = 'c. والقيدان الأول والثالث متناقضان، لأنه لا يمكن أن يكون 'a = int و'a = bool معًا. وسيُستبدل أحدهما أثناء التوحيد، فيبقى قيد غير قابل للإرضاء هو int = bool. وعند تلك النقطة سيفشل التوحيد، معلنًا أن البرنامج سيّئ الأنواع.

المشكلة أن متغيّر النوع 'a في النوع المستنتَج لـ id يمثّل نوعًا مجهولًا لكنه ثابت. وعند كل تطبيق لـ id، نريد أن ندع 'a يصبح نوعًا مختلفًا، بدلًا من إجباره على أن يكون النوع نفسه دائمًا.

حلّ مشكلة تعدّد الأشكال في تعبيرات let ليس بسيطًا. فهو يتطلب إدخال نوع جديد من الأنواع: مخطط النوع (type scheme). تشبه مخططات الأنواع التكميم الكلي (universal quantification) في المنطق الرياضي. فمثلًا، قد تكتب في المنطق: «لكل عدد طبيعي $x$، يتحقق أن $0 \cdot x = 0$». وعبارة «لكل» هي التكميم الكلي: فهي تجرّد من $x$ بعينه وتصرّح بخاصية صحيحة لكل الأعداد الطبيعية.

يُكتب مخطط النوع 'a . t، حيث 'a متغيّر نوع وt نوع قد يظهر فيه 'a. فمثلًا، 'a . 'a -> 'a مخطط نوع. وهو نوع دالة تأخذ قيمة من النوع 'a وتعيد قيمة من النوع 'a، لكل 'a. ومن ثم فهو نوع دالة الهوية متعدّدة الأشكال.

يمكن أن يكون لدينا أيضًا متغيّرات نوع كثيرة على يسار النقطة في مخطط النوع. فمثلًا، 'a 'b . 'a -> 'b -> 'a هو نوع دالة تأخذ وسيطين وتعيد الأول. وفي OCaml، يمكننا كتابة ذلك بالشكل fun x y -> x. لاحظ أن utop يستنتج نوعه كما نتوقع:

# let f = fun x y -> x;;
val f : 'a -> 'b -> 'a = <fun>

لكن يمكننا في الواقع كتابة تعليق نوعي يدويًا مع مخطط نوع:

# let f : 'a 'b . 'a -> 'b -> 'a = fun x y -> x;;
val f : 'a -> 'b -> 'a = <fun>

لاحظ أن OCaml يقبل تعليقنا النوعي اليدوي لكنه لا يدرج الجزء 'a 'b . منه في ناتجه. لكنه موجود ضمنًا، وكان كذلك دائمًا. وبوجه عام، كلما استنتج OCaml نوعًا t وكان في ذلك النوع متغيّرات نوع، فهو في الحقيقة مخطط نوع. فمثلًا، نوع List.length هو في الحقيقة مخطط نوع:

# let mylen : 'a . 'a list -> int = List.length;;
val mylen : 'a list -> int = <fun>

كل ما في الأمر أن OCaml لا يتكلف عناء إخراج قائمة متغيّرات النوع الواقعة على يسار النقطة في مخطط النوع. فهي في الحقيقة ستكدّر الناتج فحسب، وكثير من المبرمجين لا يحتاجون أبدًا إلى معرفتها. لكن بما أنك تتعلم الآن استدلال الأنواع، فقد حان وقت أن تعرفها.

الآن بعد أن أصبحت لدينا مخططات أنواع، سيكون لدينا بيئات ساكنة تربط الأسماء بمخططات أنواع. ويمكننا اعتبار الأنواع حالات خاصة من مخططات الأنواع تكون فيها قائمة متغيّرات النوع فارغة. ومع مخططات الأنواع، تتغيّر قاعدة let من القاعدة الساذجة أعلاه في أمر واحد فقط، هو generalize في السطر الأخير:

env |- let x = e1 in e2 : t2 -| C1, C2
  if env |- e1 : t1 -| C1
  and generalize(C1, env, x : t1) |- e2 : t2 -| C2

مهمة generalize هي أخذ نوع كـ 'a -> 'a وتعميمه إلى مخطط نوع كـ 'a . 'a -> 'a في بيئة env في مواجهة القيود C1. وسنعود إلى كيفية عملها بعد قليل. وقبل ذلك، ثمة قاعدة أخرى تحتاج إلى تغيير، هي قاعدة الاسم:

env |- n : instantiate(env(n)) -| {}

الشيء الوحيد الذي يتغيّر هناك هو استخدام instantiate. فمهمته أخذ مخطط نوع كـ 'a . 'a -> 'a وتجسيده في نوع جديد (ونعني هنا نوعًا بالضبط، لا مخطط نوع) بمتغيّرات نوع طازجة. فمثلًا، يمكن تجسيد 'a . 'a -> 'a ليصبح 'b -> 'b، إن لم يكن 'b قيد الاستخدام بعد في مكان آخر بوصفه متغيّر نوع.

وإليك كيف تعمل هاتان القاعدتان المنقّحتان معًا لإنجاز مثالنا السابق مع دالة الهوية على نحو صحيح:

{} |- let id = fun x -> x in (let a = id 0 in id true)
  {} |- fun x -> x : 'a -> 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a . 'a -> 'a |- let a = id 0 in id true   <--- POINT 1

لنتوقف هناك عند النقطة 1. عندما تُوضع id في البيئة بقاعدة let، يُعمَّم نوعها من 'a -> 'a إلى 'a . 'a -> 'a؛ أي من نوع إلى مخطط نوع. ويسجّل ذلك حقيقة أن كل تطبيق لـ id ينبغي أن يستخدم قيمته الخاصة لـ 'a. ونواصل:

{} |- let id = fun x -> x in (let a = id 0 in id true)
  {} |- fun x -> x : 'a -> 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a . 'a -> 'a |- let a = id 0 in id true   <--- POINT 1
    id : 'a . 'a -> 'a |- id 0
      id : 'a . 'a -> 'a |- id : 'b -> 'b -| {}   <--- POINT 3

نتوقف هنا عند النقطة 3. عندما يُطبَّق id على 0، نجسّد متغيّر نوعه 'a بمتغيّر نوع طازج 'b. لنُكمل:

{} |- let id = fun x -> x in (let a = id 0 in id true) : 'e -| 'b -> 'b = int -> 'c, 'd -> 'd = bool -> 'e
  {} |- fun x -> x : 'a -> 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a . 'a -> 'a |- let a = id 0 in id true : 'e -| 'b -> 'b = int -> 'c, 'd -> 'd = bool -> 'e   <--- POINT 1
    id : 'a . 'a -> 'a |- id 0 : 'c -| 'b -> 'b = int -> 'c
      id : 'a . 'a -> 'a |- id : 'b -> 'b -| {}   <--- POINT 3
      id : 'a . 'a -> 'a |- 0 : int -| {}
    id : 'a . 'a -> 'a, a : 'b |- id true : 'e -| 'd -> 'd = bool -> 'e   <--- POINT 2
      id : 'a . 'a -> 'a, a : 'b |- id : 'd -> 'd -| {}   <--- POINT 4
      id : 'a . 'a -> 'a, a : 'b |- true : bool -| {}

عند النقطة 4، عندما يُطبَّق id على true، نجسّد متغيّر نوعه 'a مرة أخرى بمتغيّر نوع طازج، هو 'd هذه المرة. لذا لم تعد القيود المجموعة عند النقطتين 1 و2 متناقضة، لأنها تتحدث عن متغيّري نوع مختلفين. وتلك القيود هي:

'b -> 'b = int -> 'c
'd -> 'd = bool -> 'e

ولذلك ستستنتج خوارزمية التوحيد:

'b = int
'c = int
'd = bool
'e = bool

وهكذا يُستنتَج بنجاح أن نوع التعبير كله هو bool.

التجسيد والتعميم. استخدمنا دالتين جديدتين، instantiate وgeneralize، لتعريف استدلال الأنواع في تعبيرات let. وعلينا تعريف هاتين الدالتين.

الأسهل هي instantiate. فبالنظر إلى مخطط نوع 'a1 'a2 ... 'an . t، نجسّده عبر:

• اختيار n من متغيّرات النوع الطازجة، و
• استبدال كل منها بـ 'a1 حتى 'an في t.

الاستبدال هنا غير معقّد، مقارنةً بما كان عليه في التقييم ضمن نموذج الاستبدال، لأنه لا يوجد في النوع ما يمكنه ربط أسماء المتغيّرات.

لكن generalize تتطلب عملًا أكثر. وإليك قاعدة let مرة أخرى:

env |- let x = e1 in e2 : t2 -| C1, C2
  if env |- e1 : t1 -| C1
  and generalize (C1, env, x : t1) |- e2 : t2 -| C2

لتعميم t1، نفعل ما يلي.

أولًا، نتظاهر بأن e1 هي كل ما يهم، وبأن بقية تعبير let غير موجودة. فلو كانت e1 البرنامج كله، فكيف ننهي استدلال الأنواع؟ كنا سنشغّل خوارزمية التوحيد على C1، فنحصل على استبدال S، ونعيد t1 S بوصفه النوع المستنتَج لـ e1. فلنفعل ذلك الآن. ولنسمِّ ذلك النوع المستنتَج u1. ولنطبّق أيضًا S على env للحصول على بيئة جديدة env1، تعكس الآن كل معلومات الأنواع التي جمعناها من e1.

ثانيًا، نحدّد أي متغيّرات نوع في u1 ينبغي تعميمها. ولِمَ لا نعمّمها كلها؟ لأن بعض متغيّرات النوع قد تكون أدخلتها شيفرة تحيط بتعبير let، مثل:

fun x ->
  (let y = e1 in e2) (let z = e3 in e4)

لا ينبغي تعميم متغيّر النوع الخاص بـ x عند استنتاج نوع y أو z، لأن x يجب أن يكون له النوع نفسه في التعبيرات الفرعية الأربعة كلها، من e1 إلى e4. فالتعميم قد يسمح خطأً بأن يكون لـ x نوع في e1 وe2، ونوع مختلف في e3 وe4.

لذا نعمّم فقط المتغيّرات الموجودة فعلًا في u1 وغير الموجودة في env1. وبهذه الطريقة نعمّم فقط متغيّرات النوع الآتية من e1، لا المتغيّرات التي كانت أصلاً في البيئة عندما بدأنا استنتاج نوع تعبير let. ولنفترض أن تلك المتغيّرات هي 'a1 ... 'an. عندئذ يكون مخطط النوع الذي نعطيه لـ x هو 'a1 ... 'an . u1.

وبجمع ذلك كله، ننتهي إلى:

generalize(C1, env, x : t1) =
  env1, x : 'a1 ... 'an . u1

عودة إلى مثالنا مع دالة الهوية من قبل، كان لدينا generalize({}, {}, x : 'a -> 'a). وفي تلك الحالة البسيطة نوعًا ما، لا يكتشف unify أي مساويات جديدة من البيئة، لذا u1 = 'a -> 'a وenv1 = {}. ومتغيّر النوع الوحيد في u1 هو 'a، وهو لا يظهر في env1. لذا يُعمَّم 'a، فينتج 'a . 'a -> 'a بوصفه مخطط النوع لـ id.

10.6.6. تعدّد الأشكال والقابلية للتغيير

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

let succ = fun x -> ( + ) 1 x;;
let id = fun x -> x;;
let r = ref id;;
r := succ;;
!r true;;  (* error *)

من الواضح أنه ينبغي أن نستنتج succ : int -> int وid : 'a . 'a -> 'a. لكن ماذا ينبغي أن يكون نوع r؟ من المغري أن نقول إننا ينبغي أن نستنتج r : 'a . ('a -> 'a) ref. فهذا سيتيح لنا تجسيد نوع r ليكون (int -> int) ref في السطر 4 وتخزين succ في r. لكنه سيتيح لنا أيضًا تجسيد نوع r ليكون (bool -> bool) ref في السطر 5. وهذه كارثة: فهي تسبب تطبيق succ على true، وهو ما لا يضمن سلامة الأنواع.

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

# let id = fun x -> x;;
val id : 'a -> 'a = <fun>   (* as expected *)
# let r = ref id;;
val r : ('_weak1 -> '_weak1) ref = { ... }   (* what is _weak? *)
# r;;
- : ('_weak1 -> '_weak1) ref = { ... }   (* it's consistent at least *)
# r := succ;;
- : unit = ()
# r;;
- : (int -> int) ref = { ... }   (* did r just change type ?! *)

عندما يُستنتَج نوع r، يعطيه OCaml نوعًا يشمل متغيّر نوع ضعيفًا. وكل تلك المتغيّرات أسماؤها تبدأ بـ '_weak. ومتغيّر النوع الضعيف هو متغيّر لم يُعمَّم، ومن ثم لا يمكن تجسيده على أنواع متعددة. بل هو يدلّ على نوع واحد غير معروف بعد. فكّر فيه كما لو أن استدلال الأنواع لذلك المتغيّر لم ينتهِ بعد: فـ OCaml ينتظر مزيدًا من المعلومات ليحدّد بدقة ما هو. وعندما يُنفَّذ r := succ، تصبح تلك المعلومات متاحة أخيرًا. فيستنتج OCaml أن '_weak1 = int من نوع succ. ثم يستبدل OCaml '_weak1 بـ int في كل مكان. وهذا ما ينتج خطأً في السطر الأخير:

# !r true;;
Error: This expression has type bool but an expression was expected of type int

وبما أن r : (int -> int) ref، فلا يمكننا تطبيق !r على bool.

لن نتناول هنا تنفيذ متغيّرات النوع الضعيفة.

لكن دعنا لا نترك بعد موضوع التفاعل بين الأنواع متعدّدة الأشكال والقابلية للتغيير. قد يغريك أن تظن أنه ظاهرة تصيب OCaml وحدها. لكن Java نفسها تعاني منها فعلًا.

تأمّل التسلسل الهرمي للأصناف التالي:

class Animal { }
class Elephant extends Animal { }
class Rabbit extends Animal { }

افترض الآن أننا ننشئ مصفوفة من الحيوانات:

Animal[] a= new Rabbit[2]

نحن هنا نستخدم تعدّد أشكال الأنماط الفرعية (subtype polymorphism) لإسناد مصفوفة من كائنات Rabbit إلى مرجع Animal[]. وهذا ليس مثل تعدّد الأشكال المُعامَلي (parametric polymorphism) الذي استخدمناه في OCaml، لكنه مع ذلك تعدّد أشكال.

ماذا لو جرّبنا هذا؟

a[0]= new Elephant()

بما أن a منمّط كمصفوفة Animal، فمن المنطقي أن نستطيع إسناد كائن فيل إليها، تمامًا كما نستطيع إسناد كائن أرنب. وفي الواقع، هذه الشيفرة سليمة وفق مصرّف Java. لكن Java تعطينا خطأ وقت تشغيل إذا شغّلنا تلك الشيفرة!

Exception java.lang.ArrayStoreException

المشكلة أن تغيير العنصر الأول في المصفوفة ليكون أرنبًا سيتركنا بمصفوفة Rabbit أحد عناصرها Elephant. (آخ! سيجلس فيل على أرنب. مسكين الأرنوب.) لكن في Java، يُفترض أن يكون نوع كل كائن في مصفوفة خاصيةً للمصفوفة ككل. لذا يجب أن يكون كل عنصر في المصفوفة المنشأة بـ new Rabbit[2] من نوع Rabbit. لذلك تمنع Java الإسناد أعلاه باكتشاف الخطأ وقت التشغيل وإطلاق استثناء.

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

10.7. الملخّص

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

10.7.1. المصطلحات والمفاهيم

• الصياغة المجرّدة (abstract syntax)
• شجرة الصياغة المجرّدة (abstract syntax tree)
• الترابطية (associativity)
• الواجهة الخلفية (back end)
• صيغة باكوس-ناور (BNF)
• الخطوة الكبيرة (big step)
• الشيفرة البايتية (bytecode)
• النداء بالاسم (call by name)
• النداء بالقيمة (call by value)
• الاستبدال المانع للالتقاط (capture-avoiding substitution)
• الإغلاق (closure)
• المصرّف (compiler)
• الصياغة الملموسة (concrete syntax)
• القيد (constraint)
• القواعد غير السياقية (context-free grammar)
• اللغة غير السياقية (context-free language)
• إزالة السكر النحوي (desugaring)
• البيئة الديناميكية (dynamic environment)
• النطاق الديناميكي (dynamic scope)
• نموذج البيئة (environment model)
• التقييم (evaluation)
• طازج (fresh)
• الواجهة الأمامية (front end)
• التعميم (generalization)
• خوارزمية استدلال الأنواع لهيندلي–ميلنر (Hindley–Milner (HM))
• التنميط الضمني (implicit typing)
• التجسيد (instantiation)
• التمثيل الوسيط (intermediate representation)
• المفسّر (interpreter)
• حساب لامبدا (lambda calculus)
• تعدّد أشكال let (let polymorphism)
• المحلّل المعجمي (lexer)
• تهيئة الآلة (machine configuration)
• المتغيّر الفوقي (metavariable)
• الرمز غير الطرفي (nonterminal)
• الدلالات التشغيلية (operational semantics)
• المصرّف المُحسِّن (optimizing compiler)
• المحلّل النحوي (parser)
• الأولوية (precedence)
• متغيّر نوع أوّلي (preliminary type variable)
• الحفظ (preservation)
• عملية أولية (primitive operation)
• التقدّم (progress)
• الآلات ذات المكدّس (pushdown automata)
• التعبير النمطي (regular expression)
• اللغة النمطية (regular language)
• العلاقة (relation)
• التحليل الدلالي (semantic analysis)
• الدارات القصيرة (short circuit)
• الخطوة الصغيرة (small step)
• البرنامج المصدر (source program)
• النطاق الساكن (static scope)
• التنميط الساكن (static typing)
• عالق (stuck)
• الاستبدال (substitution)
• نموذج الاستبدال (substitution model)
• تعدّد أشكال الأنماط الفرعية (subtype polymorphism)
• الرمز (symbol)
• جدول الرموز (symbol table)
• البرنامج الهدف (target program)
• الرمز الطرفي (terminal)
• الوحدة المعجمية (token)
• التعليق النوعي (type annotation)
• فحص الأنواع (type checking)
• استدلال الأنواع (type inference)
• إعادة بناء الأنواع (type reconstruction)
• سلامة الأنواع (type safety)
• مخطط النوع (type scheme)
• نظام الأنواع (type system)
• متغيّر النوع (type variable)
• سياق التنميط (typing context)
• التوحيد (unification)
• الموحِّد (unifier)
• القيمة (value)
• قيد القيم (value restriction)
• الآلة الافتراضية (virtual machine)
• متغيّر النوع الضعيف (weak type variable)
• سليم الأنواع (well-typed)

10.7.2. قراءات إضافية

• Types and Programming Languages بقلم Benjamin C. Pierce، الفصول 1-14، 22.
• Modern Compiler Implementation (بلغة Java أو ML) بقلم Andrew W. Appel، الفصول 1-5.
• Automata and Computability بقلم Dexter C. Kozen، الفصول 1-27.
• يتضمن Real World OCaml فصلًا عن واجهة OCaml الأمامية.
• توثّق هذه الصفحة بعض التفاصيل الداخلية لفاحص الأنواع ومستنتج الأنواع في OCaml.
• تُوصَف آلة OCaml الافتراضية المعروفة بآلة Zinc في هاتين الورقتين: 1، 2.

10.7.3. شكر وتقدير

معالجتنا لاستدلال الأنواع مبنية على Pierce.

  7+5*2
-->  (step * operation)
  7+10
-->  (step + operation)
  17

(e1, e2) --> (e1', e2)
  if e1 --> e1'

(v1, e2) --> (v1, e2')
  if e2 --> e2'

(e1, e2) ==> (v1, v2)
  if e1 ==> v1
  and e2 ==> v2

p ::= i | (p1, p2) | Left p | Right p | x | _

e ::= ...
    | match e with | p1 -> e1 | p2 -> e2 | ... | pn -> en

v =~ p // s

v =~ p // s
  if v = p s

2 =~ x // {2/x}
  because 2 = x{2/x}

(* This rule should implement evaluation of e. *)
match e with | p1 -> e1 | p2 -> e2 | ... | pn -> en
--> ???
  if ???

(* This rule implements moving past p1 to the next pattern. *)
match v with | p1 -> e1 | p2 -> e2 | ... | pn -> en
--> match v with | p2 -> e2 | ... | pn -> en
  if there does not exist an s such that ???

(* This rule implements matching v with p1 then proceeding to evaluate e1. *)
match v with | p1 -> e1 | p2 -> e2 | ... | pn -> en
--> ??? (* something involving e1 *)
  if ???

match v with |  -/->

let x = v in e --> e{v/x}

let rec x = v in e --> e{v/x}   (* broken *)

  let rec fact = fun x ->
    if x <= 1 then 1 else x * (fact (x - 1)) in
  fact 3

-->

  (fun x -> if x <= 1 then 1 else x * (fact (x - 1)) 3

-->

  if 3 <= 1 then 1 else 3 * (fact (3 - 1))

-->

  3 * (fact (3 - 1))

-->

  3 * (fact 2)

-/->

e ::= ...
    | rec f -> e

rec f -> e  -->  e{(rec f -> e)/f}

  rec f -> f

-->  (* step rec *)

  f{(rec f -> f)/f}

= (* substitute *)

  rec f -> f

--> (* step rec *)

  f{(rec f -> f)/f}

...

let rec f = e1 in e2

let f = rec f -> e1 in e2

let fact = rec fact -> fun x ->
  if x <= 1 then 1 else x * (fact (x - 1)) in
fact 3

let rec fact = fun x ->
  if x <= 1 then 1 else x * (fact (x - 1)) in
fact 3

(rec f -> e){v/x} = rec f -> e{v/x}
  if x <> f
  and f not in FV(v)

(rec f -> e){v/f} = rec f -> e

<{}, (3 + 5) * 2> ==> 16          (op rule)
    because <{}, (3 + 5)> ==> 8   (op rule)
        because <{}, 3> ==> 3     (int const rule)
        and     <{}, 5> ==> 5     (int const rule)
        and 3+5 is 8
    and <{}, 2> ==> 2             (int const rule)
    and 8*2 is 16

let x = 5 in
let f y = x + y in
let x = 4 in
f 3

let x = 5 in
let f y = x + y in
let g x = f x in
let x = 4 in
g 3

let f y = x + y in
let x = 3 in
let y = 4 in
f 2

1. fun x -> ( + ) 1 x
2. fun b -> if b then false else true
3. fun x -> fun y -> if x <= y then y else x

X = int
Y = X -> X

X -> Y = Y -> Z
     Z = U -> W

let apply f x = f x

let double f x = f (f x)

let s x y z = (x z) (y z)