لغة البرمجة ML

📅 آخر تحديث: ١٩ يوليو ٢٠٢٦
✍️ نُشر في: ١٩ يوليو ٢٠٢٦
الموسوعة الحرة

لغة ML (اللغة الوصفية) هي لغة وصفية طُوِّرت لبرنامج إثبات النظريات LCF في إدنبرة خلال سبعينيات القرن العشرين. وهي لغة وظيفية مبكرة ذات كتابة ثابتة ، تتميز باستنتاج أنواع متعددة الأشكال على نمط هيندلي-ميلنر ، بالإضافة إلى ميزات أخرى مثل الاستثناءات والمتغيرات القابلة للتغيير . [ 1 ] وقد ألهم تصميم ML في LCF بشكل مباشر عائلة لغات ML اللاحقة (ولا سيما Standard ML و Caml ومشتقاتهما)، كما أثر على تطوير اللغات الوظيفية اللاحقة. [ 4 ]

تاريخ

بدأ روبن ميلنر تطوير لغة ML عند وصوله إلى جامعة إدنبرة عام 1973، بمساعدة مساعدي البحث لوكوود موريس ومالكولم نيوي، وكلاهما باحثان ما بعد الدكتوراه من جامعة ستانفورد، واللذان وظفهما ميلنر. [ 5 ] انضم مايكل جوردون وكريستوفر وادزورث وطلاب دراسات عليا آخرون إلى البحث بحلول عام 1975. [ 4 ] تاريخيًا، صُممت لغة ML لتطوير أساليب البرهان في مُثبت نظريات LCF ، ولتخلف الإصدار السابق Stanford LCF ، في محاولة لحل المشكلات المتعلقة باستخدام المساحة وقابلية توسيع البرهان. عملت ML كلغة وصفية (ومن هنا جاء الاسم) ولغة أوامر ( REPL ) لنظام LCF . أما لغة PPLAMBDA ، وهي لغة كانت من الناحية المفاهيمية مزيجًا من حساب التفاضل والتكامل من الدرجة الأولى وحساب التفاضل والتكامل متعدد الأشكال ذي النوع البسيط ، فكانت اللغة الأساسية التي بُنيت بها عبارات النظريات بشكل مباشر. [ 1 ]

أثناء تطوير لغة ML، كتب ميلنر ورقة بحثية بعنوان "نظرية تعدد أشكال الأنواع في البرمجة" عام 1978، والتي شرح فيها مفهوم "البرنامج ذي الأنواع الجيدة" في سياق نظام أنواع متعدد الأشكال (عام). استخدم ميلنر لغة ML كدراسة حالة لتطبيق النظريات التي طورها، وأشار إلى التحديات النظرية التي ظهرت أثناء التطوير والتي لم تُحل بعد. [ 6 ] تم الانتهاء من تصميم النسخة الأولى من ML، ووُثِّق لاحقًا في كتاب "Edinburgh LCF" الصادر عام 1979، من تأليف ميلنر بالاشتراك مع جوردون ووادزورث. [ 5 ] [ 1 ]

بعد تأسيس لغة إدنبرة LCF ونشرها تحت الاسم نفسه، ازداد الاهتمام بها، وبدأ العديد من الأطراف العمل على تطوير تطبيقات لها، مع بعض التعديلات الطفيفة في التصميم والميزات. أنشأ لوكا كارديلي لغة Cardelli ML ، أو VAX ML ، التي تطورت لاحقًا إلى لهجة مستقلة مناسبة للحوسبة العامة، وتم تحديدها في ورقة ML تحت نظام يونكس . [ 7 ] [ 4 ] بدأ جيرار هويه في معهد Inria بنقل الشفرة المصدرية من لغة Stanford Lisp إلى لهجات أخرى مختلفة من لغة Lisp ضمن مشروع "Project Formel". ثم قام لاري بولسون بتطوير نسخة Franz Lisp ، والتي أُطلق عليها لاحقًا اسم Cambridge LCF . [ 8 ] تم تحديث هذه النسخة من LCF لاحقًا لاستخدام إصدار مبكر من Standard ML ، وتم تحميلها على GitHub . [ 9 ]

