तो, आप अभी भी Hindley-Milner को नहीं समझते हैं? भाग ३

भाग 2 में, हमने उन सभी औपचारिक शब्दों और प्रतीकों की परिभाषाओं के साथ समाप्त किया , जिन्हें आप स्टेकऑवरफ्लो प्रश्न में हिंडले-मिलनर एल्गोरिथम के बारे में देख सकते हैं। तो अब हम अनुवाद करने के लिए तैयार हैं जो वहाँ पूछा जा रहा है, अर्थात्, प्रकार के अनुमान के बारे में कथन प्राप्त करने के नियम। चलो शुरू हो जाओ!

प्रकार के निष्कर्ष बयानों को प्राप्त करने के लिए नियम

[वार]



यह निम्नानुसार अनुवाद करता है: यदि " x प्रकार का है" हमारे पदों के संग्रह से एक स्थिति है, तो ded से आप यह घटा सकते हैं कि x टाइप: का है। यहाँ x एक चर है (इसलिए नियम का नाम)। हां, यह स्पष्ट रूप से स्पष्ट लगता है, लेकिन इसमें गहरे और जटिल तथ्य संक्षिप्त और संक्षिप्त रूप में होते हैं जिन्हें मशीन समझ सकती है। यह आपको प्रकार के आक्षेप को स्वचालित करने की अनुमति देता है।

[ऐप]



यह निम्नानुसार अनुवाद करता है: यदि हम यह घटा सकते हैं कि e ₀ प्रकार की अभिव्यक्ति है as → τ: (यानी, e ₀₎ एक अनाम फ़ंक्शन हो सकता है, जो accordance के अनुसार, इनपुट के प्रकार type का मान लेता है और प्रकार का मान लौटाता है। τ type), और वह e ₁ प्रकार, का है, तो हम यह निष्कर्ष निकाल सकते हैं कि e ₀ ( e ₁ ) - e ₀ से e ₁ लागू करने से प्राप्त अभिव्यक्ति τ, की है । एक सहज बिंदु: यदि हम फ़ंक्शन के इनपुट और आउटपुट के प्रकार को कम कर सकते हैं, साथ ही तथ्य यह है कि कुछ अभिव्यक्ति का इनपुट के समान प्रकार है, तो जब हम फ़ंक्शन को इस अभिव्यक्ति पर लागू करते हैं, तो हम सुरक्षित रूप से निष्कर्ष निकाल सकते हैं कि परिणाम अभिव्यक्ति में फ़ंक्शन आउटपुट का प्रकार होगा। यहाँ कुछ भी भ्रमित नहीं है।

[पेट]



यह निम्नानुसार अनुवाद करता है: यदि हम मान सकते हैं कि x प्रकार: का है और e प्रकार ′: का है , तो हम यह निष्कर्ष निकाल सकते हैं कि हम चर x संबंध में e के अमूर्तन / λx.e - λx.e यह τ → τ τ होगा। उदाहरण के लिए, अगर हम जानते हैं कि टाइप x String , तो एक्सप्रेशन x[0] टाइप Char । अब [Abs] हमें यह निष्कर्ष निकालने की अनुमति देता है:

 function(x) { return x[0]; } 

String प्रकार → Char ।

की तरफ। मैंने पहले ही पॉलीटाइप्स का उल्लेख किया है। आइए इस उदाहरण में उनके पास वापस जाएं, बस इस अवधारणा को मेरे दिमाग में बेहतर बनाने के लिए। तो, आपने पहले ही देखा कि ऊपर का फ़ंक्शन Array[Int] → Int । वास्तव में, किसी भी प्रकार t फ़ंक्शन Array[t] → t । तो वास्तव में, इसके कई अलग-अलग प्रकार हैं, और String → Char उनमें से सिर्फ एक है। प्रत्येक प्रकार के Array[t] → t एक मोनोटाइप है। हम यह कह सकते हैं कि यह फ़ंक्शन इन सभी मोनोटाइप को रखता है, बस यह कहते हुए कि इसमें बहुपद this t(Array[t] → t) । यह पढ़ता है: "किसी भी t - प्रकार Array[t] → t " है, और हम एक ही प्रकार (हालांकि अधिक सार) द्वारा सब कुछ का एक गुच्छा निरूपित करते हैं। इसलिए, ध्यान दें कि जब हम अभिव्यक्ति के प्रकार को घटाते हैं, तो इसका मतलब यह नहीं है कि यह इस अभिव्यक्ति के लिए एकमात्र है। इसके कई अलग-अलग प्रकार हो सकते हैं, जिनमें से कुछ अधिक विशिष्ट होंगे, जबकि अन्य अधिक सार होंगे। सबसे सरल प्रकार के प्रकार मोनोटाइप्स हैं: Int , String , String → Char और इसी तरह, लेकिन अगर हम चाहें, तो हम अधिक सार / सामान्य प्रकार - पॉलीटाइप्स बना सकते हैं।

