أنواع التبعية - مستقبل لغات البرمجة

مرحبا بالجميع!

على الرغم من الغرابة وبعض التجريد من الموضوع الذي تم النظر فيه اليوم - نأمل أن يتمكن من تنويع عطلة نهاية الأسبوع. في نهاية المنشور ، نضع ثلاثة روابط من المؤلف ، مما يتيح لك التعرف على الكتابة التابعة في Idris و F * و JavaScript

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

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

عالم الأنواع

الكتابة هي واحدة من تلك الأشياء التي لا يمكن فصلها عن تفكيرنا لدرجة أننا بالكاد نفكر في مفهوم الأنواع على هذا النحو؟ لماذا 1 int ، ولكن إذا وضعت هذه القيمة بين علامتي اقتباس - وتتحول إلى string ؟ ما هو "النوع" في جوهره؟ كما هو الحال غالبًا في البرمجة ، تعتمد الإجابة على صياغة السؤال.

أنواع متنوعة. في بعض أنظمة الكتابة ، توجد حدود واضحة للغاية بين الأنواع والقيم. لذلك ، 3 و 2 و 1 قيم integer ، ولكن integer ليس قيمة. هذا البناء "مضمن" في اللغة ويختلف اختلافًا جوهريًا عن المعنى. لكن ، في الواقع ، هذا الاختلاف ليس ضروريًا ويمكن أن يحدنا فقط.

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

 if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") } 

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

 if typeof(user) == User { print("Well, it's a user. That's all I know") } 

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

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

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

الرياضيات في الاستوديو!

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

 1 + 2 + 3 + ... + x = x * (x + 1) / 2 

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

1. ويلاحظ هذا البيان لليوم الأول. (عادة ما يكون 0 أو 1)
2. إذا كانت هذه العبارة صحيحة للرقم n ، فسيكون صحيحًا للرقم التالي n + 1

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

لإثبات أن هذا ليس بالأمر الصعب:

 1 = 1 * (1 + 1) / 2 1 = 1 

الآن علينا أيضًا أن نثبت أن البيان ينطبق على جميع الأرقام الأخرى. للقيام بذلك ، افترض أنه يعمل مع عدد n ، ثم تأكد من أنه يعمل مع n + 1 أيضًا.

بافتراض أن التعبير التالي صحيح:

 1 + 2 + 3 + ... + n = n * (n + 1) / 2 

تحقق منه لمعرفة n + 1 :

 (1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2 

وبالتالي ، يمكننا استبدال "(1 + 2 + 3 + ... + n)" بالمساواة أعلاه:

 (n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2) 

وتبسيط ل

 (n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1) 

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

يكمن جمال هذا النهج في حقيقة أنه يمكن إصدار أي دليل رياضي في شكل برنامج كمبيوتر - وهذا ما نحتاج إليه!

العودة إلى البرمجة

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

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

 append: (arr1: Array, arr2: Array) -> Array 

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

 newArray = append([1], [2, 3]) assert(length(newArray) == 3) 

ولكن لماذا تحقق من ذلك في وقت التشغيل إذا كنت تستطيع إنشاء قيد سيتم فحصه في وقت الترجمة:

 append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2) 

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

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

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

بعد القيام بذلك ، يمكنك إنشاء أنواع منفصلة للصفائف التي تحتوي على 1 و 2 و 3 وعددًا مختلفًا من العناصر. ArrayOfOne ، ArrayOfTwo ، إلخ.

وبالتالي ، يمكنك تحديد دالة الطول ، والتي ستأخذ أحد أنواع الصفيف أعلاه ولديك نوع إرجاع تابع من النوع One لـ ArrayOfOne ، Two لـ ArrayOfTwo ، إلخ. لكل رقم.

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

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

لنفترض أننا نريد إنشاء متغير من النوع ArrayOfThree :

 result: ArrayOfThree = append([1], [2, 3]) 

يمكن للمترجم تحديد أن [1] له قيمة واحدة فقط ، لذلك يمكنك تعيين النوع ArrayOfOne . يمكن أيضًا تعيين ArrayOfTwo إلى [2 ، 3].

يعرف المحول البرمجي أن نوع النتيجة يجب أن يكون مساويًا لمجموع أنواع الوسيطة الأولى والثانية. يعرف أيضًا أن ArrayOfOne + ArrayOfTwo يساوي ArrayOfThree ، أي أنه يعرف أن التعبير بالكامل على الجانب الأيمن من الهوية هو من النوع ArrayOfThree. يطابق التعبير على اليسار ، ويسر المترجم.

إذا كتبنا ما يلي:

 result: ArrayOfTwo = append([1], [2, 3]) 

عندها سيكون المحول البرمجي غير راضٍ تمامًا ، لأنه سيعرف أن النوع غير صحيح.

الكتابة التابعة رائعة جدا

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

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

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

أعتقد أن الكتابة المعتمدة هي مستقبل لغات البرمجة السائدة ، ولا يمكنني الانتظار حتى ننتظرها!

→ ادريس

→ F *

→ إضافة أنواع تابعة لجافا سكريبت