مع الاهتمام والحماس اللذين أثيرا حول لغة ML وLCF والتقنيات الأخرى ذات الصلة آنذاك، مثل لغة البرمجة Hope ، التي ظهرت بعد إصدار Edinburgh LCF والتطورات الأخرى في ذلك الوقت، عُقد اجتماع بعنوان "ML وLCF وHope" في نوفمبر 1982. وأُثيرت خلال هذا الاجتماع مخاوف بشأن تشتت كل من التصميم والتنفيذ، مما يؤدي إلى ازدواجية العمل. ورغم أن ميلنر بدا منفتحًا على روح التجريب في الاجتماع، فقد جرت مناقشات واجتماعات أخرى بين برنارد سوفرين وميلنر، حيث حث سوفرين ميلنر على توحيد تصميم ML. وقد أشير إلى هذه المراسلات لاحقًا في المسودة الثانية لاقتراح ميلنر لمعيار ML. [ 4 ]

ملخص

يمكن تتبع أبرز مصادر الإلهام لبنية لغة ML إلى لغة ISWIM ، التي وُصفت بأنها " حساب لامدا مع تبسيط نحوي". [ 4 ] صُممت ML بنظام أنواع ثابت قوي يسمح للمستخدم بتعريف أنواع مجردة بتعدد أشكال بارامتري ، ويتم التحقق من ذلك أثناء الترجمة. [ 1 ] كما أنها تتميز باستنتاج تلقائي للأنواع، مما منحها سهولة استخدام اللغات الديناميكية في ذلك الوقت مثل Lisp أو POP-2، وذلك بالاستغناء عن الحاجة إلى تحديد الأنواع بشكل صريح. [ 4 ]

أمثلة

الأمثلة التالية مستمدة بشكل وثيق من إطار عمل إدنبرة لتنسيق اللغات (LCF) ، وهي تُقدم لمحة عامة عن بنية وخصائص لغة ML. #يشير الحرف في بداية السطر إلى مُدخلات المستخدم، بينما تُمثل الأسطر التي لا تحتوي عليه استجابات النظام التي تُظهر القيمة ونوعها المُستنتج. تجدر الإشارة إلى أن هذا القسم لا يُقصد به أن يكون مجموعة شاملة لخصائص لغة ML، بل هو جزء منها لإعطاء فكرة عامة عن اللغة. يُرجى الرجوع إلى إطار عمل إدنبرة لتنسيق اللغات (LCF) للحصول على تعريف أكثر دقة. [ 1 ]

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

#2+3;; 5 : عدد صحيح #let x = it;; x = 5 : عدد صحيح #let y = 2*5 and z = 7;; y = 10 : عدد صحيح z = 7 : عدد صحيح #let x,y,z = y,x,2;; x = 10 : عدد صحيح y = 5 : عدد صحيح z = 2 : عدد صحيح

تُعرَّف الدوال باستخدام let`. تطبيق الدالة له أولوية أعلى من المعاملات الرياضية، لذا f 3 + 4فإن ` (f 3) + 4. الدوال المُعرَّفة بمعاملات متعددة تُطبَّق بشكل جزئي ، لذا فإن تمرير معامل واحد إلى الدالة سيُعيد دالة تقبل المعامل الثاني، وهكذا. تتطلب الدوال التكرارية `، letrecلذا فإن اسم الدالة يكون ضمن نطاق جسمها. صيغة الدالة المجهولة مشابهة لحساب لامدا، حيث `.` \لـ `lambda` و`.` .لفصل الوسائط عن التعبير.

#لنجمع xy = x+y;; أضف = - : (عدد صحيح -> (عدد صحيح -> عدد صحيح)) #أضف 3;; - : (int -> int) #جلسة 4;; 7 : عدد صحيح #letrec fact n = if n = 0 then 1 else n * fact(n-1);; حقيقة = - : (عدد صحيح -> عدد صحيح) #حقيقة 4;; 24 : عدد صحيح #(\x.x+1) 3;; 4 : عدد صحيح

تستخدم القوائم الفواصل المنقوطة بين عناصرها. hdو tlهي دوال مدمجة تُرجع رأس القائمة وذيلها؛ .و هي دالة cons (إضافة عنصر في البداية)؛ @و هي دالة append. الدوال مثل hdهذه متعددة الأشكال - يستخدم ML متغيرات أنواع عامة ( *، **، إلخ) للتعبير عن ذلك:

#let m = [1;2;3;4];; m = [1; 2; 3; 4] : (قائمة أعداد صحيحة) #shd m, tl m;; 1، [2؛ 3؛ 4] : (عدد صحيح # (قائمة أعداد صحيحة)) #0.م @ [5;6];; [0; 1; 2; 3; 4; 5; 6] : (قائمة أعداد صحيحة) #hd;; - : ((* قائمة) -> *) #map (\xx*x) [1;2;3;4];; [1; 4; 9; 16] : (قائمة أعداد صحيحة)

يتم تعريف المتغيرات القابلة للتغييرletref باستخدام `var` ويتم تحديثها باستخدام `var` :=. loopتنتمي الكلمة المفتاحية `var` إلى بنية حلقة `if-then`، والتي تتكرر في كل مرة ifيفشل فيها الشرط:

#ليت الحقيقة ن = # letref count = n and result = 1 # في حالة العد = 0 ثم النتيجة # عدد مرات التكرار، النتيجة := العدد - 1، العدد * النتيجة؛ حقيقة = - : (عدد صحيح -> عدد صحيح) #حقيقة 4;; 24 : عدد صحيح

الرموز هي نوع سلسلة نصية في لغة ML، مفصولة بعلامة `; تُستخدم علامات التنصيص المزدوجة لإنشاء قوائم الرموز. كان من الاستخدامات الشائعة للرموز تحديد حالات الفشل باستخدام failwith، وهي كلمة مفتاحية تُستخدم لرفع استثناءات مع رمز صريح، ?وتُستخدم لمعالجتها.

