हिंडली-मिलनर एल्गोरिदम: बाइंडिंग को लागू करने के लिए प्रकारों का उपयोग

Question

मैं Mark Jones और Oleg Kiselyov के ट्यूटोरियल के बाद, हिंडली-मिलनर प्रकार अनुमान एल्गोरिदम लागू कर रहा हूं। इन दोनों के रूप

applyBindings :: TyEnv -> Type -> Type 

दिया Type को TyEnv में tyvar -> ty बाइंडिंग लागू होता है जो मोटे तौर पर एक प्रकार के साथ एक "बाइंडिंग लागू" आपरेशन किया है। मुझे applyBindings पर कॉल करना भूलने के लिए मेरे कोड में यह एक आम गलती मिली है, और मुझे ty के समान प्रकार applyBindings tyenv ty के समान है, इसलिए मुझे हास्केल के प्रकार सिस्टम से कोई मदद नहीं मिली है।

जब प्रकार निष्कर्ष कर रही है, बाइंडिंग एक 'अंतिम' परिणाम

लौटने जब एक के लिए प्रकार निष्कर्ष करने से पहले लागू किया जाना चाहिए: मैं एक तरह से प्रकार प्रणाली में निम्नलिखित अपरिवर्तनीय लागू करने के लिए देख रहा हूँ monomorphic वस्तु भाषा, वहाँ एक प्राकृतिक तरीके इस लागू करने के लिए है में लागू किया रेन एनजी थार्नटन की unification-fd package:

-- | 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 

औरदे: हम Type रों के लिए दो डेटाटाइप्स को परिभाषितप्रकार

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

(इस समारोह वास्तव में freeze . applyBindings एकीकरण-fd में है)। यह हमारे invariant को लागू करता है - अगर हम applyBindings भूल जाते हैं, तो हमें एक प्रकार की त्रुटि मिल जाएगी।

यह एक तरह का समाधान है जिसे मैं ढूंढ रहा हूं, लेकिन ऑब्जेक्ट भाषाओं के लिए बहुरूपता के साथ। उपर्युक्त दृष्टिकोण, जैसा कि यह खड़ा है, लागू नहीं होता है, क्योंकि हमारे ऑब्जेक्ट-भाषा प्रकारों में प्रकार चर हो सकते हैं - वास्तव में, यदि बाइंडिंग लागू करने के बाद कोई चर मुक्त है, तो हम Nothing वापस नहीं करना चाहते हैं, लेकिन हम सामान्य बनाना चाहते हैं इन चरों पर।

क्या मेरे द्वारा वर्णित लाइनों के साथ कोई समाधान है, यानी applyBindingsconst id से एक अलग प्रकार देता है? असली कंपाइलर्स एक ही पनिंग (एकीकरण चर और ऑब्जेक्ट-भाषा प्रकार चर के बीच) का उपयोग करते हैं जो मार्क और ओलेग के ट्यूटोरियल करते हैं?

Answer 1

मैं यहाँ है, क्योंकि मुझे लगता है कि समाधान आप का प्रस्ताव के साथ अन्य समस्याओं हो सकता है अंधेरे में एक चाकू ले जा रहा हूँ, लेकिन मैं कम से कम एक कठिनाई को कर सकते हैं:

• आपका प्रकार चेकर होना चाहिए विभिन्नएकीकरण प्रकार चर और ऑब्जेक्ट-भाषा प्रकार चर के लिए प्रतिनिधित्व।

इस भिन्नता को लागू करने के लिए मुश्किल नहीं है, और वास्तव में मुझे लगता है कि GHC प्रकार चेकर इस तरह से काम किया है, कम से कम एक समय में। आप पेपर Practical Type Inference for Arbitrary-Rank Types पेपर देखना चाहेंगे; परिशिष्ट में बहुत उपयोगी कोड है।