خوارزمية هيندلي ميلنر:باستخدام الأنواع لضمان تطبيق الارتباطات

Question

أقوم بتنفيذ خوارزمية الاستدلال من النوع Hindley-Milner، باتباع البرامج التعليمية الخاصة بـ مارك جونز و أوليغ كيسيليوف.كلاهما لهما عملية "تطبيق الارتباطات" بنوع النموذج تقريبًا

applyBindings :: TyEnv -> Type -> Type

الذي يطبق tyvar -> ty الارتباطات في TyEnv إلى المعطى Type.لقد وجدت أنه من الخطأ الشائع في الكود الخاص بي أن أنسى الاتصال applyBindings, ، ولم أحصل على أي مساعدة من نظام كتابة هاسكل منذ ذلك الحين ty لديه نفس النوع كما applyBindings tyenv ty.أنا أبحث عن طريقة لفرض المتغير التالي في نظام الكتابة:

عند القيام باستدلال النوع، يجب تطبيق الارتباطات قبل إرجاع النتيجة "النهائية".

عند إجراء الاستدلال النوعي للغة كائن أحادية الشكل، توجد طريقة طبيعية لفرض ذلك، كما تم تنفيذها في نظرية Wren ng thornton حزمة التوحيد-FD:نحدد نوعين من البيانات لـ Typeس:

-- | Types not containing unification variables
type Type = ...          -- (Fix TypeF) in wren's package

-- | Types possibly containing unification variables
type MutType = ...       -- (MutTerm IntVar TypeF) in wren's package

وتعطي applyBindings نوع

-- | Apply all bindings, returning Nothing if there are still free variables
-- otherwise just
applyBindings :: TyEnv -> MutType -> Maybe Type

(هذه الوظيفة في الواقع freeze . applyBindings في التوحيد-FD).وهذا يفرض ثوابتنا - إذا نسينا ذلك applyBindings, ، فسنحصل على خطأ في النوع.

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

هل هناك حل على غرار ما أصفه، أي.واحد الذي يعطي applyBindings نوع مختلف عن const id؟هل يستخدم المترجمون الحقيقيون نفس الكلمات (بين متغيرات التوحيد ومتغيرات نوع لغة الكائن) التي تستخدمها البرامج التعليمية لمارك وأوليج؟

Answer 1

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

• يجب أن يكون مدقق النوع الخاص بك مختلف تمثيلات ل متغيرات نوع التوحيد و متغيرات نوع لغة الكائن.

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