#`هذا رمز`;; `هذا رمز مميز` : tok #``هذه قائمة رموز``;; [`this`; `is`; `a`; `token`; `list`] : (tok list) #لنفترض أن نصف ن = # إذا كانت قيمة n تساوي صفرًا، فافشل مع `صفر` وإلا فليكن m = n/2 # في حالة n = 2*m فإن m وإلا فإن failwith `odd`;; نصف = - : (عدد صحيح -> عدد صحيح) النصف 4؛ 2 : عدد صحيح النصف 3؛ فشل التقييم (فردي) نصف 3 ؟ 0;; 0 : عدد صحيح

تُعرَّف الأنواع المجردة باستخدام `<type>` abstype، مما يُنشئ نوعًا جديدًا ويُحدد الدوال التي تعمل معه، مع إخفاء البنية الداخلية (النوع الملموس الذي بُني منه). تُعرَّف الأنواع المجردة المتكررة باستخدام `<type>` absrectype، مما يسمح باستخدام النوع في تعريفه الخاص. توجد كلمة مفتاحية مشابهة `<type>` lettype، تُستخدم لتعريف أسماء بديلة للأنواع الأساسية . إليك مثال على نوع مجرد متكرر يُعرّف شجرة ثنائية مع بعض العمليات الأساسية:

#absrectype (*, **) tree = * + ** # (*, **) tree # (*, **) tree # مع tiptree x = abstree(inl x) # و comptree (y, t1, t2) = abstree(inr(y, t1, t2)) # و istip t = isl(reptree t) # و tipof t = outl(reptree t) ? failwith `tipof` # و labelof t = fst(outr(reptree t)) ? failwith `labelof` # و sonsof t = snd(outr(reptree t)) ? failwith `sonsof`;; tiptree = - : (* -> (*, **) tree) comptree = - : ((** # (*, **) tree # (*, **) tree) -> (*, **) tree) istip = - : ((*, **) tree -> bool) tipof = - : ((*, **) tree -> *) labelof = - : ((*, **) tree -> **) أبناء = - : ((*, **) شجرة -> ((*, **) شجرة # (*, **) شجرة))

داخل تعريفات العمليات ( withالكتلة)، يمكن إضافة بادئة إلى اسم النوع absلتغليف القيم داخل النوع، و لفكrep تغليفها. تشير الأحرف +في #تعريفات الأنواع إلى أنواع الجمع (الاتحادات الموسومة) وأنواع الضرب (الصفوف)، على التوالي، مع #أولوية أعلى للأولى.

