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

نقدم منهجًا لإثراء نظام الأنواع في ML بشكل معتمد من أنواع معتمدة مقيدة، حيث يتم استمداد كائنات فهرس النوع من مجال قياسي C، مما يؤدي إلى مخطط لغة DML(C). هذا يسمح بتحديد واستنتاج معلومات نوعية أكثر دقة بشكل كبير، مما يسهل اكتشاف أخطاء البرنامج وتحسين المترجم. إحدى التعقيدات الرئيسية الناتجة عن إدخال الأنواع المعتمدة هي أن الاستنتاج النقي للنوع في النظام المعزز لم يعد ممكنًا، ولكننا نوضح أن التحقق من النوع لبرنامج معلق بما فيه الكفاية في DML(C) يمكن أن يتم اختزاله إلى تحقيق القيود في المجال القياسي C. نحن نعرض عدم تدخّل منهجنا من خلال أمثلة عملية ونثبت أن DML(C) محافظ على ML. تكمن المساهمة الرئيسية في البحث في تصميم لغتنا، بما في ذلك صياغة قواعد التحقق من النوع التي تجعل المنهج عمليًا. حسب علمنا، لم يجمع أي نظام أنواع سابق للغة برمجة عامة مثل ML الأنواع المعتمدة مع ميزات تتضمن إعلانات عن نوع البيانات، الوظائف من الدرجة الأعلى، التكرارات العامة، بوليمورفية let، المراجع القابلة للتغيير، والاستثناءات. بالإضافة إلى ذلك، أكملنا تنفيذ نموذج أولي لـ DML(C) لمجال قيود صحيحة، حيث تكون القيود من عدم المساواة الخطية (Xi وPfenning 1998).