Hindley–Milner type system
एक हिंडले-मिलनर (एच. एम.) प्रकार प्रणाली पैरामीट्रिक बहुरूपता के साथ लैम्ब्डा कलन के लिए एक शास्त्रीय प्रकार की प्रणाली है। इसे दामास-मिलनर या दामास-हिंडले-मिलनर के नाम से भी जाना जाता है। इसे पहले जे. रोजर हिंडले द्वारा वर्णित किया गया था और बाद में रॉबिन मिलनर द्वारा फिर से खोजा गया था। लुइस दामास ने अपनी पीएचडी थीसिस में एक करीबी औपचारिक विश्लेषण और विधि के प्रमाण का योगदान दिया। एच. एम. के अधिक उल्लेखनीय गुणों में इसकी पूर्णता और प्रोग्रामर द्वारा प्रदान किए गए प्रकार एनोटेशन या अन्य संकेतों के बिना किसी दिए गए प्रोग्राम के सबसे सामान्य प्रकार का अनुमान लगाने की इसकी क्षमता है। एल्गोरिदम डब्ल्यू व्यवहार में एक कुशल प्रकार की अनुमान विधि है और इसे बड़े कोड आधारों पर सफलतापूर्वक लागू किया गया है, हालांकि इसमें उच्च सैद्धांतिक जटिलता है। एच. एम. का उपयोग अधिमानतः कार्यात्मक भाषाओं के लिए किया जाता है। इसे पहली बार प्रोग्रामिंग भाषा एमएल की प्रकार प्रणाली के हिस्से के रूप में लागू किया गया था। तब से, एच. एम. को विभिन्न तरीकों से विस्तारित किया गया है, विशेष रूप से हास्केल की तरह प्रकार वर्ग की बाधाओं के साथ। परिचय एक प्रकार अनुमान विधि के रूप में, हिंडले-मिलनर पूरी तरह से अप्रचलित शैली में लिखे गए कार्यक्रमों से चर, अभिव्यक्तियों और कार्यों के प्रकार का अनुमान लगाने में सक्षम है। कार्यक्षेत्र के प्रति संवेदनशील होने के कारण, यह केवल स्रोत कोड के एक छोटे से हिस्से से ही प्रकार प्राप्त करने तक सीमित नहीं है, बल्कि पूर्ण कार्यक्रमों या मॉड्यूल से प्राप्त करने तक सीमित है। पैरामीट्रिक प्रकारों का सामना करने में सक्षम होने के कारण, यह कई कार्यात्मक प्रोग्रामिंग भाषाओं की प्रकार प्रणालियों के लिए भी महत्वपूर्ण है। इसे पहली बार एम. एल. प्रोग्रामिंग भाषा में इस तरह से लागू किया गया था। इसकी उत्पत्ति सरल रूप से टाइप किए गए लैम्ब्डा कलन के लिए प्रकार अनुमान एल्गोरिथ्म है जिसे 1958 में हास्केल करी और रॉबर्ट फीस द्वारा तैयार किया गया था। 1969 में, जे. रोजर हिंडले ने इस काम का विस्तार किया और साबित किया कि उनके एल्गोरिदम ने हमेशा सबसे सामान्य प्रकार का अनुमान लगाया। 1978 में, रॉबिन मिलनर, स्वतंत्र रूप से हिंडले के काम से, एक समकक्ष एल्गोरिथ्म प्रदान किया, एल्गोरिथ्म डब्ल्यू। 1982 में, लुइस डमास ने अंततः साबित किया कि मिलनर का एल्गोरिथ्म पूरा हो गया है और इसे बहुरूपी संदर्भों के साथ प्रणालियों का समर्थन करने के लिए विस्तारित किया। मोनोमोर्फिज्म बनाम बहुरूपता सरल रूप से टाइप किए गए लैम्ब्डा कलन में, प्रकार या तो परमाणु प्रकार के स्थिरांक या कार्य प्रकार के रूप होते हैं। इस प्रकार के मोनोमॉर्फिक होते हैं। विशिष्ट उदाहरण अंकगणितीय मूल्यों में उपयोग किए जाने वाले प्रकार हैंः 3: संख्या जोड़ 3 4: संख्या जोड़ः संख्या-> संख्या-> संख्या इसके विपरीत, अनटाइप्ड लैम्ब्डा कलन टाइपिंग के लिए बिल्कुल भी तटस्थ है, और इसके कई कार्यों को सभी प्रकार के तर्कों पर सार्थक रूप से लागू किया जा सकता है। तुच्छ उदाहरण पहचान फलन आईडी ष्ण λx है। x जो बस जो भी मूल्य पर लागू होता है उसे लौटाता है। कम तुच्छ उदाहरणों में सूचियों जैसे पैरामीट्रिक प्रकार शामिल हैं। जबकि सामान्य रूप से बहुरूपता का अर्थ है कि संचालन एक से अधिक प्रकार के मूल्यों को स्वीकार करते हैं, यहाँ उपयोग किया जाने वाला बहुरूपता पैरामीट्रिक है। साहित्य में प्रकार योजनाओं की संकेतन भी पाई जाती है, जो बहुरूपता की पैरामीट्रिक प्रकृति पर जोर देती है। इसके अतिरिक्त, स्थिरांक को (मात्रात्मक) प्रकार के चर के साथ टाइप किया जा सकता है। ई. जी. : विपक्षः सभी ए। a-> सूची a-> सूची a शून्यः सभी के लिए a। एक आई. डी. सूचीबद्ध कीजिएः forall a. a-> एक बहुरूपी प्रकार अपने चरों के सुसंगत प्रतिस्थापन द्वारा एकरस हो सकते हैं। मोनोमोर्फिक उदाहरणों के उदाहरण हैंः आईडी ': स्ट्रिंग-> स्ट्रिंग नील': सूची संख्या अधिक आम तौर पर, प्रकार बहुरूपी होते हैं जब उनमें प्रकार चर होते हैं, जबकि उनके बिना प्रकार मोनोमोर्फिक होते हैं। उदाहरण के लिए पास्कल (1970) या सी (1972) में उपयोग की जाने वाली प्रकार प्रणालियों के विपरीत, जो केवल मोनोमोर्फिक प्रकारों का समर्थन करते हैं, एच. एम. को पैरामीट्रिक बहुरूपता पर जोर देने के साथ डिज़ाइन किया गया है। सी + + (1985) जैसी उल्लिखित भाषाओं के उत्तराधिकारियों ने विभिन्न प्रकार के बहुरूपता पर ध्यान केंद्रित किया, अर्थात् ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग और ओवरलोडिंग के संबंध में सबटाइपिंग। जबकि उपप्रकार एच. एम. के साथ असंगत है, हास्केल की एच. एम.-आधारित प्रकार प्रणाली में व्यवस्थित अधिभार का एक प्रकार उपलब्ध है। चलो-बहुरूपता जब बहुरूपता की ओर सरल रूप से टाइप किए गए लैम्ब्डा कलन के लिए प्रकार अनुमान का विस्तार करते हैं, तो किसी को यह परिभाषित करना होगा कि किसी मूल्य का उदाहरण कब प्राप्त करना स्वीकार्य है। आदर्श रूप से, इसे एक बाध्य चर के किसी भी उपयोग के साथ अनुमति दी जाएगी, जैसे किः (λ आईडी। . (आईडी 3). (आईडी "पाठ").) (λx। x) दुर्भाग्य से, बहुरूपी लैम्ब्डा कलन में प्रकार का अनुमान निर्णायक नहीं है। इसके बजाय, एच. एम. आई. डी. = λx के रूप में एक लेट-बहुरूपता प्रदान करता है। x में. (आईडी 3). (आईडी "पाठ"). अभिव्यक्ति वाक्यविन्यास के विस्तार में बाध्यकारी तंत्र को सीमित करना। केवल एक लेट निर्माण में बंधे मूल्य तात्कालिकता के अधीन हैं, अर्थात। बहुरूपी होते हैं, जबकि लैम्ब्डा-एब्स्ट्रैक्शन में मापदंडों को मोनोमोर्फिक माना जाता है। इस लेख का शेष भाग इस प्रकार हैः एच. एम. प्रकार प्रणाली को परिभाषित किया गया है। यह एक कटौती प्रणाली का वर्णन करके किया जाता है जो सटीक बनाता है कि किस प्रकार की अभिव्यक्तियाँ हैं, यदि कोई हो। वहाँ से, यह प्रकार अनुमान विधि के कार्यान्वयन की दिशा में काम करता है। उपरोक्त अनुमानात्मक प्रणाली के एक वाक्यविन्यास-संचालित संस्करण को पेश करने के बाद, यह एक कुशल कार्यान्वयन (एल्गोरिथ्म जे) का चित्रण करता है, जो ज्यादातर पाठक के धात्विक अंतर्ज्ञान को आकर्षित करता है। क्योंकि यह खुला रहता है कि क्या एल्गोरिथ्म जे वास्तव में प्रारंभिक कटौती प्रणाली को महसूस करता है, एक कम कुशल कार्यान्वयन (एल्गोरिथ्म डब्ल्यू), पेश किया जाता है और एक प्रमाण में इसके उपयोग का संकेत दिया जाता है। अंत में, एल्गोरिथ्म से संबंधित आगे के विषयों पर चर्चा की जाती है। कटौती प्रणाली के समान विवरण का उपयोग पूरे समय किया जाता है, यहां तक कि दो एल्गोरिदम के लिए भी, विभिन्न रूपों को बनाने के लिए जिसमें एच. एम. विधि को सीधे तुलनीय रूप से प्रस्तुत किया जाता है। हिंडले-मिलनर प्रकार प्रणाली प्रकार प्रणाली को औपचारिक रूप से वाक्यविन्यास नियमों द्वारा वर्णित किया जा सकता है जो अभिव्यक्तियों, प्रकारों आदि के लिए एक भाषा तय करते हैं। यहाँ इस तरह के वाक्यविन्यास की प्रस्तुति बहुत औपचारिक नहीं है, क्योंकि इसे सतह व्याकरण का अध्ययन करने के लिए नहीं, बल्कि गहन व्याकरण का अध्ययन करने के लिए लिखा गया है, और कुछ वाक्यात्मक विवरणों को खुला छोड़ देता है। प्रस्तुतिक ई रूप सामान्य अछि। इसके आधार पर, टाइपिंग नियमों का उपयोग यह परिभाषित करने के लिए किया जाता है कि अभिव्यक्तियाँ और प्रकार कैसे संबंधित हैं। पहले की तरह, उपयोग किया जाने वाला रूप थोड़ा उदार है। वाक्यविन्यास टाइप की जाने वाली अभिव्यक्तियाँ ठीक लैम्ब्डा कैलकुलस की हैं जो एक लेट-एक्सप्रेशन के साथ विस्तारित हैं जैसा कि आसन्न तालिका में दिखाया गया है। कोष्ठक का उपयोग किसी अभिव्यक्ति को अस्पष्ट करने के लिए किया जा सकता है। अनुप्रयोग लेफ्ट-बाइंडिंग है और एब्स्ट्रैक्शन या लेट-इन निर्माण की तुलना में मजबूत बांधता है। प्रकारों को वाक्यात्मक रूप से दो समूहों, मोनोटाइप और पॉलीटाइप में विभाजित किया गया है। मोनोटाइप मोनोटाइप हमेशा एक विशेष प्रकार को निर्दिष्ट करते हैं। मोनोटाइप को वाक्यात्मक रूप से शब्दों के रूप में दर्शाया जाता है। मोनोटाइप के उदाहरणों में प्रकार स्थिरांक जैसे या, और पैरामीट्रिक प्रकार जैसे शामिल हैं। बाद के प्रकार प्रकार कार्यों के अनुप्रयोगों के उदाहरण हैं, उदाहरण के लिए, सेट से, जहां सुपरस्क्रिप्ट प्रकार मापदंडों की संख्या को इंगित करता है। एच. एम. में प्रकार कार्यों का पूरा सेट मनमाना है, सिवाय इसके कि इसमें कम से कम, प्रकार के कार्य होने चाहिए। इसे अक्सर सुविधा के लिए इन्फिक्स संकेतन में लिखा जाता है। उदाहरण के लिए, स्ट्रिंग्स के लिए एक फ़ंक्शन मैपिंग पूर्णांक में प्रकार होता है। एक बार फिर, कोष्ठक का उपयोग किसी प्रकार की अभिव्यक्ति को स्पष्ट करने के लिए किया जा सकता है। अनुप्रयोग इन्फिक्स तीर की तुलना में मजबूत बंधन करता है, जो कि सही-बंधन है। प्रकार चर को मोनोटाइप के रूप में स्वीकार किया जाता है। मोनोटाइप को मोनोमोर्फिक प्रकारों के साथ भ्रमित नहीं किया जाना चाहिए, जो चर को बाहर करते हैं और केवल जमीनी शब्दों की अनुमति देते हैं। यदि समान पद हों तो दो मोनोटाइप बराबर होते हैं। पॉलीटाइप्स पॉलीटाइप्स (या प्रकार योजनाएं) ऐसे प्रकार हैं जिनमें शून्य या सभी के लिए अधिक क्वांटिफायर से बंधे चर होते हैं, जैसे। .. पॉलीटाइप के साथ एक फ़ंक्शन एक ही प्रकार के किसी भी मूल्य को अपने लिए मैप कर सकता है, और पहचान फ़ंक्शन इस प्रकार के लिए एक मान है। एक अन्य उदाहरण के रूप में, पूर्णांकों के लिए सभी परिमित सेटों का मानचित्रण करने वाले फ़ंक्शन का प्रकार है। एक फलन जो एक समुच्चय की कार्डिनलिटी देता है, इस प्रकार का मान होगा। क्वांटिफायर केवल शीर्ष स्तर पर दिखाई दे सकते हैं। उदाहरण के लिए, एक प्रकार को प्रकारों के वाक्यविन्यास द्वारा बाहर रखा जाता है। एकर अलावा मोनोटाइपकेँ पॉलीटाइप्समे शामिल कयल जायत छैक, एहि प्रकारेँ एक प्रकारक सामान्य रूप होयत छैक, जतऽ एक मोनोटाइप होयत छैक। बहुपदों की समानता परिमाणीकरण को फिर से व्यवस्थित करने और परिमाणीकृत चर (-रूपांतरण) का नाम बदलने पर निर्भर है। इसके अलावा, मोनोटाइप में नहीं होने वाले मात्रात्मक चर को हटाया जा सकता है। संदर्भ और टाइपिंग अभी भी असंबद्ध भागों (वाक्यविन्यास अभिव्यक्तियों और प्रकारों) को सार्थक रूप से एक साथ लाने के लिए एक तीसरे भाग की आवश्यकता हैः संदर्भ। वाक्यात्मक रूप से, एक संदर्भ जोड़े की एक सूची है, जिसे असाइनमेंट, धारणाएं या बाइंडिंग कहा जाता है, प्रत्येक जोड़ी यह बताती है कि मूल्य चर का प्रकार है सभी तीन भाग संयुक्त रूप से रूप का एक टाइपिंग निर्णय देते हैं, जिसमें कहा गया है कि मान्यताओं के तहत, अभिव्यक्ति का प्रकार होता है। मुक्त प्रकार के चर एक प्रकार में, प्रतीक मोनोटाइप में प्रकार के चर को बांधने वाला परिमापक है। चर को मात्रात्मक कहा जाता है और एक मात्रात्मक प्रकार के चर की किसी भी घटना को बाध्य कहा जाता है और सभी अनबाउंड प्रकार के चर को मुक्त कहा जाता है। पॉलीटाइप्स में परिमाणीकरण के अतिरिक्त, प्रकार चर भी संदर्भ में होने से बंधे हो सकते हैं, लेकिन के दाहिने हाथ की ओर विपरीत प्रभाव के साथ। इस तरह के चर तब वहाँ प्रकार स्थिरांक की तरह व्यवहार करते हैं। अंत में, एक प्रकार चर कानूनी रूप से एक टाइपिंग में अनबाउंड हो सकता है, जिस स्थिति में वे निहित रूप से सभी-मात्रा में होते हैं। प्रोग्रामिंग भाषाओं में बाउंड और अनबाउंड दोनों प्रकार के चरों की उपस्थिति थोड़ी असामान्य है। अक्सर, सभी प्रकार के चर को अंतर्निहित रूप से पूर्ण-मात्रात्मक माना जाता है। उदाहरण के लिए, प्रोलॉग में मुक्त चर वाले खंड नहीं हैं। इसी तरह हास्केल में, जहां सभी प्रकार के चर निहित रूप से मात्रात्मक रूप से होते हैं, अर्थात। यहाँ एक हास्केल टाइप a-> a का मतलब है। असाइनमेंट के दाहिने हाथ की ओर का बाध्यकारी प्रभाव संबंधित और बहुत असामान्य भी है। आमतौर पर, बाध्य और अनबाउंड दोनों प्रकार के चरों का मिश्रण एक अभिव्यक्ति में मुक्त चरों के उपयोग से उत्पन्न होता है। स्थिर फलन K = एक उदाहरण प्रदान करता है। इसका मोनोटाइप है। द्वारा बहुरूपता को मजबूर किया जा सकता है। यहाँ, प्रकार है। मुक्त मोनोटाइप चर आसपास के दायरे में बंधे चर के प्रकार से उत्पन्न होता है। प्रकार है। के प्रकार से बंधे होने के प्रकार में मुक्त प्रकार के चर की कल्पना की जा सकती है। लेकिन इस तरह के दायरे को एच. एम. में व्यक्त नहीं किया जा सकता है। बल्कि, बंधन को संदर्भ द्वारा महसूस किया जाता है। प्रकार क्रम बहुरूपता का अर्थ है कि एक ही अभिव्यक्ति में (शायद अनंत) कई प्रकार हो सकते हैं। लेकिन इस प्रकार की प्रणाली में, ये प्रकार पूरी तरह से असंबंधित नहीं हैं, बल्कि पैरामीट्रिक बहुरूपता द्वारा ऑर्केस्ट्रेटेड हैं। एक उदाहरण के रूप में, पहचान के अपने प्रकार के साथ-साथ या और कई अन्य हो सकते हैं, लेकिन नहीं। इस कार्य के लिए सबसे सामान्य प्रकार है, जबकि अन्य अधिक विशिष्ट हैं और प्रकार पैरामीटर के लिए दूसरे प्रकार को लगातार प्रतिस्थापित करके सामान्य से प्राप्त किया जा सकता है, अर्थात। मात्रात्मक चर। प्रति-उदाहरण विफल हो जाता है क्योंकि प्रतिस्थापन सुसंगत नहीं है। लगातार प्रतिस्थापन को लिखित रूप में एक प्रकार की अवधि के प्रतिस्थापन को लागू करके औपचारिक बनाया जा सकता है। जैसा कि उदाहरण से पता चलता है, प्रतिस्थापन न केवल एक आदेश से दृढ़ता से संबंधित है, जो व्यक्त करता है कि एक प्रकार कमोबेश विशेष है, बल्कि सभी-मात्रा के साथ भी है जो प्रतिस्थापन को लागू करने की अनुमति देता है। औपचारिक रूप से, एच. एम. में, एक प्रकार अधिक सामान्य होता है, औपचारिक रूप से, यदि कुछ मात्रात्मक चर को लगातार इस तरह प्रतिस्थापित किया जाता है कि एक लाभ जैसा कि साइड बार में दिखाया गया है। यह क्रम प्रकार प्रणाली की प्रकार परिभाषा का हिस्सा है। हमारे पिछले उदाहरण में, प्रतिस्थापन को लागू करने का परिणाम होगा। जबकि एक मात्रात्मक चर के लिए एक मोनोमॉर्फिक (ग्राउंड) प्रकार को प्रतिस्थापित करना सीधा है, एक पॉलीटाइप को प्रतिस्थापित करने में मुक्त चर की उपस्थिति के कारण कुछ नुकसान होते हैं। विशेष रूप से, अनबाउंड चर को प्रतिस्थापित नहीं किया जाना चाहिए। इन्हें यहाँ स्थिर माना जाता है। इसके अतिरिक्त, परिमाणीकरण केवल शीर्ष स्तर पर ही हो सकते हैं। एक पैरामीट्रिक प्रकार को प्रतिस्थापित करते हुए, किसी को इसके क्वांटिफायर्स को उठाना पड़ता है। दाहिनी ओर की मेज नियम को सटीक बनाती है। वैकल्पिक रूप से, बिना क्वांटिफायर के पॉलीटाइप्स के लिए एक समतुल्य संकेतन पर विचार करें जिसमें क्वांटिफाइड चर को प्रतीकों के एक अलग सेट द्वारा दर्शाया जाता है। इस तरह के संकेतन में, विशेषज्ञता इस तरह के चर के सादे सुसंगत प्रतिस्थापन तक कम हो जाती है। संबंध एक आंशिक क्रम है और इसका सबसे छोटा तत्व है। जबकि एक प्रकार की योजना का विशेषज्ञता क्रम का एक उपयोग है, यह प्रकार प्रणाली में एक महत्वपूर्ण दूसरी भूमिका निभाता है। बहुरूपता के साथ प्रकार अनुमान एक अभिव्यक्ति के सभी संभावित प्रकारों को संक्षेप में प्रस्तुत करने की चुनौती का सामना करता है। आदेश इस बात की गारंटी देता है कि इस तरह का सारांश अभिव्यक्ति के सबसे सामान्य प्रकार के रूप में मौजूद है। टाइपिंग में प्रतिस्थापन ऊपर परिभाषित प्रकार क्रम को टाइपिंग तक बढ़ाया जा सकता है क्योंकि टाइपिंग का निहित ऑल-क्वांटिफिकेशन सुसंगत प्रतिस्थापन को सक्षम बनाता हैः विशेषज्ञता नियम के विपरीत, यह परिभाषा का हिस्सा नहीं है, बल्कि अंतर्निहित ऑल-क्वांटिफिकेशन की तरह है, बल्कि अगले परिभाषित प्रकार नियमों का एक परिणाम है। टाइपिंग में मुक्त प्रकार के चर संभावित परिष्करण के लिए प्लेसहोल्डर के रूप में काम करते हैं। दाहिने हाथ की ओर मुक्त प्रकार के चर के लिए पर्यावरण का बाध्यकारी प्रभाव विशेषज्ञता नियम में उनके प्रतिस्थापन को फिर से प्रतिबंधित करता है कि एक प्रतिस्थापन सुसंगत होना चाहिए और पूरी टाइपिंग को शामिल करने की आवश्यकता होगी। यह लेख चार अलग-अलग नियम सेटों पर चर्चा करेगाः घोषणात्मक प्रणाली वाक्यात्मक प्रणाली एल्गोरिदम जे एल्गोरिदम डब्ल्यू डिडक्टिव सिस्टम एच. एम. के वाक्यविन्यास को अनुमान नियमों के वाक्यविन्यास के लिए आगे बढ़ाया जाता है जो औपचारिक प्रणाली के मुख्य भाग का निर्माण करते हैं, निर्णय के रूप में टाइपिंग का उपयोग करके। प्रत्येक नियम परिभाषित करता है कि किस परिसर से क्या निष्कर्ष निकाला जा सकता है। निर्णयों के अतिरिक्त, ऊपर पेश की गई कुछ अतिरिक्त शर्तों का उपयोग परिसर के रूप में भी किया जा सकता है। नियमों का उपयोग करने वाला प्रमाण निर्णयों का एक क्रम है जिसमें किसी निष्कर्ष से पहले सभी परिसरों को सूचीबद्ध किया जाता है। नीचे दिए गए उदाहरण प्रमाणों का एक संभावित प्रारूप दिखाते हैं। बाएँ से दाएँ, प्रत्येक पंक्ति निष्कर्ष, लागू किए गए नियम और परिसर को दिखाती है, या तो पहले की पंक्ति (संख्या) का उल्लेख करके यदि आधार एक निर्णय है या विधेय को स्पष्ट करके। टाइपिंग के नियम भी देखें टाइपिंग के नियम साइड बॉक्स एच. एम. प्रकार प्रणाली के कटौती नियमों को दर्शाता है। नियमों को मोटे तौर पर दो समूहों में विभाजित किया जा सकता हैः पहले चार नियम (चर या कार्य अभिगम), (अनुप्रयोग, अर्थात। एक पैरामीटर के साथ फ़ंक्शन कॉल), (अमूर्तता, अर्थात। फलन घोषणा) और (परिवर्तनीय घोषणा) वाक्यविन्यास के आसपास केंद्रित हैं, जो अभिव्यक्ति रूपों में से प्रत्येक के लिए एक नियम प्रस्तुत करते हैं। उनका अर्थ पहली नज़र में स्पष्ट है, क्योंकि वे प्रत्येक अभिव्यक्ति को विघटित करते हैं, अपनी उप-अभिव्यक्तियों को साबित करते हैं और अंत में परिसर में पाए जाने वाले अलग-अलग प्रकारों को निष्कर्ष में पाए जाने वाले प्रकार से जोड़ते हैं। दूसरा समूह शेष दो नियमों और द्वारा बनाया जाता है। वे प्रकारों के विशेषज्ञता और सामान्यीकरण को संभालते हैं। जबकि उपरोक्त विशेषज्ञता पर अनुभाग से नियम स्पष्ट होना चाहिए, विपरीत दिशा में काम करते हुए पूर्व का पूरक है। यह सामान्यीकरण की अनुमति देता है, अर्थात। मोनोटाइप चरों की मात्रा निर्धारित करने के लिए जो संदर्भ में बाध्य नहीं हैं। निम्नलिखित दो उदाहरण नियम प्रणाली का उपयोग करते हैं। चूँकि अभिव्यक्ति और प्रकार दोनों दिए गए हैं, वे नियमों का एक प्रकार-जाँच उपयोग हैं। उदाहरण-कहाँ, के लिए एक प्रमाण लिखा जा सकता है सामान्यीकरण को प्रदर्शित करने के लिए, नीचे दिखाया गया हैः चलो-बहुरूपता तुरंत दिखाई नहीं देता है, नियम सेट एक विनियमन को कूटबद्ध करता है जिसके तहत एक प्रकार को सामान्यीकृत किया जा सकता है या नहीं नियमों में मोनो-और पॉलीटाइप्स के थोड़े अलग उपयोग से और। इसे याद रखें और क्रमशः पॉली-और मोनोटाइप को निरूपित करें। नियम में, फलन के पैरामीटर के मूल्य चर को आधार के माध्यम से एक मोनोमॉर्फिक प्रकार के साथ संदर्भ में जोड़ा जाता है, जबकि नियम में, चर बहुरूपी रूप में वातावरण में प्रवेश करता है। हालांकि दोनों ही मामलों में संदर्भ में की उपस्थिति असाइनमेंट में किसी भी मुक्त चर के लिए सामान्यीकरण नियम के उपयोग को रोकती है, यह विनियमन एक-अभिव्यक्ति में पैरामीटर के प्रकार को मोनोमोर्फिक रहने के लिए मजबूर करता है, जबकि एक अभिव्यक्ति में, चर को बहुरूपी पेश किया जा सकता है, जिससे विशेषज्ञता संभव हो जाती है। इस विनियमन के परिणामस्वरूप, टाइप नहीं किया जा सकता है, क्योंकि पैरामीटर एक मोनोमॉर्फिक स्थिति में है, जबकि टाइप है, क्योंकि इसे एक लेट-एक्सप्रेशन में पेश किया गया है और इसलिए इसे बहुरूपी माना जाता है। सामान्यीकरण नियम सामान्यीकरण नियम को भी करीब से देखने लायक है। यहाँ, आधार में निहित सभी-मात्रा को बस निष्कर्ष में दाहिने हाथ की ओर ले जाया जाता है। यह संभव है, क्योंकि यह संदर्भ में स्वतंत्र रूप से नहीं होता है। फिर से, जबकि यह सामान्यीकरण नियम को प्रशंसनीय बनाता है, यह वास्तव में एक परिणाम नहीं है। इसके विपरीत, सामान्यीकरण नियम एच. एम. की प्रकार प्रणाली की परिभाषा का हिस्सा है और अंतर्निहित सभी-मात्रा एक परिणाम है। एक अनुमान एल्गोरिथ्म अब जब एच. एम. की कटौती प्रणाली हाथ में है, तो कोई एक एल्गोरिथ्म प्रस्तुत कर सकता है और नियमों के संबंध में इसे मान्य कर सकता है। वैकल्पिक रूप से, नियमों की परस्पर क्रिया और प्रमाण कैसे बनाए जाते हैं, इस पर करीब से नज़र डालकर इसे प्राप्त करना संभव हो सकता है। यह इस लेख के शेष भाग में उन संभावित निर्णयों पर ध्यान केंद्रित करते हुए किया गया है जो एक टाइपिंग साबित करते समय किए जा सकते हैं। एक प्रमाण में अंकों को अलग करते हुए, जहां कोई निर्णय संभव नहीं है, वाक्य रचना के आसपास केंद्रित नियमों का पहला समूह कोई विकल्प नहीं छोड़ता है क्योंकि प्रत्येक वाक्य रचना नियम एक अद्वितीय टाइपिंग नियम से मेल खाता है, जो प्रमाण के एक हिस्से को निर्धारित करता है, जबकि निष्कर्ष और इन निश्चित भागों की श्रृंखलाओं के परिसर के बीच और हो सकता है। इस तरह की एक श्रृंखला प्रमाण के निष्कर्ष और सर्वोच्च अभिव्यक्ति के नियम के बीच भी मौजूद हो सकती है। सभी प्रमाणों में इस तरह से रेखाचित्रित आकार होना चाहिए। क्योंकि नियम चयन के संबंध में प्रमाण में एकमात्र विकल्प और श्रृंखलाएं हैं, प्रमाण का रूप इस सवाल का सुझाव देता है कि क्या इसे अधिक सटीक बनाया जा सकता है, जहां इन श्रृंखलाओं की आवश्यकता नहीं हो सकती है। यह वास्तव में संभव है और बिना ऐसे नियमों के नियम प्रणाली के एक प्रकार की ओर ले जाता है। वाक्यविन्यास-निर्देशित नियम प्रणाली एच. एम. का एक समकालीन उपचार एक मध्यवर्ती चरण के रूप में क्लेमेंट के कारण विशुद्ध रूप से वाक्यविन्यास-निर्देशित नियम प्रणाली का उपयोग करता है। इस प्रणाली में, विशेषज्ञता सीधे मूल नियम के बाद स्थित होती है और इसमें विलय हो जाती है, जबकि सामान्यीकरण नियम का हिस्सा बन जाता है। वहाँ सामान्यीकरण को हमेशा फ़ंक्शन को पेश करके सबसे सामान्य प्रकार का उत्पादन करने के लिए भी निर्धारित किया जाता है, जो सभी मोनोटाइप चरों की मात्रा निर्धारित करता है जो बाध्य नहीं हैं। औपचारिक रूप से, यह मान्य करने के लिए कि यह नई नियम प्रणाली मूल के बराबर है, किसी को यह दिखाना होगा, जो दो उप-प्रमाणों में विघटित हो जाता हैः (निरंतरता) (पूर्णता) जबकि स्थिरता को नियमों को विघटित करके और प्रमाणों में देखा जा सकता है, यह संभवतः दिखाई देता है जो अधूरा है, जैसा कि कोई भी उदाहरण के लिए नहीं दिखा सकता है, लेकिन केवल। पूर्णता का केवल थोड़ा कमजोर संस्करण सिद्ध करने योग्य है, जिसका अर्थ है, कोई भी हमें अंत में प्रमाण को सामान्य बनाने की अनुमति देने में एक अभिव्यक्ति के लिए प्रमुख प्रकार प्राप्त कर सकता है। तुलना और, अब सभी नियमों के निर्णयों में केवल मोनोटाइप दिखाई देते हैं। इसके अतिरिक्त, कटौती प्रणाली के साथ किसी भी संभावित प्रमाण का आकार अब अभिव्यक्ति के आकार (दोनों को पेड़ के रूप में देखा जाता है) के समान है। इस प्रकार अभिव्यक्ति पूरी तरह से प्रमाण के आकार को निर्धारित करती है। आकार में संभवतः और को छोड़कर सभी नियमों के संबंध में निर्धारित किया जाएगा, जो अन्य नोड्स के बीच मनमाने ढंग से लंबी शाखाओं (श्रृंखलाओं) के निर्माण की अनुमति देते हैं। अब जब प्रमाण का आकार ज्ञात हो गया है, तो कोई पहले से ही एक प्रकार के अनुमान एल्गोरिदम को तैयार करने के करीब है। चूँकि किसी दिए गए अभिव्यक्ति के लिए किसी भी प्रमाण का एक ही आकार होना चाहिए, कोई भी प्रमाण के निर्णयों में मोनोटाइप को अनिर्धारित मान सकता है और विचार कर सकता है कि उन्हें कैसे निर्धारित किया जाए। यहाँ, प्रतिस्थापन (विशेषज्ञता) क्रम लागू होता है। हालांकि पहली नज़र में कोई भी स्थानीय रूप से प्रकारों का निर्धारण नहीं कर सकता है, उम्मीद है कि प्रूफ ट्री को पार करते समय क्रम की मदद से उन्हें परिष्कृत करना संभव है, अतिरिक्त रूप से यह मानते हुए कि परिणामी एल्गोरिथ्म एक अनुमान विधि बनने वाली है, कि किसी भी आधार में प्रकार को सर्वोत्तम संभव के रूप में निर्धारित किया जाएगा। और वास्तव में, जैसा कि सुझावों के नियमों को देखते हुए कहा जा सकता हैः महत्वपूर्ण विकल्प है। इस बिंदु पर, इसके बारे में कुछ भी ज्ञात नहीं है, इसलिए कोई केवल सबसे सामान्य प्रकार को मान सकता है, जो है। यदि आवश्यक हो जाए तो इस प्रकार को विशेषज्ञ बनाने की योजना है। दुर्भाग्य से, इस स्थान पर एक पॉलीटाइप की अनुमति नहीं है, इसलिए कुछ को अभी के लिए करना पड़ता है। अवांछित कैप्चर से बचने के लिए, एक प्रकार चर जो अभी तक प्रमाण में नहीं है, एक सुरक्षित विकल्प है। इसके अतिरिक्त, यह ध्यान रखना होगा कि यह मोनोटाइप अभी तक तय नहीं हुआ है, लेकिन इसे और परिष्कृत किया जा सकता है। : चुनाव यह है कि कैसे परिष्कृत किया जाए। क्योंकि यहाँ किसी भी प्रकार का कोई भी विकल्प चर के उपयोग पर निर्भर करता है, जो स्थानीय रूप से ज्ञात नहीं है, सबसे सुरक्षित शर्त सबसे सामान्य है। ऊपर के समान विधि का उपयोग करके सभी मात्रात्मक चरों को नए मोनोटाइप चरों के साथ तुरंत प्रमाणित किया जा सकता है, जिससे उन्हें आगे के परिष्करण के लिए खुला रखा जा सकता है। : नियम कोई विकल्प नहीं छोड़ता है। हो गया। : केवल आवेदन नियम दोनों परिसरों द्वारा आवश्यक रूप से अब तक "खोले गए" चर को परिष्कृत करने के लिए मजबूर कर सकता है। पहला आधार अनुमान के परिणाम को उस रूप में होने के लिए मजबूर करता है। अगर ऐसा है तो ठीक है। कोई भी बाद में परिणाम के लिए इसे चुन सकता है। यदि नहीं, तो यह एक खुला चर हो सकता है। फिर इसे पहले की तरह दो नए चर के साथ आवश्यक रूप में परिष्कृत किया जा सकता है। अन्यथा, प्रकार जाँच विफल हो जाती है क्योंकि पहला आधार एक प्रकार का अनुमान लगाता है जिसे कार्य प्रकार में नहीं बनाया जा सकता है। दूसरे आधार के लिए आवश्यक है कि अनुमानित प्रकार पहले आधार के बराबर हो। अब दो संभवतः अलग-अलग प्रकार हैं, शायद खुले प्रकार के चर के साथ, तुलना करने के लिए और यदि संभव हो तो बराबर करने के लिए। यदि ऐसा है, तो एक परिष्करण पाया जाता है, और यदि नहीं, तो फिर से एक प्रकार की त्रुटि का पता लगाया जाता है। एक प्रभावी विधि को प्रतिस्थापन द्वारा "दो शब्दों को बराबर बनाने" के लिए जाना जाता है, तथाकथित यूनियन-फाइंड एल्गोरिदम के संयोजन में रॉबिन्सन का एकीकरण। संघ-खोज एल्गोरिदम को संक्षेप में संक्षेप में प्रस्तुत करने के लिए, एक प्रमाण में सभी प्रकारों के समूह को देखते हुए, यह एक प्रक्रिया के माध्यम से उन्हें समतुल्य वर्गों में एक साथ समूहित करने और एक प्रक्रिया का उपयोग करके ऐसे प्रत्येक वर्ग के लिए एक प्रतिनिधि चुनने की अनुमति देता है। दुष्प्रभाव के अर्थ में प्रक्रिया शब्द पर जोर देते हुए, हम स्पष्ट रूप से एक प्रभावी एल्गोरिथ्म तैयार करने के लिए तर्क के क्षेत्र को छोड़ रहे हैं। a का प्रतिनिधि इस तरह से निर्धारित किया जाता है कि, यदि दोनों और प्रकार चर हैं तो प्रतिनिधि मनमाने ढंग से उनमें से एक है, लेकिन एक चर और एक शब्द को एकजुट करते समय, शब्द प्रतिनिधि बन जाता है। हाथ में यूनियन-फाइंड के कार्यान्वयन को मानते हुए, कोई भी दो मोनोटाइप के एकीकरण को निम्नानुसार तैयार कर सकता हैः यूनिफाई (ta, tb): ta = फाइंड (ta) tb = फाइंड (tb) यदि दोनों ta, tb समान D, n के साथ फॉर्म D p1.pn के शब्द हैं तो प्रत्येक संबंधित ith पैरामीटर के लिए यूनिफाई (ta [i], tb [i]) करें अन्यथा यदि ta, tb में से कम से कम एक प्रकार चर है तो यूनियन (ta, tb) अन्यथा त्रुटि 'प्रकार मेल नहीं खाते हैं' अब हाथ में एक अनुमान एल्गोरिदम का स्केच होने पर, अगले खंड में अधिक औपचारिक प्रस्तुति दी जाती है। इसका वर्णन मिलनर पी. 370 एफ. एफ. में किया गया है। एल्गोरिदम जे. एल्गोरिदम जे. एल्गोरिदम जे. की प्रस्तुति तार्किक नियमों के संकेतन का दुरुपयोग है, क्योंकि इसमें दुष्प्रभाव शामिल हैं लेकिन एक ही समय में एक कुशल कार्यान्वयन को व्यक्त करते हुए एक सीधी तुलना की अनुमति देता है। नियम अब उस निष्कर्ष पर पहुंचने वाले मापदंडों के साथ एक प्रक्रिया को निर्दिष्ट करते हैं जहां परिसर का निष्पादन बाएं से दाएं की ओर होता है। प्रक्रिया पॉलीटाइप को शब्द की प्रतिलिपि बनाकर और नए मोनोटाइप चर द्वारा लगातार बाध्य प्रकार चर को प्रतिस्थापित करके विशेषज्ञता प्रदान करती है। एक नया मोनोटाइप चर उत्पन्न करता है। संभवतः, अवांछित ग्रहण से बचने के लिए परिमाणीकरण के लिए नए चर पेश करने वाले प्रकार की प्रतिलिपि बनानी होगी। कुल मिलाकर, एल्गोरिथ्म अब हमेशा एकीकरण के लिए विशेषज्ञता को छोड़कर सबसे सामान्य विकल्प बनाकर आगे बढ़ता है, जो अपने आप में सबसे सामान्य परिणाम उत्पन्न करता है। जैसा कि ऊपर उल्लेख किया गया है, किसी दिए गए अभिव्यक्ति के लिए सबसे सामान्य प्रकार प्राप्त करने के लिए अंतिम परिणाम को अंत में सामान्यीकृत करना होगा। क्योंकि एल्गोरिथ्म में उपयोग की जाने वाली प्रक्रियाओं की लागत लगभग ओ (1) है, एल्गोरिथ्म की समग्र लागत अभिव्यक्ति के आकार में रैखिक के करीब है जिसके लिए एक प्रकार का अनुमान लगाया जाना है। यह प्रकार अनुमान एल्गोरिदम प्राप्त करने के कई अन्य प्रयासों के विपरीत है, जो अक्सर एनपी-हार्ड के रूप में सामने आते हैं, यदि समाप्ति के संबंध में अनिश्चित नहीं हैं। इस प्रकार एच. एम. प्रदर्शन करता है और साथ ही सबसे अच्छा पूरी तरह से सूचित प्रकार-जाँच एल्गोरिदम कर सकता है। यहाँ टाइप-चेकिंग का मतलब है कि एक एल्गोरिथ्म को एक प्रमाण खोजने की आवश्यकता नहीं है, बल्कि केवल एक दिए गए प्रमाण को मान्य करने के लिए है। दक्षता थोड़ी कम हो जाती है क्योंकि संदर्भ में प्रकार चर के बंधन को बनाए रखना पड़ता है ताकि गणना की अनुमति दी जा सके और इस दौरान पुनरावर्ती प्रकारों के निर्माण को रोकने के लिए एक घटना की जांच को सक्षम किया जा सके। ऐसे मामले का एक उदाहरण है, जिसके लिए एच. एम. का उपयोग करके कोई प्रकार प्राप्त नहीं किया जा सकता है। व्यावहारिक रूप से, प्रकार केवल छोटे शब्द हैं और विस्तार संरचनाओं का निर्माण नहीं करते हैं। इस प्रकार, जटिलता विश्लेषण में, उनकी तुलना को एक स्थिर, ओ (1) लागत को बनाए रखने के रूप में माना जा सकता है। एल्गोरिदम को साबित करना पिछले खंड में, एल्गोरिदम को स्केच करते समय इसके प्रमाण को धातुशास्त्रीय तर्क के साथ संकेत दिया गया था। जबकि यह एक कुशल एल्गोरिथ्म जे की ओर ले जाता है, यह स्पष्ट नहीं है कि क्या एल्गोरिथ्म डिडक्शन सिस्टम डी या एस को ठीक से दर्शाता है जो एक शब्दार्थ आधार रेखा के रूप में काम करता है। उपरोक्त तर्क में सबसे महत्वपूर्ण बिंदु संदर्भ से बंधे मोनोटाइप चर का परिष्करण है। उदाहरण के लिए, एल्गोरिथ्म साहसपूर्वक अनुमान लगाते हुए संदर्भ को बदल देता है। , क्योंकि पैरामीटर के संदर्भ में जोड़े गए मोनोटाइप चर को बाद में अनुप्रयोग को संभालते समय परिष्कृत करने की आवश्यकता होती है। समस्या यह है कि कटौती नियम इस तरह के परिष्करण की अनुमति नहीं देते हैं। यह तर्क देना कि परिष्कृत प्रकार को मोनोटाइप चर के बजाय पहले जोड़ा जा सकता था, सबसे अच्छा है। एक औपचारिक रूप से संतोषजनक तर्क तक पहुँचने की कुंजी परिष्करण के भीतर संदर्भ को ठीक से शामिल करना है। औपचारिक रूप से, टाइपिंग मुक्त प्रकार चर के प्रतिस्थापन के साथ संगत है। इस प्रकार मुक्त चर को परिष्कृत करने का अर्थ है पूरी टाइपिंग को परिष्कृत करना। एल्गोरिदम डब्ल्यू वहाँ से, एल्गोरिदम जे का एक प्रमाण एल्गोरिदम डब्ल्यू की ओर ले जाता है, जो केवल प्रतिस्थापन के माध्यम से अपनी क्रमिक संरचना को व्यक्त करके प्रक्रिया द्वारा लगाए गए दुष्प्रभावों को स्पष्ट करता है। साइडबार में एल्गोरिथ्म डब्ल्यू की प्रस्तुति अभी भी इटैलिक में सेट किए गए कार्यों में दुष्प्रभावों का उपयोग करती है, लेकिन ये अब नए प्रतीकों को उत्पन्न करने तक सीमित हैं। निर्णय का रूप है, एक संदर्भ और अभिव्यक्ति के साथ एक फ़ंक्शन को एक प्रतिस्थापन के साथ एक मोनोटाइप का उत्पादन करने वाले पैरामीटर के रूप में दर्शाना। एक प्रतिस्थापन के उत्पादन का एक दुष्प्रभाव मुक्त संस्करण है जो सबसे सामान्य एकीकरणकर्ता है। जबकि एल्गोरिथ्म डब्ल्यू को आम तौर पर एच. एम. एल्गोरिथ्म माना जाता है और अक्सर साहित्य में नियम प्रणाली के बाद सीधे प्रस्तुत किया जाता है, इसका उद्देश्य पी. 369 पर मिलनर द्वारा इस प्रकार वर्णित किया गया हैः जैसा कि यह खड़ा है, डब्ल्यू शायद ही एक कुशल एल्गोरिथ्म है; प्रतिस्थापन बहुत बार लागू किए जाते हैं। इसे स्वस्थता के प्रमाण में सहायता के लिए तैयार किया गया था। अब हम एक सरल एल्गोरिथ्म जे प्रस्तुत करते हैं जो एक सटीक अर्थ में डब्ल्यू का अनुकरण करता है। जबकि वे डब्ल्यू को अधिक जटिल और कम कुशल मानते थे, उन्होंने इसे जे के सामने अपने प्रकाशन में प्रस्तुत किया। जब दुष्प्रभाव अनुपलब्ध या अवांछित होते हैं तो इसके अपने फायदे होते हैं। डब्ल्यू को पूर्णता साबित करने के लिए भी आवश्यक है, जिसे उसके द्वारा ध्वनि प्रमाण में शामिल किया जाता है। प्रमाण दायित्वों को तैयार करने से पहले, नियम प्रणाली डी और एस और प्रस्तुत एल्गोरिदम के बीच एक विचलन पर जोर देने की आवश्यकता है। जबकि उपरोक्त विकास ने "ओपन" प्रूफ चर के रूप में मोनोटाइप का दुरुपयोग किया, इस संभावना को कि उचित मोनोटाइप चर को नुकसान हो सकता है, नए चर पेश करके और सर्वश्रेष्ठ की उम्मीद करके दरकिनार कर दिया गया। लेकिन एक पकड़ हैः किए गए वादों में से एक यह था कि इन नए चर को "ध्यान में रखा जाएगा"। यह वादा एल्गोरिथ्म द्वारा पूरा नहीं किया जाता है। एक संदर्भ होने के कारण, अभिव्यक्ति को या तो टाइप नहीं किया जा सकता है, लेकिन एल्गोरिदम उस प्रकार के साथ आते हैं, जहां डब्ल्यू अतिरिक्त रूप से प्रतिस्थापन प्रदान करता है, जिसका अर्थ है कि एल्गोरिदम सभी प्रकार की त्रुटियों का पता लगाने में विफल रहता है। इस चूक को अधिक सावधानीपूर्वक प्रूफ चर और मोनोटाइप चर को अलग करके आसानी से ठीक किया जा सकता है। लेखक समस्या के बारे में अच्छी तरह से जानते थे लेकिन उन्होंने इसे ठीक नहीं करने का फैसला किया। इसके पीछे कोई व्यावहारिक कारण हो सकता है। जबकि प्रकार अनुमान को अधिक ठीक से लागू करने से एल्गोरिथ्म को अमूर्त मोनोटाइप से निपटने में सक्षम बनाया जा सकता था, वे इच्छित अनुप्रयोग के लिए आवश्यक नहीं थे जहां पहले से मौजूद संदर्भ में किसी भी वस्तु में मुक्त चर नहीं होते हैं। इस प्रकाश में, एक सरल एल्गोरिथ्म के पक्ष में अनावश्यक जटिलता को हटा दिया गया था। शेष नकारात्मक पक्ष यह है कि नियम प्रणाली के संबंध में एल्गोरिथ्म का प्रमाण कम सामान्य है और केवल एक साइड कंडीशन के साथ संदर्भों के लिए बनाया जा सकता है। पूर्णता दायित्व में साइड कंडीशन यह बताती है कि कटौती कैसे कई प्रकार दे सकती है, जबकि एल्गोरिथ्म हमेशा एक का उत्पादन करता है। साथ ही, साइड कंडीशन की मांग है कि अनुमानित प्रकार वास्तव में सबसे सामान्य है। दायित्वों को ठीक से साबित करने के लिए पहले उन्हें मजबूत करने की आवश्यकता होती है ताकि और के माध्यम से प्रतिस्थापन को थ्रेडिंग करने वाले प्रतिस्थापन लेम्मा को सक्रिय करने की अनुमति दी जा सके। वहाँ से, प्रमाण अभिव्यक्ति पर प्रेरण द्वारा होते हैं। एक अन्य प्रमाण दायित्व स्वयं प्रतिस्थापन लेम्मा है, अर्थात। टाइपिंग का प्रतिस्थापन, जो अंत में सभी-मात्रा को स्थापित करता है। बाद वाले को औपचारिक रूप से साबित नहीं किया जा सकता है, क्योंकि ऐसा कोई वाक्यविन्यास हाथ में नहीं है। विस्तार पुनरावर्ती परिभाषाएँ प्रोग्रामिंग को व्यावहारिक पुनरावर्ती कार्य बनाने के लिए आवश्यक हैं। लैम्ब्डा कलन का एक केंद्रीय गुण यह है कि पुनरावर्ती परिभाषाएँ सीधे उपलब्ध नहीं हैं, लेकिन इसके बजाय एक निश्चित बिंदु संयोजक के साथ व्यक्त की जा सकती हैं। लेकिन दुर्भाग्य से, फिक्सप्वाइंट संयोजक को नीचे उल्लिखित प्रणाली पर विनाशकारी प्रभाव डाले बिना लैम्ब्डा कलन के टाइप किए गए संस्करण में तैयार नहीं किया जा सकता है। टाइपिंग नियम मूल पेपर दिखाता है कि रिकर्शन को एक संयोजक द्वारा महसूस किया जा सकता है। एक संभावित पुनरावर्ती परिभाषा इस प्रकार तैयार की जा सकती है। वैकल्पिक रूप से अभिव्यक्ति वाक्यविन्यास का एक विस्तार और एक अतिरिक्त टाइपिंग नियम संभव हैः जहां मूल रूप से विलय होता है और मोनोटाइप स्थितियों में पुनरावर्ती रूप से परिभाषित चर को शामिल करते हुए जहां वे इसके बाईं ओर होते हैं लेकिन इसके दाईं ओर पॉलीटाइप के रूप में होते हैं। परिणाम जबकि उपरोक्त सीधा है, यह एक कीमत पर आता है। प्रकार सिद्धांत लैम्ब्डा कलन को गणना और तर्क से जोड़ता है। ऊपर दिए गए आसान संशोधन का दोनों पर प्रभाव पड़ता हैः मजबूत सामान्यीकरण गुण अमान्य है, क्योंकि गैर-समाप्ति शर्तों को तैयार किया जा सकता है। तर्क ध्वस्त हो जाता है क्योंकि प्रकार आबाद हो जाता है। ओवरलोडिंग का मतलब है कि एक ही नाम के साथ विभिन्न कार्यों को परिभाषित और उपयोग किया जा सकता है। अधिकांश प्रोग्रामिंग भाषाएँ कम से कम अंतर्निहित अंकगणितीय संचालन (+, <, आदि) के साथ अधिभार प्रदान करती हैं। ), प्रोग्रामर को एक ही रूप में अंकगणितीय अभिव्यक्तियों को लिखने की अनुमति देने के लिए, यहां तक कि विभिन्न संख्यात्मक प्रकारों जैसे इंट या रियल के लिए भी। क्योंकि एक ही अभिव्यक्ति के भीतर इन विभिन्न प्रकारों का मिश्रण भी अंतर्निहित रूपांतरण की मांग करता है, विशेष रूप से इन कार्यों के लिए अतिभारण को अक्सर प्रोग्रामिंग भाषा में ही बनाया जाता है। कुछ भाषाओं में, इस सुविधा को सामान्यीकृत किया जाता है और उपयोगकर्ता के लिए उपलब्ध कराया जाता है, जैसे। सी + + में। जबकि प्रकार जाँच और अनुमान दोनों में गणना लागतों के लिए कार्यात्मक प्रोग्रामिंग में तदर्थ अतिभारण से बचा गया है, अतिभारण को व्यवस्थित करने का एक साधन पेश किया गया है जो रूप और नाम दोनों में ऑब्जेक्ट ओरिएंटेड प्रोग्रामिंग से मिलता-जुलता है, लेकिन एक स्तर ऊपर की ओर काम करता है। इस प्रणाली में "उदाहरण" वस्तु नहीं हैं (अर्थात। मूल्य स्तर पर), बल्कि प्रकार। परिचय में उल्लिखित क्विकसोर्ट उदाहरण आदेशों में अधिभार का उपयोग करता है, जिसमें हास्केल में निम्नलिखित प्रकार की एनोटेशन होती हैः क्विकसोर्टःः ऑर्ड a => [a]-> [a] यहाँ, प्रकार a न केवल बहुरूपी है, बल्कि किसी प्रकार के वर्ग ऑर्ड का एक उदाहरण होने के लिए भी प्रतिबंधित है, जो फ़ंक्शन बॉडी में उपयोग किए जाने वाले क्रम <और> = को प्रदान करता है। जैसे ही अधिक ठोस प्रकारों पर क्विकसोर्ट का उपयोग किया जाता है, इन विधेयकों के उचित कार्यान्वयन को अतिरिक्त मापदंडों के रूप में क्विकसोर्ट को पारित किया जाता है, जो ओवरलोडेड फ़ंक्शन क्विकसोर्ट का एकल कार्यान्वयन प्रदान करता है। क्योंकि "वर्ग" केवल एक ही प्रकार को अपने तर्क के रूप में अनुमति देते हैं, परिणामी प्रकार प्रणाली अभी भी अनुमान प्रदान कर सकती है। इसके अतिरिक्त, प्रकार वर्गों को तब किसी प्रकार के अधिभार आदेश से सुसज्जित किया जा सकता है जिससे कक्षाओं को जाली के रूप में व्यवस्थित किया जा सकता है। उच्च-क्रम प्रकार पैरामीट्रिक बहुरूपता का तात्पर्य है कि प्रकारों को स्वयं मापदंडों के रूप में पारित किया जाता है जैसे कि वे उचित मूल्य थे। एक उचित कार्य के लिए तर्क के रूप में पारित किया जाता है, लेकिन "पैरामीट्रिक" प्रकार स्थिरांक के रूप में "प्रकार कार्य" में भी, इस सवाल की ओर ले जाता है कि स्वयं को अधिक ठीक से टाइप कैसे किया जाए। उच्च-क्रम प्रकारों का उपयोग और भी अधिक अभिव्यंजक प्रकार प्रणाली बनाने के लिए किया जाता है। दुर्भाग्य से, एकीकरण अब मेटा प्रकारों की उपस्थिति में निर्णायक नहीं है, जिससे सामान्यता के इस विस्तार में प्रकार का अनुमान असंभव हो जाता है। इसके अतिरिक्त, सभी प्रकारों के एक प्रकार को मानते हुए जो खुद को एक प्रकार के रूप में शामिल करता है, एक विरोधाभास की ओर ले जाता है, जैसा कि सभी सेटों के सेट में होता है, इसलिए किसी को अमूर्तता के स्तरों के चरणों में आगे बढ़ना चाहिए। दूसरे क्रम के लैम्ब्डा कलन में एक कदम ऊपर की ओर किए गए शोध से पता चला है कि इस प्रकार का अनुमान इस व्यापकता में अनिश्चित है। हास्केल नामक प्रकार में एक अतिरिक्त स्तर के कुछ हिस्सों को शामिल किया गया है, जहां इसका उपयोग मोनाड टाइप करने में मदद करने के लिए किया जाता है। प्रकारों को अंतर्निहित छोड़ दिया जाता है, जो विस्तारित प्रकार प्रणाली के आंतरिक यांत्रिकी में पर्दे के पीछे काम करते हैं। उपप्रकार और प्रकार अनुमान को संयोजित करने के प्रयासों ने काफी निराशा पैदा की है। उपप्रकार बाधाओं को जमा करना और प्रचारित करना (प्रकार समानता बाधाओं के विपरीत) सीधा है, जिससे परिणामी बाधाएं अनुमानित टाइपिंग योजनाओं का हिस्सा बन जाती हैं, उदाहरण के लिए, जहां प्रकार चर पर एक बाधा है। हालाँकि, क्योंकि प्रकार चर अब इस दृष्टिकोण में उत्सुकता से एकीकृत नहीं हैं, यह कई बेकार प्रकार चर और बाधाओं वाली बड़ी और भारी टाइपिंग योजनाओं को उत्पन्न करता है, जिससे उन्हें पढ़ना और समझना मुश्किल हो जाता है। इसलिए, गैर-निर्धारक सीमित स्वचालित (एन. एफ. ए.) सरलीकरण (अनुमानित पुनरावर्ती प्रकारों की उपस्थिति में उपयोगी) के समान तकनीकों का उपयोग करके ऐसी टाइपिंग योजनाओं और उनकी बाधाओं को सरल बनाने के लिए काफी प्रयास किए गए। हाल ही में, डोलन और माइक्रॉफ्ट ने टाइपिंग योजना सरलीकरण और एन. एफ. ए. सरलीकरण के बीच संबंध को औपचारिक रूप दिया और दिखाया कि उपप्रकार के औपचारिकरण पर एक बीजगणितीय लेने से एम. एल. जैसी भाषा (जिसे एम. एल. सब कहा जाता है) के लिए कॉम्पैक्ट प्रिंसिपल टाइपिंग योजनाओं को उत्पन्न करने की अनुमति मिली। विशेष रूप से, उनकी प्रस्तावित टाइपिंग योजना में स्पष्ट बाधाओं के बजाय संघ और प्रतिच्छेदन प्रकारों के एक प्रतिबंधित रूप का उपयोग किया गया था। पेरो ने बाद में दावा किया कि यह बीजगणितीय सूत्रीकरण एल्गोरिदम डब्ल्यू के समान एक अपेक्षाकृत सरल एल्गोरिदम के बराबर था, और संघ और प्रतिच्छेदन प्रकारों का उपयोग आवश्यक नहीं था। दूसरी ओर, ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग भाषाओं के संदर्भ में प्रकार का अनुमान अधिक कठिन साबित हुआ है, क्योंकि ऑब्जेक्ट विधियों के लिए सिस्टम एफ की शैली में प्रथम श्रेणी के बहुरूपता की आवश्यकता होती है (जहां प्रकार का अनुमान अनिश्चित है) और एफ-बाउंडेड बहुरूपता जैसी विशेषताओं के कारण। नतीजतन, ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग को सक्षम करने वाले सबटाइपिंग के साथ टाइप सिस्टम, जैसे कि कार्डेली का सिस्टम, एचएम-स्टाइल प्रकार के अनुमान का समर्थन नहीं करता है। पंक्ति बहुरूपता का उपयोग संरचनात्मक अभिलेखों जैसी भाषा विशेषताओं का समर्थन करने के लिए उपप्रकार के विकल्प के रूप में किया जा सकता है। हालांकि बहुरूपता की यह शैली कुछ तरीकों से उपप्रकार की तुलना में कम लचीली है, विशेष रूप से प्रकार की बाधाओं में दिशात्मकता की कमी से निपटने के लिए सख्ती से आवश्यक अधिक बहुरूपता की आवश्यकता होती है, इसका लाभ यह है कि इसे मानक एच. एम. एल्गोरिदम के साथ काफी आसानी से एकीकृत किया जा सकता है। नोट्स संदर्भ बाहरी लिंक गिटहब पर अपने स्रोत कोड के साथ एल्गोरिदम डब्ल्यू का एक साक्षर हास्केल कार्यान्वयन। पायथन में हिंडले-मिलनर एल्गोरिदम का एक सरल कार्यान्वयन। प्रकार प्रणाली प्रकार सिद्धांत प्रकार अनुमान लैम्ब्डा कलन सैद्धांतिक कंप्यूटर विज्ञान औपचारिक तरीके 1969 संगणना में 1978 संगणना में 1985 संगणना एल्गोरिदम में