وفرت مكتبة ML على LCF عدة دوال مساعدة مستخدمة في المثال أعلاه. عند العمل على أنواع الجمع +، تقوم الدالتان inlو inrبحقن القيم في الجانب الأيسر أو الأيمن من نوع الجمع. outlتستخرج الدالة القيم من الحقن الأيسر (وتفشل إذا تم إدخال حقن أيمن)، بينما outrتستخرج الدالة القيم من الحقن الأيمن (وتفشل إذا تم إدخال حقن أيسر). بالنسبة لأنواع الضرب #، فإن دالتي الاستخراج و هما fstو snd، اللتان تستخرجان المكونين الأول والثاني من الزوج. يتم إنشاء أنواع الضرب باستخدام عامل الفاصلة الوسطي. في مثال الشجرة أعلاه، comptreeتأخذ الدالة مُعاملًا واحدًا وهو نمط الزوج (y, t1, t2)، والذي يقوم بتفكيك الزوج إلى مكوناته الثلاثة.

انظر أيضاً

مراجع

  1. 1 2 3 4 5 6 غوردون، م.؛ ميلنر، ر.؛ وادزورث، س. ب. (1979). إدنبرة LCF: منطق آلي للحوسبة . سلسلة محاضرات في علوم الحاسوب. برلين، هايدلبرغ: سبرينغر برلين هايدلبرغ. doi : 10.1007/3-540-09724-4 . ISBN 978-3-540-09724-2.
  2. ↑ تيت، بروس؛ ديز، إيان؛ داود، فريدريك؛ موفيت، جاك (18 نوفمبر 2014). سبع لغات أخرى في سبعة أسابيع: لغات تُشكّل المستقبل . المبرمجون العمليون ( الطبعة P1.0). دالاس: مكتبة براغماتيك. ص 97، 101. ISBN   978-1-941222-15-7أميل إلى القول بأن " Elm هي لغة من عائلة ML" للوصول إلى التراث المشترك لجميع هذه اللغات [Haskell و OCaml و SML و F#].
  3. ↑ لغة برمجة لـ"قوات خاصة" من المطورين ، شبكة تطوير البرمجيات الروسية: فريق مشروع نيميرلي ، تم الاطلاع عليه في 24 يناير 2021
  4. 1 2 3 4 5 6 ماكوين، ديفيد؛ هاربر، روبرت؛ ريبي، جون (14 يونيو 2020). "تاريخ لغة Standard ML" . وقائع مؤتمر ACM حول لغات البرمجة . 4 (HOPL): 1-100 . doi : 10.1145/3386336 . ISSN 2475-1421 . 
  5. 1 2 غوردون، مايكل جيه سي (1996). "من كلية لندن للأزياء إلى جامعة لندن: تاريخ موجز" . تم الاسترجاع في 11-10-2007 .
  6. ↑ ميلنر، روبن (ديسمبر 1978). "نظرية تعدد الأشكال في البرمجة" . مجلة علوم الحاسوب والنظم . 17 (3): 348-375 . doi : 10.1016/0022-0000(78)90014-4 .
  7. ↑ كارديلي، لوكا (1983). "ML تحت يونكس" (ملف PDF) . مؤرشف من الأصل (ملف PDF) في 12 نوفمبر 2025. تم الاطلاع عليه في 25 يناير 2025 .
  8. ↑ غوردون، مايكل جيه سي (1988)، بيرتويستل، غراهام؛ سوبرامانيام، بي إيه (محررون)، "HOL: نظام توليد البراهين لمنطق الرتبة العليا" ، مواصفات VLSI، والتحقق منها، وتوليفها ، المجلد 35، بوسطن، ماساتشوستس: سبرينغر الولايات المتحدة، الصفحات 73-128 ، doi : 10.1007/978-1-4613-2007-4_3 ، ISBN   978-1-4612-9197-8تم الاطلاع عليه بتاريخ 2026-01-03{{citation}}: CS1 maint: work parameter with ISBN ( link )
  9. ^ كولهاس ، مايكل (11/05/2024)، كوهلهاس / كامبريدجLCF ، استرجاعها 2026/01/03

للمزيد من القراءة

  • كريستوف كريتز، فينسنت راهلي، مقدمة في لغة ML الكلاسيكية ( مؤرشفة في 8 يوليو 2024 )، جامعة كورنيل، أكتوبر 2011. ملاحظات محاضرة حول لهجة من لغة ML قريبة في روحها من LCF/ML .
  • لوكا كارديلي، أوراق بحثية ( مؤرشفة في 25 يناير 2026 )، جامعة أكسفورد. قائمة بالأوراق البحثية المتعلقة بتطوير Cardelli ML/ML تحت VMS/ML تحت نظام يونكس.