[Let]



आम तौर पर आसान:
यदि हम यह घटा सकते हैं कि e ₀ टाइप that का है
और
अगर हम मान लें कि x भी टाइप σ है और इससे हम यह घटा सकते हैं कि e ₁ टाइप τ का है

हम यह निष्कर्ष निकाल सकते हैं कि x को e _{0 के} बराबर सेट करने और इसे e ₁ में प्रतिस्थापित करने का परिणाम the होगा।

अंतिम चार नियम हमारे सहज ज्ञान के एक औपचारिक प्रतिबिंब से अधिक कुछ भी नहीं हैं कि हम किस प्रकार प्राप्त कर सकते हैं यदि हमारे पास चर हैं जिनके साथ हम गुमनाम कार्य करते हैं, या जिनसे हम साधारण कार्यों को लागू करते हैं, या अभिव्यक्तियों के अंदर स्थानापन्न अभिव्यक्तियाँ करते हैं। यह वही है जो हम, प्रोग्रामर के रूप में, सहज रूप से करते हैं। यहां हम केवल इस बारे में बात करते हैं कि इस सभी को औपचारिक रूप से कैसे वर्णित किया जाए। अंत में, हमारे दिमाग में होने वाली हर चीज अज्ञात जादू नहीं है। यह भी ध्यान देने योग्य है कि अंतिम चार नियम वास्तव में चार नियमों के अनुरूप हैं जो यह निर्धारित करते हैं कि लैम्ब्डा कैलकुलस में एक वैध अभिव्यक्ति क्या है। और यह कोई संयोग नहीं है।

[Inst]



यह एक उदाहरण नियम है। आप बहुवचन Array[Int] बारे में सोच सकते हैं Array[Int] → बहुवचन के उदाहरण के रूप में .A t.Array[t] → t । दूसरे शब्दों में, यह "विशेषज्ञता" है: Array[Int] → Int t.Array[t] → t तुलना Int अधिक विशिष्ट है। हमारा मतलब है "से अधिक विशिष्ट"। यानी



इस प्रकार, [Inst] का सीधा अनुवाद इस प्रकार है: यदि हम यह घटा सकते हैं कि e टाइप σ ′ का है और / σ σ का उदाहरण / विशेषज्ञता है, तो हम यह निष्कर्ष निकाल सकते हैं कि e टाइप σ का है। आप क्रमशः → और σ Array[t] को Array[t] → t और t.Array[t] → t रूप में सोच सकते हैं।

[जनरल]



यह समझने में सबसे कठिन हिस्सा है। वास्तव में, यह अकेले नियमों की संकीर्ण सेट का उपयोग करते हुए टाइप इंफ़ेक्शन प्रक्रिया के संदर्भ में मायने रखता है जो ऊपर उल्लिखित था। इसका एक स्पष्ट एनालॉग नहीं है, क्योंकि यह काफी हद तक एक प्रकार के चर की अवधारणा पर निर्भर करता है - ऐसा कुछ जो वास्तविक प्रोग्रामिंग भाषाओं में कभी नहीं पाया जाता है, लेकिन अपरिहार्य है जब हम किसी भी प्रकार के मनमाने ढंग से बात करने के लिए मेटा-भाषा के साथ काम करने की कोशिश करते हैं प्रोग्रामिंग भाषा। सामान्य शब्दों में, इस विचार को निम्नलिखित "उदाहरण" में दिखाया जा सकता है:

मान लीजिए कि आपके पास दो चर x और y , और सबसे पहले आप यह मानते हैं कि दोनों प्रकार α के हैं, जहाँ α एक प्रकार को दर्शाने वाला चर है। बाद में आप एक अभिव्यक्ति के लिए आते हैं जिसके लिए आपने किसी तरह से यह माना है कि इसका प्रकार α → α है इस संदर्भ में (धारणा का संदर्भ कि x और y प्रकार α के हैं)। और अब ध्यान सवाल है: क्या इस फ़ंक्शन का पॉलीटाइप ∀α.α → α होगा? यानी क्या यह फ़ंक्शन ऑब्जेक्ट्स को समान रूप से समान रूप से जोड़ता है, या क्या यह केवल ऐसा प्रतीत होता है क्योंकि आपने माना कि x और y एक ही प्रकार के हैं α?

चूंकि α एक प्रकार का चर है, अर्थात किसी भी प्रकार को निरूपित कर सकते हैं, हम यह सोचना चाहेंगे कि चूंकि हमने घटाया है कि e प्रकार α → α का है, तो इसका भी बहुदेवता ∀α.α → α है। लेकिन हम यह नहीं कह सकते हैं कि यह सामान्यीकरण x और y से संबंधित e बारे में अधिक समझ के बिना आवश्यक है। विशेष रूप से, यदि हमारा निष्कर्ष यह है कि इसका प्रकार α → α है, जो इस प्रकार से संबंधित हमारी पिछली मान्यताओं से दृढ़ता से जुड़ा हुआ है, तो हम यह निष्कर्ष नहीं निकाल सकते हैं कि e में बहुपद ∀α.α → α है।

और अब (अंत में!) नियम का अनुवाद:

यदि α का कुछ चर हमारे वर्तमान संदर्भ / ज्ञान / मान्यताओं के सेट में "स्वतंत्र रूप से" वर्णित नहीं है, और हम यह निष्कर्ष निकाल सकते हैं कि कुछ अभिव्यक्ति e में कुछ प्रकार है, तो हम निष्कर्ष निकाल सकते हैं कि e का प्रकार σ है, चाहे , आखिरकार α में बदल जाता है। थोड़ा और अधिक तकनीकी: e में पॉलीटाइप σα. e है।

ठीक है, लेकिन "शिथिल उल्लेख" का क्या अर्थ है? बहुवचन .α.α → α, α को "वास्तविक" के लिए संदर्भित नहीं किया जाता है। यह प्रकार पूरी तरह से अनुरूप है, उदाहरण के लिए, β.β → ous। इनमें से किसी भी प्रकार के साथ एक अभिव्यक्ति एक नियमित कार्य है जिसमें समान इनपुट और आउटपुट प्रकार होते हैं। दूसरी ओर, x: α α का "वास्तविक" उल्लेख है।



और



विभिन्न चीजों का मतलब है। उत्तरार्द्ध का सुझाव है कि x और y निश्चित रूप से एक ही प्रकार के हैं (भले ही उस प्रकार को अभी तक परिभाषित नहीं किया गया है)। पहला x और y के संबंधों की रिपोर्ट नहीं करता है। अंतर यह है कि जब α का उल्लेख डोमेन the के अंदर होता है (जैसा कि thatα.α → α के मामले में), तो यह केवल एक कल्पना है जिसे बाकी संदर्भ की परवाह किए बिना किसी भी अन्य प्रकार के चर के साथ प्रतिस्थापित किया जा सकता है। इस प्रकार, हम स्थिति की व्याख्या कर सकते हैं "α स्वतंत्र रूप से as के संदर्भ में संदर्भित नहीं है" के रूप में "या तो बिल्कुल भी उल्लेख नहीं किया गया है, या एक कल्पना माना जाता है और, सिद्धांत रूप में, हमारे संदर्भ में ज्ञान या मान्यताओं के शब्दार्थ को बदलने के बिना कुछ पूरी तरह से अलग किया जा सकता है"।

वह सब है।

अनुवादक का नोट: अनुवाद के बारे में पीएम की किसी भी टिप्पणी के लिए मैं बहुत आभारी रहूंगा।