हिंडले-मिलनर टाइप सिस्टम

	Expressions
	Types
	Context and Typing
	Free Type Variables

हिंडले-मिलनर (एचएम) प्रकार प्रणाली प्राचलिक बहुरूपता के साथ लैम्ब्डा कैलकुलस के लिए चिरसम्मत प्रकार की प्रणाली है। इसे दमास-मिलनर या दमास-हिंडले-मिलनर के नाम से भी जाना जाता है। इसका वर्णन सबसे पहले जे. रोजर हिंडले ने किया था^[1] और बाद में रॉबिन मिलनर द्वारा पुनः खोजा गया था।^[2] लुइस दामास ने अपनी पीएचडी थीसिस में विधि का एक करीबी औपचारिक विश्लेषण और प्रमाण दिया।^[3]^[4] एचएम के अधिक उल्लेखनीय गुणों में इसकी पूर्णता (तर्क) और प्रोग्रामर द्वारा प्रदत्त प्रकार के एनोटेशन या अन्य संकेतों के बिना किसी दिए गए प्रोग्राम के प्रमुख प्रकार का अनुमान लगाने की क्षमता है। #एल्गोरिदम डब्ल्यू व्यवहार में एक कुशल प्रकार की अनुमान विधि है और इसे बड़े कोड आधारों पर सफलतापूर्वक लागू किया गया है, हालांकि इसमें उच्च सैद्धांतिक कम्प्यूटेशनल जटिलता है।^{[note 1]} एचएम का उपयोग अधिमानतः कार्यात्मक भाषाओं के लिए किया जाता है। इसे सबसे पहले प्रोग्रामिंग भाषा एमएल (प्रोग्रामिंग भाषा) के टाइप सिस्टम के हिस्से के रूप में लागू किया गया था। तब से, एचएम को विभिन्न तरीकों से विस्तारित किया गया है, विशेष रूप से हास्केल (प्रोग्रामिंग भाषा) जैसे प्रकार वर्ग की बाधाओं के साथ।

परिचय

एक प्रकार की अनुमान विधि के रूप में, हिंडले-मिलनर पूरी तरह से अलिखित शैली में लिखे गए कार्यक्रमों से चर, अभिव्यक्ति और कार्यों के प्रकारों को निकालने में सक्षम है। स्कोप (कंप्यूटर विज्ञान) संवेदनशील होने के कारण, यह केवल स्रोत कोड के एक छोटे हिस्से से प्रकार प्राप्त करने तक सीमित नहीं है, बल्कि संपूर्ण प्रोग्राम या मॉड्यूल से प्राप्त होता है। प्राचलिक बहुरूपता से निपटने में सक्षम होने के कारण, यह कई कार्यात्मक प्रोग्रामिंग भाषाओं की प्रकार प्रणालियों का मूल है। इसे सबसे पहले इस तरीके से ML (प्रोग्रामिंग लैंग्वेज) प्रोग्रामिंग लैंग्वेज में लागू किया गया था।

मूल सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस के लिए प्रकार अनुमान एल्गोरिदम है जिसे 1958 में हास्केल करी और रॉबर्ट फेयस द्वारा तैयार किया गया था।^{[citation needed]} 1969 में, जे. रोजर हिंडले ने इस काम को आगे बढ़ाया और साबित किया कि उनका एल्गोरिदम हमेशा सबसे सामान्य प्रकार का अनुमान लगाता है। 1978 में, रॉबिन मिलनर,^[5] हिंडले के काम से स्वतंत्र, एक समतुल्य एल्गोरिदम, #एल्गोरिदम डब्ल्यू प्रदान किया गया। 1982 में, लुई दामास^[4]अंततः साबित हुआ कि मिलनर का एल्गोरिदम पूर्ण है और इसे बहुरूपी संदर्भों वाले सिस्टम का समर्थन करने के लिए विस्तारित किया गया है।

एकरूपता बनाम बहुरूपता

सरलता से टाइप किए गए लैम्ब्डा कैलकुलस में, प्रकार $T$ या तो परमाणु प्रकार के स्थिरांक हैं या कार्य प्रकार के रूप हैं $T\rightarrow T$ . ऐसे प्रकार मोनोमोर्फिक होते हैं। विशिष्ट उदाहरण अंकगणितीय मानों में प्रयुक्त प्रकार हैं:

 3 : संख्या
 3 4 जोड़ें : संख्या
 जोड़ें : संख्या -> संख्या -> संख्या

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

id ≡ λ x . एक्स

जो जिस भी मूल्य पर लागू होता है, उसे वापस लौटा देता है। कम तुच्छ उदाहरणों में सूची (कंप्यूटर विज्ञान) जैसे पैरामीट्रिक प्रकार शामिल हैं।

जबकि सामान्य तौर पर बहुरूपता का अर्थ है कि ऑपरेशन एक से अधिक प्रकार के मूल्यों को स्वीकार करते हैं, यहां प्रयुक्त बहुरूपता पैरामीट्रिक है। साहित्य में प्रकार की योजनाओं का उल्लेख भी मिलता है, जो बहुरूपता की पैरामीट्रिक प्रकृति पर जोर देता है। इसके अतिरिक्त, स्थिरांक को (मात्राबद्ध) प्रकार के चर के साथ टाइप किया जा सकता है। जैसे:

 विपक्ष : कुल मिलाकर ए . ए -> सूची ए -> सूची ए
 शून्य : कुल मिलाकर ए . सूची ए
 आईडी : सभी के लिए ए . ए -> ए

बहुरूपी प्रकार अपने चरों के लगातार प्रतिस्थापन से मोनोमोर्फिक बन सकते हैं। मोनोमोर्फिक उदाहरणों के उदाहरण हैं:

आईडी': स्ट्रिंग -> स्ट्रिंग
शून्य' : सूची संख्या

अधिक आम तौर पर, प्रकार बहुरूपी होते हैं जब उनमें प्रकार चर होते हैं, जबकि उनके बिना प्रकार मोनोमोर्फिक होते हैं।

उदाहरण के लिए पास्कल (प्रोग्रामिंग भाषा) (1970) या सी (प्रोग्रामिंग भाषा) (1972) में प्रयुक्त प्रकार प्रणालियों के विपरीत, जो केवल मोनोमोर्फिक प्रकारों का समर्थन करते हैं, एचएम को प्राचलिक बहुरूपता पर जोर देने के साथ डिजाइन किया गया है। उल्लिखित भाषाओं के उत्तराधिकारी, जैसे C++ (1985), विभिन्न प्रकार के बहुरूपता पर ध्यान केंद्रित करते हैं, अर्थात् बहुरूपता (कंप्यूटर विज्ञान)#ऑब्जेक्ट ओरिएंटेड प्रोग्रामिंग और बहुरूपता (कंप्यूटर विज्ञान)#तदर्थ बहुरूपता के संबंध में उपप्रकार। जबकि उपटाइपिंग एचएम के साथ असंगत है, हास्केल के एचएम-आधारित प्रकार प्रणाली में व्यवस्थित ओवरलोडिंग का एक प्रकार उपलब्ध है।

मान लीजिए-बहुरूपता

सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस के प्रकार के अनुमान को बहुरूपता की ओर विस्तारित करते समय, किसी को यह परिभाषित करना होगा कि किसी मान का उदाहरण प्राप्त करना कब स्वीकार्य है। आदर्श रूप से, किसी बाध्य चर के किसी भी उपयोग के साथ इसकी अनुमति दी जाएगी, जैसे:

 (λ आईडी... (आईडी 3)... (आईडी टेक्स्ट)...) (λ x. x)

दुर्भाग्य से, सिस्टम एफ में प्रकार का अनुमान निर्णय योग्य नहीं है।^[6] इसके बजाय, एचएम फॉर्म का लेट-पॉलीमोर्फिज्म प्रदान करता है

 'चलो' आईडी = λ एक्स। एक्स
  'इन'... (आईडी 3) ... (आईडी टेक्स्ट) ...

अभिव्यक्ति सिंटैक्स के विस्तार में बाइंडिंग तंत्र को प्रतिबंधित करना। केवल लेट निर्माण में बंधे मान तात्कालिकता के अधीन हैं, यानी बहुरूपी हैं, जबकि लैम्ब्डा-अमूर्त में मापदंडों को मोनोमोर्फिक माना जाता है।

सिंहावलोकन

इस लेख का शेष भाग इस प्रकार है:

एचएम प्रकार प्रणाली परिभाषित की गई है। यह एक कटौती प्रणाली का वर्णन करके किया जाता है जो सटीक बनाता है कि कौन से भाव किस प्रकार के हैं, यदि कोई हो।
वहां से, यह प्रकार अनुमान विधि के कार्यान्वयन की दिशा में काम करता है। उपरोक्त निगमनात्मक प्रणाली का वाक्य-विन्यास-संचालित संस्करण पेश करने के बाद, यह एक कुशल कार्यान्वयन (एल्गोरिदम जे) का रेखाचित्र बनाता है, जो पाठक के धातु संबंधी अंतर्ज्ञान को आकर्षित करता है।
क्योंकि यह खुला रहता है कि क्या एल्गोरिदम जे वास्तव में प्रारंभिक कटौती प्रणाली का एहसास करता है, एक कम कुशल कार्यान्वयन (एल्गोरिदम डब्ल्यू) पेश किया जाता है और प्रमाण में इसके उपयोग का संकेत दिया जाता है।
अंत में, एल्गोरिथम से संबंधित अन्य विषयों पर चर्चा की गई है।

कटौती प्रणाली का एक ही विवरण, यहां तक कि दो एल्गोरिदम के लिए भी उपयोग किया जाता है, ताकि एचएम पद्धति को प्रस्तुत किए जाने वाले विभिन्न रूपों को सीधे तुलनीय बनाया जा सके।

हिंडले-मिलनर प्रकार प्रणाली

प्रकार प्रणाली को औपचारिक व्याकरण द्वारा औपचारिक रूप से वर्णित किया जा सकता है जो अभिव्यक्तियों, प्रकारों आदि के लिए एक भाषा तय करता है। इस तरह के वाक्यविन्यास की यहां प्रस्तुति बहुत औपचारिक नहीं है, इसमें इसे पार्स पेड़ का अध्ययन करने के लिए नहीं लिखा गया है, बल्कि सार वाक्यविन्यास, और कुछ वाक्यात्मक विवरण खुला छोड़ देता है। प्रस्तुति का यह रूप सामान्य है. इसके आधार पर, टाइपिंग नियमों का उपयोग यह परिभाषित करने के लिए किया जाता है कि अभिव्यक्ति और प्रकार कैसे संबंधित हैं। पहले की तरह, इस्तेमाल किया गया फॉर्म थोड़ा उदार है।

सिंटेक्स

टाइप किए जाने वाले भाव बिल्कुल लैम्ब्डा कैलकुलस के समान हैं जिन्हें लेट-एक्सप्रेशन के साथ विस्तारित किया गया है जैसा कि आसन्न तालिका में दिखाया गया है। किसी अभिव्यक्ति को स्पष्ट करने के लिए कोष्ठक का उपयोग किया जा सकता है। एप्लिकेशन लेफ्ट-बाइंडिंग है और एब्स्ट्रैक्शन या लेट-इन कंस्ट्रक्शन की तुलना में अधिक मजबूती से बांधता है।

प्रकारों को वाक्यात्मक रूप से दो समूहों, मोनोटाइप्स और पॉलीटाइप्स में विभाजित किया गया है।^{[note 2]}

मोनोटाइप्स

मोनोटाइप हमेशा एक विशेष प्रकार को निर्दिष्ट करते हैं। मोनोटाइप्स $\tau$ वाक्यात्मक रूप से टर्म (तर्क) के रूप में दर्शाया जाता है।

मोनोटाइप के उदाहरणों में प्रकार स्थिरांक शामिल हैं ${\mathtt {int}}$ या ${\mathtt {string}}$ , और पैरामीट्रिक प्रकार जैसे ${\mathtt {Map\ (Set\ string)\ int}}$ . बाद वाले प्रकार प्रकार के कार्यों के अनुप्रयोगों के उदाहरण हैं, उदाहरण के लिए, सेट से $\{{\mathtt {Map^{2},\ Set^{1},\ string^{0},\ int^{0}}},\ \rightarrow ^{2}\}$ , जहां सुपरस्क्रिप्ट प्रकार के मापदंडों की संख्या को इंगित करता है। प्रकार के कार्यों का पूरा सेट $C$ एचएम में मनमाना है,^{[note 3]} सिवाय इसके कि इसमें कम से कम शामिल होना चाहिए $\rightarrow ^{2}$ , कार्यों का प्रकार। सुविधा के लिए इसे अक्सर इन्फ़िक्स नोटेशन में लिखा जाता है। उदाहरण के लिए, पूर्णांकों को स्ट्रिंग्स से मैप करने वाले फ़ंक्शन का प्रकार होता है ${\mathtt {int}}\rightarrow {\mathtt {string}}$ . फिर से, कोष्ठक का उपयोग किसी प्रकार की अभिव्यक्ति को स्पष्ट करने के लिए किया जा सकता है। एप्लिकेशन इन्फ़िक्स एरो की तुलना में अधिक मजबूती से बाइंड होता है, जो राइट-बाइंडिंग है।

प्रकार चर को मोनोटाइप के रूप में स्वीकार किया जाता है। मोनोटाइप्स को मोनोमोर्फिक प्रकारों के साथ भ्रमित नहीं किया जाना चाहिए, जो चर को छोड़कर केवल जमीनी शब्दों की अनुमति देते हैं।

दो मोनोटाइप समान हैं यदि उनके पद समान हैं।

बहुप्रकार

पॉलीटाइप्स (या टाइप स्कीम) वे प्रकार हैं जिनमें सभी क्वांटिफायरों के लिए शून्य या अधिक से बंधे चर होते हैं, उदाहरण के लिए $\forall \alpha .\alpha \rightarrow \alpha$ .

पॉलीटाइप वाला एक फ़ंक्शन $\forall \alpha .\alpha \rightarrow \alpha$ एक ही प्रकार के किसी भी मान को स्वयं में मैप कर सकता है, और पहचान फ़ंक्शन इस प्रकार के लिए एक मान है।

एक अन्य उदाहरण के रूप में, $\forall \alpha .({\mathtt {Set}}\ \alpha )\rightarrow {\mathtt {int}}$ एक फ़ंक्शन का प्रकार है जो सभी परिमित सेटों को पूर्णांकों में मैप करता है। एक फ़ंक्शन जो किसी सेट की प्रमुखता लौटाता है वह इस प्रकार का मान होगा।

क्वांटिफ़ायर केवल शीर्ष स्तर के दिखाई दे सकते हैं। उदाहरण के लिए, एक प्रकार $\forall \alpha .\alpha \rightarrow \forall \alpha .\alpha$ प्रकारों के सिंटैक्स द्वारा बाहर रखा गया है। इसके अलावा बहुप्रकारों में मोनोटाइप भी शामिल होते हैं, इस प्रकार एक प्रकार का सामान्य रूप होता है $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau ,n\geq 0$ , कहाँ $\tau$ एक मोनोटाइप है.

बहुप्रकारों की समानता परिमाणीकरण को पुन: व्यवस्थित करने और परिमाणित चरों का नाम बदलने तक है ( $\alpha$ -रूपांतरण). इसके अलावा, मोनोटाइप में नहीं आने वाले परिमाणित चर को हटाया जा सकता है।

प्रसंग और टाइपिंग

अभी भी असंबद्ध भागों (वाक्यविन्यास अभिव्यक्ति और प्रकार) को सार्थक रूप से एक साथ लाने के लिए एक तीसरे भाग की आवश्यकता है: संदर्भ। वाक्यात्मक रूप से, एक संदर्भ जोड़ियों की एक सूची है $x:\sigma$ , जिसे असाइनमेंट (गणितीय तर्क), :wikt:धारणा या नाम बंधन कहा जाता है, प्रत्येक जोड़ी उस मान चर को बताती है $x_{i}$ प्रकार है $\sigma _{i}.$ तीनों भाग मिलकर फॉर्म का टाइपिंग निर्णय देते हैं $\Gamma \ \vdash \ e:\sigma$ , यह बताते हुए कि धारणाओं के तहत $\Gamma$ , इजहार $e$ प्रकार है $\sigma$ .

मुक्त प्रकार के चर

एक प्रकार में $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau$ , प्रतीक $\forall$ प्रकार चर को बांधने वाला क्वांटिफायर है $\alpha _{i}$ मोनोटाइप में $\tau$ . चर $\alpha _{i}$ परिमाणित कहलाते हैं और परिमाणित प्रकार के चर की कोई भी घटना $\tau$ को बाउंड कहा जाता है और सभी अनबाउंड प्रकार के वेरिएबल को कहा जाता है $\tau$ मुक्त कहलाते हैं. परिमाणीकरण के अतिरिक्त $\forall$ बहुप्रकारों में, प्रकार चर को संदर्भ में घटित होने से भी बाध्य किया जा सकता है, लेकिन दाईं ओर विपरीत प्रभाव के साथ $\vdash$ . ऐसे चर तब वहां प्रकार स्थिरांक की तरह व्यवहार करते हैं। अंत में, एक प्रकार का चर कानूनी रूप से टाइपिंग में अनबाउंड हो सकता है, जिस स्थिति में वे अंतर्निहित रूप से सभी-मात्राबद्ध होते हैं।

प्रोग्रामिंग भाषाओं में बाउंड और अनबाउंड दोनों प्रकार के वेरिएबल की उपस्थिति थोड़ी असामान्य है। अक्सर, सभी प्रकार के चरों को अंतर्निहित रूप से सर्व-मात्राबद्ध माना जाता है। उदाहरण के लिए, प्रोलॉग में फ्री वेरिएबल वाले क्लॉज नहीं हैं। इसी तरह हास्केल में, ^{[note 4]} जहां सभी प्रकार के चर अंतर्निहित रूप से मात्राबद्ध होते हैं, यानी एक हास्केल प्रकार a -> a साधन $\forall \alpha .\alpha \rightarrow \alpha$ यहाँ। दाहिने हाथ की ओर का बंधनकारी प्रभाव संबंधित और बहुत ही असामान्य भी है $\sigma$ असाइनमेंट का.

आमतौर पर, बाध्य और अनबाउंड दोनों प्रकार के चर का मिश्रण एक अभिव्यक्ति में मुक्त चर के उपयोग से उत्पन्न होता है। कॉम्बिनेटरी लॉजिक # कॉम्बिनेटर्स के उदाहरण K = $\lambda x.\lambda y.x$ एक उदाहरण प्रदान करता है. इसका मोनोटाइप है $\alpha \rightarrow \beta \rightarrow \alpha$ . कोई व्यक्ति बहुरूपता को बलपूर्वक लागू कर सकता है $\mathbf {let} \ k=\lambda x.(\mathbf {let} \ f=\lambda y.x\ \mathbf {in} \ f)\ \mathbf {in} \ k$ . यहाँ, $f$ प्रकार है $\forall \gamma .\gamma \rightarrow \alpha$ . निःशुल्क मोनोटाइप चर $\alpha$ चर के प्रकार से उत्पन्न होता है $x$ आसपास के दायरे में बंधा हुआ. $k$ प्रकार है $\forall \alpha \forall \beta .\alpha \rightarrow \beta \rightarrow \alpha$ . कोई मुक्त प्रकार के चर की कल्पना कर सकता है $\alpha$ के प्रकार में $f$ से बंधे रहें $\forall \alpha$ के प्रकार में $k$ . लेकिन ऐसी गुंजाइश एचएम में व्यक्त नहीं की जा सकती। बल्कि संदर्भ से बंधन का एहसास होता है।

ऑर्डर टाइप करें

बहुरूपता का अर्थ है कि एक ही अभिव्यक्ति के (संभवतः अनंत रूप से) कई प्रकार हो सकते हैं। लेकिन इस प्रकार की प्रणाली में, ये प्रकार पूरी तरह से असंबंधित नहीं हैं, बल्कि प्राचलिक बहुरूपता द्वारा व्यवस्थित हैं।

उदाहरण के तौर पर, पहचान $\lambda x.x$ हो सकता है $\forall \alpha .\alpha \rightarrow \alpha$ इसके प्रकार के रूप में भी ${\texttt {string}}\rightarrow {\texttt {string}}$ या ${\texttt {int}}\rightarrow {\texttt {int}}$ और कई अन्य, लेकिन नहीं ${\texttt {int}}\rightarrow {\texttt {string}}$ . इस फ़ंक्शन के लिए सबसे सामान्य प्रकार है $\forall \alpha .\alpha \rightarrow \alpha$ , जब अन्य अधिक विशिष्ट हैं और उन्हें सामान्य से लगातार प्राप्त किया जा सकता है प्रकार पैरामीटर के लिए किसी अन्य प्रकार को प्रतिस्थापित करना, यानी परिमाणित चर $\alpha$ . प्रति-उदाहरण विफल हो जाता है क्योंकि प्रतिस्थापन सुसंगत नहीं है.

एकीकरण (कंप्यूटर विज्ञान)#प्रतिस्थापन लागू करके लगातार प्रतिस्थापन को औपचारिक बनाया जा सकता है $S=\left\{\ a_{i}\mapsto \tau _{i},\ \dots \ \right\}$ एक प्रकार की अवधि के लिए $\tau$ , लिखा हुआ $S\tau$ . जैसा कि उदाहरण से पता चलता है, प्रतिस्थापन न केवल एक आदेश से दृढ़ता से संबंधित है, जो व्यक्त करता है कि एक प्रकार कम या ज्यादा विशेष है, बल्कि सभी-परिमाणीकरण के साथ भी है जो प्रतिस्थापन को लागू करने की अनुमति देता है।

औपचारिक रूप से, एचएम में, एक प्रकार $\sigma '$ से अधिक सामान्य है $\sigma$ , औपचारिक रूप से $\sigma '\sqsubseteq \sigma$ , यदि कुछ परिमाणित चर में $\sigma '$ लगातार इस प्रकार प्रतिस्थापित किया जाता है कि व्यक्ति को लाभ हो $\sigma$ जैसा कि साइड बार में दिखाया गया है। यह ऑर्डर टाइप सिस्टम की टाइप परिभाषा का हिस्सा है।

हमारे पिछले उदाहरण में, प्रतिस्थापन लागू करना $S=\left\{\alpha \mapsto {\texttt {string}}\right\}$ परिणाम होगा $\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq {\texttt {string}}\rightarrow {\texttt {string}}$ .

एक परिमाणित चर के लिए एक मोनोमोर्फिक (जमीन) प्रकार को प्रतिस्थापित करते समय सीधे तौर पर, एक पॉलीटाइप को प्रतिस्थापित करने से कुछ नुकसान होते हैं मुक्त चर की उपस्थिति. विशेष रूप से, अनबाउंड वैरिएबल नहीं होना चाहिए जगह ले ली। उन्हें यहां स्थिरांक के रूप में माना जाता है। इसके अतिरिक्त, परिमाणीकरण केवल शीर्ष स्तर पर ही हो सकता है। एक पैरामीट्रिक प्रकार को प्रतिस्थापित करते हुए, किसी को इसके क्वांटिफायर को ऊपर उठाना होगा। दाईं ओर की तालिका नियम को सटीक बनाती है।

वैकल्पिक रूप से, बिना बहुप्रकारों के लिए समतुल्य अंकन पर विचार करें क्वांटिफायर जिसमें क्वांटिफाइड वेरिएबल्स को एक अलग सेट द्वारा दर्शाया जाता है प्रतीक. ऐसे संकेतन में, विशेषज्ञता सादे संगत में कम हो जाती है ऐसे चरों का प्रतिस्थापन.

रिश्ता $\sqsubseteq$ आंशिक आदेश है और $\forall \alpha .\alpha$ इसका सबसे छोटा तत्व है.

प्रमुख प्रकार

जबकि एक प्रकार की योजना का विशेषज्ञता ऑर्डर का एक उपयोग है, यह एक भूमिका निभाता है टाइप सिस्टम में महत्वपूर्ण दूसरी भूमिका। बहुरूपता के साथ अनुमान टाइप करें अभिव्यक्ति के सभी संभावित प्रकारों को संक्षेप में प्रस्तुत करने की चुनौती का सामना करना पड़ता है। आदेश गारंटी देता है कि ऐसा सारांश सबसे सामान्य प्रकार के रूप में मौजूद है अभिव्यक्ति का.

टाइपिंग में प्रतिस्थापन

ऊपर परिभाषित प्रकार क्रम को टाइपिंग तक बढ़ाया जा सकता है क्योंकि टाइपिंग की अंतर्निहित सभी-मात्रा लगातार प्रतिस्थापन को सक्षम बनाती है:

\Gamma \vdash e:\sigma \quad \Longrightarrow \quad S\Gamma \vdash e:S\sigma

विशेषज्ञता नियम के विपरीत, यह परिभाषा का हिस्सा नहीं है, बल्कि अंतर्निहित सभी-परिमाणीकरण की तरह है, बल्कि आगे परिभाषित प्रकार के नियमों का परिणाम है। टाइपिंग में फ्री टाइप वेरिएबल संभावित शोधन के लिए प्लेसहोल्डर के रूप में काम करते हैं। मुक्त प्रकार के लिए पर्यावरण का बाध्यकारी प्रभाव दाहिनी ओर चर $\vdash$ जो विशेषज्ञता नियम में उनके प्रतिस्थापन को फिर से प्रतिबंधित करता है कि प्रतिस्थापन सुसंगत होना चाहिए और इसमें संपूर्ण टाइपिंग को शामिल करने की आवश्यकता होगी।

यह आलेख चार अलग-अलग नियम सेटों पर चर्चा करेगा:

$\vdash _{D}$ घोषणात्मक प्रणाली
$\vdash _{S}$ वाक्यात्मक प्रणाली
$\vdash _{J}$ एल्गोरिदम एक्स
$\vdash _{W}$ एल्गोरिदम ओ

निगमनात्मक प्रणाली

जजमेंट (गणितीय तर्क) के रूप में टाइपिंग का उपयोग करके, एचएम के सिंटैक्स को अनुमान के नियम के सिंटैक्स तक आगे बढ़ाया जाता है जो औपचारिक प्रणाली का मुख्य भाग बनाता है। प्रत्येक नियम परिभाषित करता है कि किस आधार से क्या निष्कर्ष निकाला जा सकता है। निर्णयों के अतिरिक्त, ऊपर प्रस्तुत कुछ अतिरिक्त शर्तों को भी परिसर के रूप में उपयोग किया जा सकता है।

नियमों का उपयोग करने वाला एक प्रमाण निर्णयों का एक क्रम है जैसे कि निष्कर्ष से पहले सभी परिसरों को सूचीबद्ध किया जाता है। नीचे दिए गए उदाहरण प्रमाणों का संभावित प्रारूप दिखाते हैं। बाएँ से दाएँ, प्रत्येक पंक्ति निष्कर्ष दर्शाती है $[{\mathtt {Name}}]$ लागू नियम और परिसर के बारे में, या तो पिछली पंक्ति (संख्या) का संदर्भ देकर यदि आधार एक निर्णय है या विधेय को स्पष्ट करके।

टाइपिंग नियम

Declarative Rule System
${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma }{\Gamma \vdash _{D}x:\sigma }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{D}e:\tau '}{\Gamma \vdash _{D}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau }}&[{\mathtt {Let}}]\\\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma '\quad \sigma '\sqsubseteq \sigma }{\Gamma \vdash _{D}e:\sigma }}&[{\mathtt {Inst}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma \quad \alpha \notin {\text{free}}(\Gamma )}{\Gamma \vdash _{D}e:\forall \ \alpha \ .\ \sigma }}&[{\mathtt {Gen}}]\\\\\end{array}}$

साइड बॉक्स एचएम प्रकार प्रणाली के कटौती नियमों को दर्शाता है। नियमों को मोटे तौर पर दो समूहों में विभाजित किया जा सकता है:

पहले चार नियम $[{\mathtt {Var}}]$ (वेरिएबल या फ़ंक्शन एक्सेस), $[{\mathtt {App}}]$ (एप्लिकेशन, यानी एक पैरामीटर के साथ फ़ंक्शन कॉल), $[{\mathtt {Abs}}]$ (अमूर्त, यानी फ़ंक्शन घोषणा) और $[{\mathtt {Let}}]$ (परिवर्तनीय घोषणा) वाक्यविन्यास पर केंद्रित हैं, प्रत्येक अभिव्यक्ति रूप के लिए एक नियम प्रस्तुत करते हैं। उनका अर्थ पहली नज़र में स्पष्ट है, क्योंकि वे प्रत्येक अभिव्यक्ति को विघटित करते हैं, उनकी उप-अभिव्यक्तियों को सिद्ध करते हैं और अंततः परिसर में पाए जाने वाले व्यक्तिगत प्रकारों को निष्कर्ष में दिए गए प्रकार से जोड़ते हैं।

शेष दो नियमों से दूसरा समूह बनता है $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ . वे प्रकारों की विशेषज्ञता और सामान्यीकरण को संभालते हैं। जबकि नियम $[{\mathtt {Inst}}]$ विशेषज्ञता #प्रकार क्रम पर अनुभाग से स्पष्ट होना चाहिए, $[{\mathtt {Gen}}]$ पूर्व को पूरक करता है, विपरीत दिशा में काम करता है। यह सामान्यीकरण की अनुमति देता है, यानी संदर्भ में बंधे हुए मोनोटाइप चर की मात्रा निर्धारित करने की अनुमति नहीं देता है।

निम्नलिखित दो उदाहरण क्रियान्वित नियम प्रणाली का प्रयोग करते हैं। चूँकि अभिव्यक्ति और प्रकार दोनों दिए गए हैं, वे नियमों का एक प्रकार-जाँच उपयोग हैं।

उदाहरण: के लिए एक प्रमाण $\Gamma \vdash _{D}id(n):int$ कहाँ $\Gamma =id:\forall \alpha .\alpha \rightarrow \alpha ,\ n:int$ , लिखा जा सकता है

{\begin{array}{llll}1:&\Gamma \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \Gamma )\\2:&\Gamma \vdash _{D}id:int\rightarrow int&[{\mathtt {Inst}}]&(1),\ (\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\3:&\Gamma \vdash _{D}n:int&[{\mathtt {Var}}]&(n:int\in \Gamma )\\4:&\Gamma \vdash _{D}id(n):int&[{\mathtt {App}}]&(2),\ (3)\\\end{array}}

उदाहरण: सामान्यीकरण प्रदर्शित करने के लिए, $\vdash _{D}\ {\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha$ नीचे दिखाया गया है:

{\begin{array}{llll}1:&x:\alpha \vdash _{D}x:\alpha &[{\mathtt {Var}}]&(x:\alpha \in \left\{x:\alpha \right\})\\2:&\vdash _{D}\lambda x.x:\alpha \rightarrow \alpha &[{\mathtt {Abs}}]&(1)\\3:&\vdash _{D}\lambda x.x:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Gen}}]&(2),\ (\alpha \not \in free(\epsilon ))\\4:&id:\forall \alpha .\alpha \rightarrow \alpha \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \left\{id:\forall \alpha .\alpha \rightarrow \alpha \right\})\\5:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Let}}]&(3),\ (4)\\\end{array}}

मान लीजिए-बहुरूपता

तुरंत दिखाई नहीं देता है, नियम सेट एक विनियमन को एन्कोड करता है जिसके तहत नियमों में मोनो- और पॉलीटाइप के थोड़े अलग उपयोग से किसी प्रकार को सामान्यीकृत किया जा सकता है या नहीं। $[{\mathtt {Abs}}]$ और $[{\mathtt {Let}}]$ . उसे याद रखो $\sigma$ और $\tau$ क्रमशः पॉली- और मोनोटाइप्स को निरूपित करें।

नियम में $[{\mathtt {Abs}}]$ , फ़ंक्शन के पैरामीटर का मान चर $\lambda x.e$ आधार के माध्यम से एक मोनोमोर्फिक प्रकार के साथ संदर्भ में जोड़ा जाता है $\Gamma ,\ x:\tau \vdash _{D}e:\tau '$ , जबकि नियम में है $[{\mathtt {Let}}]$ , चर पर्यावरण में बहुरूपी रूप में प्रवेश करता है $\Gamma ,\ x:\sigma \vdash _{D}e_{1}:\tau$ . हालाँकि दोनों ही मामलों में की उपस्थिति $x$ संदर्भ में असाइनमेंट में किसी भी मुक्त चर के लिए सामान्यीकरण नियम के उपयोग को रोकता है, यह विनियमन पैरामीटर के प्रकार को बाध्य करता है $x$ में एक $\lambda$ -अभिव्यक्ति मोनोमोर्फिक बनी रहेगी, जबकि लेट-एक्सप्रेशन में, वैरिएबल को बहुरूपी पेश किया जा सकता है, जिससे विशेषज्ञता संभव हो सकेगी।

इस विनियमन के परिणामस्वरूप, $\lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})$ टाइप नहीं किया जा सकता, पैरामीटर के बाद से $f$ एक मोनोमोर्फिक स्थिति में है, जबकि ${\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})$ प्रकार है $(bool,int)$ , क्योंकि $f$ लेट-एक्सप्रेशन में पेश किया गया है और इसलिए इसे बहुरूपी माना जाता है।

सामान्यीकरण नियम

सामान्यीकरण नियम भी करीब से देखने लायक है। यहां, आधार में निहित सभी-परिमाणीकरण $\Gamma \vdash e:\sigma$ को बस दाहिनी ओर ले जाया जाता है $\vdash _{D}$ निष्कर्ष में। यह तब से संभव है $\alpha$ संदर्भ में मुक्त नहीं होता है. फिर, जबकि यह सामान्यीकरण नियम को प्रशंसनीय बनाता है, यह वास्तव में कोई परिणाम नहीं है। इसके विपरीत, सामान्यीकरण नियम एचएम की प्रकार प्रणाली की परिभाषा का हिस्सा है और अंतर्निहित सभी-परिमाणीकरण एक परिणाम है।

एक अनुमान एल्गोरिथ्म

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

नियमों को चुनने की स्वतंत्रता की डिग्री

प्रमाण में उन बिंदुओं को अलग करना, जहां कोई निर्णय संभव ही नहीं है, वाक्य-विन्यास पर केन्द्रित नियमों का पहला समूह तब से कोई विकल्प नहीं छोड़ता है प्रत्येक वाक्यात्मक नियम के अनुरूप एक अद्वितीय टाइपिंग नियम होता है, जो निर्धारित करता है प्रमाण का एक भाग, जबकि निष्कर्ष और इनके परिसर के बीच के निश्चित भागों की शृंखलाएँ $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ घटित हो सकता है. ऐसी श्रृंखला के निष्कर्ष के बीच भी मौजूद हो सकती है सर्वोच्च अभिव्यक्ति के लिए प्रमाण और नियम। सभी सबूत होने चाहिए इतना रेखांकित आकार.

क्योंकि नियम चयन के संबंध में प्रमाण में एकमात्र विकल्प हैं $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ जंजीरें, प्रमाण का स्वरूप यह प्रश्न सुझाता है कि क्या इसे और अधिक सटीक बनाया जा सकता है, जहां इन जंजीरों की आवश्यकता नहीं हो सकती है। यह वास्तव में संभव है और एक की ओर ले जाता है नियम प्रणाली का एक प्रकार जिसमें ऐसे कोई नियम नहीं हैं।

सिंटैक्स-निर्देशित नियम प्रणाली

Syntactical Rule System
${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \sigma \sqsubseteq \tau }{\Gamma \vdash _{S}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{S}e_{1}:\tau }{\Gamma \vdash _{S}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{S}e:\tau '}{\Gamma \vdash _{S}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{S}e_{1}:\tau '}{\Gamma \vdash _{S}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}$
Generalization
${\bar {\Gamma }}(\tau )=\forall \ {\hat {\alpha }}\ .\ \tau \quad \quad {\hat {\alpha }}={\textrm {free}}(\tau )-{\textrm {free}}(\Gamma )$

एचएम का एक समकालीन उपचार विशुद्ध रूप से वाक्यविन्यास-निर्देशित नियम प्रणाली का उपयोग करता है मेहरबान^[7] एक मध्यवर्ती कदम के रूप में. इस प्रणाली में, विशेषज्ञता सीधे मूल के बाद स्थित होती है $[{\mathtt {Var}}]$ नियम और इसमें विलीन हो जाता है, जबकि सामान्यीकरण इसका हिस्सा बन जाता है $[{\mathtt {Let}}]$ नियम। वहां सामान्यीकरण है फ़ंक्शन को प्रस्तुत करके हमेशा सबसे सामान्य प्रकार का उत्पादन करने के लिए भी निर्धारित किया गया है ${\bar {\Gamma }}(\tau )$ , जो मात्रा निर्धारित करता है सभी मोनोटाइप वैरिएबल बाध्य नहीं हैं $\Gamma$ .

औपचारिक रूप से, इस नई नियम प्रणाली को मान्य करने के लिए $\vdash _{S}$ मूल के समतुल्य है $\vdash _{D}$ , किसी के पास उसे दिखाने के लिए $\Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma$ , जो दो उप-प्रमाणों में विघटित हो जाता है:

$\Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma$ (गाढ़ापन)
$\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma$ (पूर्णता (तर्क))

जबकि नियमों को विघटित करके एकरूपता देखी जा सकती है $[{\mathtt {Let}}]$ और $[{\mathtt {Var}}]$ का $\vdash _{S}$ सबूतों में $\vdash _{D}$ , संभावना यही दिख रही है $\vdash _{S}$ अधूरा है, जैसे कोई दिखा नहीं सकता $\lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha$ में $\vdash _{S}$ , उदाहरण के लिए, लेकिन केवल $\lambda \ x.x:\alpha \rightarrow \alpha$ . पूर्णता का केवल थोड़ा कमजोर संस्करण ही सिद्ध किया जा सकता है ^[8] हालाँकि, अर्थात्

$\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma$

तात्पर्य यह है कि, कोई किसी अभिव्यक्ति के लिए मुख्य प्रकार प्राप्त कर सकता है $\vdash _{S}$ हमें अंत में प्रमाण को सामान्यीकृत करने की अनुमति देता है।

की तुलना $\vdash _{D}$ और $\vdash _{S}$ , अब सभी नियमों के निर्णयों में केवल मोनोटाइप ही दिखाई देते हैं। इसके अतिरिक्त, कटौती प्रणाली के साथ किसी भी संभावित प्रमाण का आकार अब अभिव्यक्ति के आकार के समान है (दोनों को टर्म (तर्क)#औपचारिक परिभाषा के रूप में देखा जाता है)। इस प्रकार अभिव्यक्ति पूरी तरह से प्रमाण के आकार को निर्धारित करती है। में $\vdash _{D}$ आकार संभवतः सभी नियमों को छोड़कर अन्य नियमों के अनुसार निर्धारित किया जाएगा $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ , जो अन्य नोड्स के बीच मनमाने ढंग से लंबी शाखाएं (चेन) बनाने की अनुमति देता है।

नियमों को लागू करने वाली स्वतंत्रता की डिग्री

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

यहां, प्रतिस्थापन (विशेषज्ञता) आदेश चलन में आता है। हालाँकि पहली नज़र में कोई भी स्थानीय रूप से प्रकारों को निर्धारित नहीं कर सकता है, आशा है कि प्रमाण वृक्ष को पार करते समय क्रम की सहायता से उन्हें परिष्कृत करना संभव है, इसके अतिरिक्त यह मानते हुए, क्योंकि परिणामी एल्गोरिदम एक अनुमान विधि बनना है, कि किसी भी परिसर का प्रकार सर्वोत्तम संभव के रूप में निर्धारित किया जाएगा। और वास्तव में, कोई भी, के नियमों को देखते हुए, ऐसा कर सकता है $\vdash _{S}$ सुझाव:

$[Abs]$ : महत्वपूर्ण विकल्प है $τ$ . फिलहाल इस बारे में कुछ पता नहीं चल पाया है $τ$ , इसलिए कोई केवल सबसे सामान्य प्रकार ही मान सकता है, जो कि है $\forall \alpha .\alpha$ . योजना यह है कि यदि आवश्यक हो तो प्रकार को विशेषज्ञ बनाया जाए। दुर्भाग्य से, इस स्थान पर पॉलीटाइप की अनुमति नहीं है, इसलिए कुछ $α$ फिलहाल करना होगा. अवांछित कैप्चर से बचने के लिए, एक प्रकार का चर जो अभी तक प्रूफ़ में नहीं है, एक सुरक्षित विकल्प है। इसके अतिरिक्त, किसी को यह ध्यान में रखना होगा कि यह मोनोटाइप अभी तक तय नहीं हुआ है, लेकिन इसे और परिष्कृत किया जा सकता है।
$[Var]$ : चुनाव यह है कि कैसे परिष्कृत किया जाए $σ$ . क्योंकि किसी भी प्रकार का कोई भी विकल्प $τ$ यहां वेरिएबल के उपयोग पर निर्भर करता है, जो स्थानीय रूप से ज्ञात नहीं है, सबसे सुरक्षित दांव सबसे सामान्य है। ऊपर दी गई समान विधि का उपयोग करके सभी मात्रात्मक चर को तुरंत चालू किया जा सकता है $σ$ नए वैरिएबल मोनोटाइप वैरिएबल के साथ, उन्हें फिर से आगे के शोधन के लिए खुला रखा गया है।
$[Let]$ : नियम कोई विकल्प नहीं छोड़ता। पूर्ण।
[App]: केवल एप्लिकेशन नियम ही अब तक खोले गए वेरिएबल्स को परिष्कृत करने के लिए बाध्य कर सकता है, जैसा कि दोनों परिसरों द्वारा आवश्यक है।
1. पहला आधार अनुमान के परिणाम को प्रपत्र का होने के लिए बाध्य करता है $\tau \rightarrow \tau '$ $\tau \rightarrow \tau '$ .
  - अगर ऐसा है तो ठीक है. कोई भी बाद में इसे चुन सकता है $τ'$ परिणाम के लिए.
  - यदि नहीं, तो यह एक खुला चर हो सकता है। फिर इसे पहले की तरह दो नए वेरिएबल्स के साथ आवश्यक रूप में परिष्कृत किया जा सकता है।
  - अन्यथा, प्रकार की जाँच विफल हो जाती है क्योंकि पहले आधार से एक ऐसे प्रकार का अनुमान लगाया गया है जो फ़ंक्शन प्रकार में नहीं है और न ही बनाया जा सकता है।
2. दूसरे आधार के लिए आवश्यक है कि अनुमानित प्रकार बराबर हो $τ$ पहले परिसर का. अब संभवतः दो अलग-अलग प्रकार हैं, शायद खुले प्रकार के चर के साथ, तुलना करने के लिए और यदि संभव हो तो बराबर करने के लिए। यदि ऐसा है, तो एक शोधन पाया जाता है, और यदि नहीं, तो एक प्रकार की त्रुटि फिर से पाई जाती है। प्रतिस्थापन द्वारा दो शब्दों को समान बनाने के लिए एक प्रभावी विधि ज्ञात है, तथाकथित असंयुक्त-सेट डेटा संरचना के साथ संयोजन में जॉन एलन रॉबिन्सन | रॉबिन्सन का एकीकरण (कंप्यूटिंग) | यूनियन-फाइंड एल्गोरिदम।

संघ-खोज एल्गोरिथ्म को संक्षेप में संक्षेप में प्रस्तुत करने के लिए, एक प्रमाण में सभी प्रकारों के सेट को देखते हुए, यह किसी को एक के माध्यम से उन्हें समतुल्य वर्गों में समूहित करने की अनुमति देता है। union प्रक्रिया और ऐसे प्रत्येक वर्ग के लिए एक प्रतिनिधि चुनना find प्रक्रिया। साइड इफेक्ट (कंप्यूटर विज्ञान) के अर्थ में प्रक्रिया (कंप्यूटर विज्ञान) शब्द पर जोर देते हुए, हम एक प्रभावी एल्गोरिदम तैयार करने के लिए स्पष्ट रूप से तर्क के दायरे को छोड़ रहे हैं। ए के प्रतिनिधि ${\mathtt {union}}(a,b)$ इस प्रकार निर्धारित किया जाता है कि, यदि दोनों $a$ और $b$ प्रकार के चर हैं तो प्रतिनिधि मनमाने ढंग से उनमें से एक है, लेकिन एक चर और एक पद को एकजुट करते समय, पद प्रतिनिधि बन जाता है। यूनियन-फाइंड के कार्यान्वयन को हाथ में लेते हुए, कोई दो मोनोटाइप्स के एकीकरण को निम्नानुसार तैयार कर सकता है:

एकजुट(ta, tb):
    टा = खोजें(टा)
    टीबी = खोजें(टीबी)
    यदि दोनों ta,tb समान D,n के साथ D p1..pn रूप के पद हैं
        प्रत्येक संगत iवें पैरामीटर के लिए unify(ta[i], tb[i])।
    अन्य
    यदि ta,tb में से कम से कम एक एक प्रकार का चर है
        संघ(टीए, टीबी)
    अन्य
        त्रुटि 'प्रकार मेल नहीं खाते'

अब अनुमान एल्गोरिदम का एक स्केच हाथ में होने से, अगले भाग में एक अधिक औपचारिक प्रस्तुति दी गई है। इसका वर्णन मिलनर में किया गया है^[2]पी. 370 एफएफ. एल्गोरिदम जे के रूप में

एल्गोरिदम एक्स

Algorithm J
${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{J}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau _{0}\quad \Gamma \vdash _{J}e_{1}:\tau _{1}\quad \tau '={\mathit {newvar}}\quad {\mathit {unify}}(\tau _{0},\ \tau _{1}\rightarrow \tau ')}{\Gamma \vdash _{J}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{J}e:\tau '}{\Gamma \vdash _{J}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{J}e_{1}:\tau '}{\Gamma \vdash _{J}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}$

एल्गोरिथम जे की प्रस्तुति तार्किक नियमों के अंकन का दुरुपयोग है, क्योंकि इसमें दुष्प्रभाव शामिल हैं लेकिन इसके साथ सीधी तुलना की अनुमति मिलती है $\vdash _{S}$ साथ ही एक कुशल कार्यान्वयन को व्यक्त करते हुए। नियम अब मापदंडों के साथ एक प्रक्रिया निर्दिष्ट करते हैं $\Gamma ,e$ उपज $\tau$ निष्कर्ष में जहां परिसर का निष्पादन बाएं से दाएं की ओर बढ़ता है।

प्रक्रिया $inst(\sigma )$ पॉलीटाइप में विशेषज्ञता रखता है $\sigma$ शब्द की प्रतिलिपि बनाकर और बाध्य प्रकार चर को लगातार नए मोनोटाइप चर द्वारा प्रतिस्थापित करके। ' $newvar$ ' एक नया मोनोटाइप वैरिएबल उत्पन्न करता है। संभावित, ${\bar {\Gamma }}(\tau )$ अवांछित कैप्चर से बचने के लिए परिमाणीकरण के लिए नए चर पेश करने वाले प्रकार की प्रतिलिपि बनाना होगा। कुल मिलाकर, एल्गोरिथ्म अब विशेषज्ञता को एकीकरण पर छोड़कर हमेशा सबसे सामान्य विकल्प चुनकर आगे बढ़ता है, जो स्वयं सबसे सामान्य परिणाम उत्पन्न करता है। जैसा कि उल्लेख किया गया है #सिंटैक्स संचालित नियम प्रणाली, अंतिम परिणाम $\tau$ को सामान्यीकृत करना होगा ${\bar {\Gamma }}(\tau )$ अंत में, किसी दिए गए अभिव्यक्ति के लिए सबसे सामान्य प्रकार प्राप्त करने के लिए।

चूँकि एल्गोरिथम में उपयोग की जाने वाली प्रक्रियाओं की लागत लगभग O(1) होती है, एल्गोरिथम की कुल लागत उस अभिव्यक्ति के आकार में रैखिक के करीब होती है जिसके लिए एक प्रकार का अनुमान लगाया जाना है। यह टाइप अनुमान एल्गोरिदम प्राप्त करने के कई अन्य प्रयासों के बिल्कुल विपरीत है, जो अक्सर समाप्ति के संबंध में अनिर्णीत समस्या होने पर भी एनपी कठिन के रूप में सामने आता है। इस प्रकार एचएम सबसे अच्छा पूर्णतः सूचित टाइप-चेकिंग एल्गोरिदम का प्रदर्शन कर सकता है। यहां टाइप-चेकिंग का मतलब है कि एल्गोरिदम को कोई प्रमाण ढूंढना नहीं है, बल्कि केवल किसी दिए गए प्रमाण को मान्य करना है।

दक्षता थोड़ी कम हो गई है क्योंकि गणना की अनुमति देने के लिए संदर्भ में प्रकार चर के बंधन को बनाए रखना पड़ता है ${\bar {\Gamma }}(\tau )$ और पुनरावर्ती प्रकार के निर्माण को रोकने के लिए एक घटित जाँच को सक्षम करें $union(\alpha ,\tau )$ . ऐसे ही एक मामले का उदाहरण है $\lambda \ x.(x\ x)$ , जिसके लिए एचएम का उपयोग करके कोई प्रकार प्राप्त नहीं किया जा सकता है। व्यावहारिक रूप से, प्रकार केवल छोटे शब्द हैं और विस्तारित संरचनाओं का निर्माण नहीं करते हैं। इस प्रकार, जटिलता विश्लेषण में, कोई उनकी तुलना O(1) लागत को बनाए रखते हुए एक स्थिर मान के रूप में कर सकता है।

एल्गोरिथ्म साबित करना

पिछले अनुभाग में, एल्गोरिथम का रेखाचित्र बनाते समय धातुवैज्ञानिक तर्क के साथ इसके प्रमाण का संकेत दिया गया था। हालांकि यह एक कुशल एल्गोरिदम जे की ओर जाता है, लेकिन यह स्पष्ट नहीं है कि एल्गोरिदम कटौती प्रणाली डी या एस को ठीक से प्रतिबिंबित करता है या नहीं जो सिमेंटिक बेस लाइन के रूप में काम करता है।

उपरोक्त तर्क में सबसे महत्वपूर्ण बिंदु मोनोटाइप का परिशोधन है संदर्भ से बंधे चर। उदाहरण के लिए, एल्गोरिदम साहसपूर्वक बदलता है उदाहरण के लिए अनुमान लगाते समय संदर्भ $\lambda f.(f\ 1)$ , क्योंकि मोनोटाइप वैरिएबल को पैरामीटर के संदर्भ में जोड़ा गया है $f$ बाद में परिष्कृत करने की आवश्यकता है को $int\rightarrow \beta$ एप्लिकेशन को संभालते समय. समस्या यह है कि कटौती नियम ऐसे परिशोधन की अनुमति नहीं देते हैं। तर्क देते हुए कहा कि इसके स्थान पर पहले भी परिष्कृत प्रकार जोड़ा जा सकता था मोनोटाइप वैरिएबल सर्वोत्तम रूप से समीचीन है।

औपचारिक रूप से संतोषजनक तर्क तक पहुंचने की कुंजी उचित रूप से शामिल करना है परिशोधन के अंतर्गत संदर्भ. औपचारिक रूप से, टाइपिंग फ्री टाइप वेरिएबल्स के प्रतिस्थापन के साथ संगत है।

\Gamma \vdash _{S}e:\tau \quad \Longrightarrow \quad S\Gamma \vdash _{S}e:S\tau

इस प्रकार मुक्त चरों को परिष्कृत करने का अर्थ है संपूर्ण टाइपिंग को परिष्कृत करना।

एल्गोरिथम Ω

Algorithm W
$\begin{array}{cl} x : σ \in Γ τ = i n s t (σ) Γ ⊢_{W} x : τ, \emptyset [V a r] & \frac{\begin{array}{ll} Γ ⊢_{W} e_{0} : τ_{0}, S_{0} & S_{0} Γ ⊢_{W} e_{1} : τ_{1}, S_{1} \\ τ^{'} = n e w v a r & S_{2} = m g u (S_{1} τ_{0}, τ_{1} \to τ^{'}) \end{array}}{Γ ⊢_{W} e_{0} e_{1} : S_{2} τ^{'}, S_{2} S_{1} S_{0}} & [A p p] & \frac{τ = n e w v a r Γ, x : τ ⊢_{W} e : τ^{'}, S}{Γ ⊢_{W} λ x . e : S τ \to τ^{'}, S} & [A b s] & Γ ⊢_{W} e_{0} : τ, S_{0} S_{0} Γ, x : \bar{S_{0} Γ} (τ) ⊢_{W} e_{1} \end{array}$

वहां से, एल्गोरिथम J का प्रमाण एल्गोरिथम W की ओर ले जाता है, जो केवल बनाता है प्रक्रिया द्वारा लगाए गए दुष्प्रभाव

{\textit {union}}

द्वारा स्पष्ट प्रतिस्थापनों के माध्यम से इसकी क्रमिक संरचना को व्यक्त करना

S_{i}

. साइडबार में एल्गोरिदम डब्ल्यू की प्रस्तुति अभी भी साइड इफेक्ट्स का उपयोग करती है इटैलिक में सेट किए गए ऑपरेशनों में, लेकिन ये अब जनरेटिंग तक ही सीमित हैं ताजा प्रतीक. निर्णय का स्वरूप है

\Gamma \vdash e:\tau ,S

, एक फ़ंक्शन को संदर्भ और अभिव्यक्ति के साथ पैरामीटर के रूप में निरूपित करना एक साथ एक मोनोटाइप का निर्माण करता है एक प्रतिस्थापन.

{\textsf {mgu}}

एक दुष्प्रभाव मुक्त संस्करण है का

{\textit {union}}

एक प्रतिस्थापन का निर्माण जो प्रथम-क्रम शब्दों का एकीकरण (कंप्यूटर विज्ञान)#वाक्यात्मक एकीकरण है।

जबकि एल्गोरिथम W को सामान्यतः HM एल्गोरिथम माना जाता है और है प्रायः साहित्य में नियम व्यवस्था के बाद सीधे प्रस्तुत किया जाता है, इसका उद्देश्य है मिलनर द्वारा वर्णित^[2]पी. 369 पर इस प्रकार है:

जैसा कि यह खड़ा है, डब्ल्यू शायद ही एक कुशल एल्गोरिदम है; प्रतिस्थापन बहुत बार लागू होते हैं। इसे सुदृढ़ता के प्रमाण में सहायता के लिए तैयार किया गया था। अब हम एक सरल एल्गोरिथ्म J प्रस्तुत करते हैं जो सटीक अर्थों में W का अनुकरण करता है।

जबकि उन्होंने डब्ल्यू को अधिक जटिल और कम कुशल माना, उन्होंने इसे प्रस्तुत किया जे से पहले अपने प्रकाशन में। जब दुष्प्रभाव अनुपलब्ध या अवांछित होते हैं तो इसके अपने गुण होते हैं। पूर्णता साबित करने के लिए डब्ल्यू की भी आवश्यकता होती है, जिसे उसके द्वारा सुदृढ़ता प्रमाण में शामिल किया जाता है।

प्रमाण दायित्व

प्रमाण दायित्वों को तैयार करने से पहले, नियम प्रणाली डी और एस और प्रस्तुत एल्गोरिदम के बीच विचलन पर जोर दिया जाना चाहिए।

जबकि उपरोक्त विकास ने ओपन प्रूफ वेरिएबल्स के रूप में मोनोटाइप्स का दुरुपयोग किया था, इस संभावना को कि उचित मोनोटाइप वेरिएबल्स को नुकसान पहुंचाया जा सकता था, नए वेरिएबल्स पेश करके और सर्वोत्तम की उम्मीद करके दरकिनार कर दिया गया था। लेकिन इसमें एक दिक्कत है: किए गए वादों में से एक यह था कि इन नए बदलावों को इसी तरह ध्यान में रखा जाएगा। यह वादा एल्गोरिथम द्वारा पूरा नहीं किया गया है.

एक प्रसंग होना $1:int,\ f:\alpha$ , इजहार $f\ 1$ टाइप भी नहीं किया जा सकता $\vdash _{D}$ या $\vdash _{S}$ , लेकिन एल्गोरिदम साथ आते हैं प्ररूप $\beta$ , जहां W अतिरिक्त रूप से प्रतिस्थापन प्रदान करता है $\left\{\alpha \mapsto int\rightarrow \beta \right\}$ , इसका मतलब है कि एल्गोरिदम सभी प्रकार की त्रुटियों का पता लगाने में विफल रहता है। इस चूक को अधिक सावधानी से अलग किए गए प्रमाण द्वारा आसानी से ठीक किया जा सकता है चर और मोनोटाइप चर।

लेखक समस्या से अच्छी तरह परिचित थे लेकिन उन्होंने इसे ठीक न करने का निर्णय लिया। इसके पीछे कोई व्यावहारिक कारण मान सकता है। जबकि प्रकार अनुमान को अधिक उचित ढंग से लागू करने से एल्गोरिदम अमूर्त मोनोटाइप से निपटने में सक्षम हो जाता, इच्छित एप्लिकेशन के लिए उनकी आवश्यकता नहीं थी, जहां पहले से मौजूद संदर्भ में कोई भी आइटम मुफ़्त नहीं है चर। इस प्रकाश में, एक सरल एल्गोरिथ्म के पक्ष में अनावश्यक जटिलता को हटा दिया गया। शेष नकारात्मक पक्ष यह है कि नियम प्रणाली के संबंध में एल्गोरिदम का प्रमाण कम सामान्य है और इसे केवल बनाया जा सकता है के साथ संदर्भों के लिए $free(\Gamma )=\emptyset$ एक पार्श्व शर्त के रूप में.

${\begin{array}{lll}{\text{(Correctness)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\{\text{(Completeness)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{forall}}\ \tau \ {\text{where}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}$ पूर्णता दायित्व में साइड कंडीशन यह बताती है कि कैसे कटौती कई प्रकार दे सकती है, जबकि एल्गोरिदम हमेशा एक उत्पन्न करता है। साथ ही, साइड कंडीशन की मांग है कि अनुमानित प्रकार वास्तव में सबसे सामान्य है।

दायित्वों को ठीक से साबित करने के लिए पहले उन्हें मजबूत करने की आवश्यकता है ताकि प्रतिस्थापन लेम्मा को सक्रिय करने की अनुमति मिल सके जो प्रतिस्थापन को फैलाता है $S$ द्वारा $\vdash _{S}$ और $\vdash _{W}$ . वहां से, प्रमाण अभिव्यक्ति पर प्रेरण द्वारा होते हैं।

एक अन्य प्रमाण दायित्व स्वयं प्रतिस्थापन लेम्मा है, यानी टाइपिंग का प्रतिस्थापन, जो अंततः सभी-मात्राकरण स्थापित करता है। बाद को औपचारिक रूप से सिद्ध नहीं किया जा सकता, क्योंकि ऐसा कोई वाक्यविन्यास उपलब्ध नहीं है।

एक्सटेंशन

पुनरावर्ती परिभाषाएँ

ट्यूरिंग को पूर्णता प्रदान करने के लिए पुनरावर्ती कार्यों की आवश्यकता होती है। लैम्ब्डा कैलकुलस की एक केंद्रीय संपत्ति पुनरावर्ती परिभाषाएँ है सीधे उपलब्ध नहीं हैं, बल्कि इन्हें एक निश्चित बिंदु संयोजक के साथ व्यक्त किया जा सकता है। लेकिन दुर्भाग्य से, फिक्सपॉइंट कॉम्बिनेटर को टाइप किए गए संस्करण में तैयार नहीं किया जा सकता है लैम्ब्डा कैलकुलस का सिस्टम पर विनाशकारी प्रभाव पड़े बिना जैसा कि बताया गया है नीचे।

टाइपिंग नियम

मूल कागज^[4]दिखाता है कि रिकर्सन को कॉम्बिनेटर द्वारा महसूस किया जा सकता है ${\mathit {fix}}:\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha$ . इस प्रकार एक संभावित पुनरावर्ती परिभाषा इस प्रकार तैयार की जा सकती है ${\mathtt {rec}}\ v=e_{1}\ {\mathtt {in}}\ e_{2}\ ::={\mathtt {let}}\ v={\mathit {fix}}(\lambda v.e_{1})\ {\mathtt {in}}\ e_{2}$ .

वैकल्पिक रूप से अभिव्यक्ति सिंटैक्स का विस्तार और एक अतिरिक्त टाइपिंग नियम संभव है:

\displaystyle {\frac {\Gamma ,\Gamma '\vdash e_{1}:\tau _{1}\quad \dots \quad \Gamma ,\Gamma '\vdash e_{n}:\tau _{n}\quad \Gamma ,\Gamma ''\vdash e:\tau }{\Gamma \ \vdash \ {\mathtt {rec}}\ v_{1}=e_{1}\ {\mathtt {and}}\ \dots \ {\mathtt {and}}\ v_{n}=e_{n}\ {\mathtt {in}}\ e:\tau }}\quad [{\mathtt {Rec}}]

कहाँ

$\Gamma '=v_{1}:\tau _{1},\ \dots ,\ v_{n}:\tau _{n}$
$\Gamma ''=v_{1}:{\bar {\Gamma }}(\ \tau _{1}\ ),\ \dots ,\ v_{n}:{\bar {\Gamma }}(\ \tau _{n}\ )$

मूलतः विलय $[{\mathtt {Abs}}]$ और $[{\mathtt {Let}}]$ जबकि पुनरावर्ती रूप से परिभाषित शामिल है मोनोटाइप स्थितियों में वेरिएबल जहां वे बाईं ओर होते हैं ${\mathtt {in}}$ लेकिन इसके दाईं ओर बहुप्रकार के रूप में।

परिणाम

हालाँकि उपरोक्त सीधा है, इसकी कीमत चुकानी पड़ती है।

प्रकार सिद्धांत लैम्ब्डा कैलकुलस को गणना और तर्क से जोड़ती है। उपरोक्त आसान संशोधन का दोनों पर प्रभाव पड़ता है:

सामान्यीकरण संपत्ति (सार पुनर्लेखन) अमान्य है, क्योंकि गैर-समाप्ति शर्तों को तैयार किया जा सकता है।
तर्क संगति क्योंकि प्रकार $\forall a.a$ निवास प्रकार बन जाता है।

ओवरलोडिंग

ओवरलोडिंग का अर्थ है कि विभिन्न कार्यों को एक ही नाम से परिभाषित और उपयोग किया जा सकता है। अधिकांश प्रोग्रामिंग भाषाएं कम से कम अंतर्निहित अंकगणितीय संचालन (+,<,आदि) के साथ ओवरलोडिंग प्रदान करती हैं, जिससे प्रोग्रामर को अंकगणितीय अभिव्यक्तियों को एक ही रूप में लिखने की अनुमति मिलती है, यहां तक कि विभिन्न संख्यात्मक प्रकारों के लिए भी int या real. क्योंकि एक ही अभिव्यक्ति के भीतर इन विभिन्न प्रकारों का मिश्रण भी अंतर्निहित रूपांतरण की मांग करता है, विशेष रूप से इन परिचालनों के लिए ओवरलोडिंग अक्सर प्रोग्रामिंग भाषा में ही निर्मित होती है। कुछ भाषाओं में, इस सुविधा को सामान्यीकृत किया गया है और उपयोगकर्ता के लिए उपलब्ध कराया गया है, उदाहरण के लिए सी++ में.

जबकि टाइप चेकिंग और अनुमान दोनों में गणना लागत के लिए कार्यात्मक प्रोग्रामिंग में तदर्थ बहुरूपता से बचा गया है^{[citation needed]}, ओवरलोडिंग को व्यवस्थित करने का एक साधन पेश किया गया है जो फॉर्म और नामकरण दोनों में ऑब्जेक्ट ओरिएंटेड प्रोग्रामिंग के समान है, लेकिन एक स्तर ऊपर की ओर काम करता है। इस व्यवस्थित में उदाहरण वस्तु नहीं हैं (अर्थात मूल्य स्तर पर), बल्कि प्रकार हैं। परिचय में उल्लिखित क्विकॉर्ट उदाहरण ऑर्डर में ओवरलोडिंग का उपयोग करता है, जिसमें हास्केल में निम्न प्रकार का एनोटेशन होता है:

quickSort :: Ord a => [a] -> [a]

यहाँ, प्रकार a न केवल बहुरूपी है, बल्कि कुछ प्रकार के वर्ग का उदाहरण होने तक भी सीमित है Ord, जो आदेश विधेय प्रदान करता है < और >= फ़ंक्शंस बॉडी में उपयोग किया जाता है। इन विधेयों के उचित कार्यान्वयन को अतिरिक्त मापदंडों के रूप में क्विकॉर्ट्स को पास कर दिया जाता है, जैसे ही क्विकॉर्ट का उपयोग अधिक ठोस प्रकारों पर किया जाता है जो ओवरलोडेड फ़ंक्शन क्विकसॉर्ट का एकल कार्यान्वयन प्रदान करता है।

क्योंकि कक्षाएं केवल एक ही प्रकार को अपने तर्क के रूप में अनुमति देती हैं, परिणामी प्रकार प्रणाली अभी भी अनुमान प्रदान कर सकती है। इसके अतिरिक्त, प्रकार की कक्षाओं को किसी प्रकार के ओवरलोडिंग ऑर्डर से सुसज्जित किया जा सकता है, जिससे कक्षाओं को जाली (आदेश) के रूप में व्यवस्थित किया जा सकता है।

उच्च-क्रम प्रकार

प्राचलिक बहुरूपता का अर्थ है कि प्रकार स्वयं को पैरामीटर के रूप में पारित किया जाता है जैसे कि वे उचित मान थे। उचित कार्यों के लिए तर्क के रूप में पारित किया गया, लेकिन पैरामीट्रिक प्रकार के स्थिरांक के रूप में प्रकार के कार्यों में भी, इस सवाल की ओर जाता है कि प्रकारों को और अधिक उचित तरीके से कैसे टाइप किया जाए। और भी अधिक अभिव्यंजक प्रकार की प्रणाली बनाने के लिए उच्च-क्रम प्रकारों का उपयोग किया जाता है।

दुर्भाग्य से, एकीकरण (कंप्यूटर विज्ञान)#उच्च-क्रम एकीकरण अब मेटा प्रकारों की उपस्थिति में निर्णय लेने योग्य नहीं है, जिससे व्यापकता के इस विस्तार में प्रकार का अनुमान असंभव हो जाता है। इसके अतिरिक्त, सभी प्रकार के एक प्रकार को मान लेना जिसमें स्वयं को प्रकार के रूप में शामिल किया जाता है, एक विरोधाभास की ओर ले जाता है, जैसा कि सभी सेटों के सेट में होता है, इसलिए किसी को अमूर्तता के स्तर के चरणों में आगे बढ़ना चाहिए। दूसरे क्रम के लैम्ब्डा कैलकुलस में अनुसंधान, एक कदम ऊपर, से पता चला कि इस व्यापकता में प्रकार का अनुमान अनिर्णीत है।

एक अतिरिक्त स्तर के हिस्सों को प्रकार (प्रकार सिद्धांत) नामक हास्केल में पेश किया गया है, जहां इसका उपयोग मोनाड (कार्यात्मक प्रोग्रामिंग) टाइप करने में मदद के लिए किया जाता है। विस्तारित प्रकार प्रणाली के आंतरिक यांत्रिकी में पर्दे के पीछे काम करते हुए, प्रकारों को अंतर्निहित छोड़ दिया जाता है।

उपप्रकार

उपप्रकार और प्रकार अनुमान को संयोजित करने के प्रयासों से काफी निराशा हुई है। उपटाइपिंग बाधाओं को जमा करना और प्रचारित करना (प्रकार समानता बाधाओं के विपरीत) सरल है, जिससे परिणामी बाधाओं को अनुमानित टाइपिंग योजनाओं का हिस्सा बना दिया जाता है, उदाहरण के लिए $\forall \alpha .\ (\alpha \leq T)\Rightarrow \alpha \rightarrow \alpha$ , कहाँ $\alpha \leq T$ प्रकार चर पर एक बाधा है $\alpha$ . हालाँकि, क्योंकि प्रकार चर अब इस दृष्टिकोण में उत्सुकता से एकीकृत नहीं हैं, यह कई बेकार प्रकार के चर और बाधाओं से युक्त बड़ी और बोझिल टाइपिंग योजनाएं उत्पन्न करता है, जिससे उन्हें पढ़ना और समझना कठिन हो जाता है। इसलिए, ऐसी टाइपिंग योजनाओं और उनकी बाधाओं को सरल बनाने में काफी प्रयास किए गए, गैर-नियतात्मक परिमित ऑटोमेटन (एनएफए) सरलीकरण के समान तकनीकों का उपयोग करना (अनुमानित पुनरावर्ती प्रकारों की उपस्थिति में उपयोगी)।^[9] अभी हाल ही में, डोलन और माइक्रॉफ्ट^[10] टाइपिंग योजना सरलीकरण और एनएफए सरलीकरण के बीच संबंध को औपचारिक रूप दिया गया और दिखाया कि उपटाइपिंग की औपचारिकता पर एक बीजगणितीय टेक ने एमएल जैसी भाषा (जिसे एमएलसब कहा जाता है) के लिए कॉम्पैक्ट प्रिंसिपल टाइपिंग योजनाएं तैयार करने की अनुमति दी। विशेष रूप से, उनकी प्रस्तावित टाइपिंग योजना में स्पष्ट बाधाओं के बजाय संघ और प्रतिच्छेदन प्रकारों के प्रतिबंधित रूप का उपयोग किया गया था। पार्रेक्स ने बाद में दावा किया^[11] यह बीजगणितीय सूत्रीकरण एल्गोरिथम डब्ल्यू से मिलते-जुलते अपेक्षाकृत सरल एल्गोरिथम के बराबर था, और यह कि यूनियन और इंटरसेक्शन प्रकारों का उपयोग आवश्यक नहीं था।

दूसरी ओर, ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग भाषाओं के संदर्भ में प्रकार का अनुमान अधिक कठिन साबित हुआ है, क्योंकि ऑब्जेक्ट विधियों को सिस्टम एफ की शैली में प्रथम श्रेणी बहुरूपता की आवश्यकता होती है (जहां प्रकार का अनुमान अनिर्दिष्ट है) और एफ-बाध्य बहुरूपता जैसी विशेषताओं के कारण। नतीजतन, ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग को सक्षम करने वाले सबटाइपिंग वाले टाइप सिस्टम, जैसे लुका कार्डेली का सिस्टम एफ-उप $F_{<:}$ ,^[12] एचएम-शैली प्रकार के अनुमान का समर्थन न करें।

पंक्ति बहुरूपता का उपयोग संरचनात्मक रिकॉर्ड जैसी भाषा सुविधाओं का समर्थन करने के लिए उपटाइपिंग के विकल्प के रूप में किया जा सकता है।^[13] हालाँकि बहुरूपता की यह शैली कुछ मायनों में उपप्रकार की तुलना में कम लचीली है, विशेष रूप से प्रकार की बाधाओं में दिशात्मकता की कमी से निपटने के लिए कड़ाई से आवश्यकता से अधिक बहुरूपता की आवश्यकता होती है, इसका लाभ यह है कि इसे मानक एचएम एल्गोरिदम के साथ काफी आसानी से एकीकृत किया जा सकता है।

↑ Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community.
↑ Polytypes are called "type schemes" in the original article.
↑ The parametric types $C\ \tau \dots \tau$ were not present in the original paper on HM and are not needed to present the method. None of the inference rules below will take care or even note them. The same holds for the non-parametric "primitive types" in said paper. All the machinery for polymorphic type inference can be defined without them. They have been included here for sake of examples but also because the nature of HM is all about parametric types. This comes from the function type $\tau \rightarrow \tau$ , hard-wired in the inference rules, below, which already has two parameters and has been presented here as only a special case.
↑ Haskell provides the ScopedTypeVariables language extension allowing to bring all-quantified type variables into scope.

संदर्भ

↑ Hindley, J. Roger (1969). "संयोजन तर्क में किसी वस्तु की प्रमुख प्रकार-योजना". Transactions of the American Mathematical Society. 146: 29–60. doi:10.2307/1995158. JSTOR 1995158.
↑ ^2.0 ^2.1 ^2.2 Milner, Robin (1978). "प्रोग्रामिंग में टाइप पालीमॉर्फिज़्म का एक सिद्धांत". Journal of Computer and System Sciences. 17 (3): 348–374. CiteSeerX 10.1.1.67.5276. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.
↑ Damas, Luis (1985). प्रोग्रामिंग भाषाओं में असाइनमेंट टाइप करें (PhD thesis). University of Edinburgh. hdl:1842/13555. CST-33-85.
↑ ^4.0 ^4.1 ^4.2 Damas, Luis; Milner, Robin (1982). कार्यात्मक कार्यक्रमों के लिए प्रमुख प्रकार-योजनाएँ (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. pp. 207–212. doi:10.1145/582153.582176. ISBN 978-0-89791-065-1.
↑ Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences, 17 (3): 348–375, doi:10.1016/0022-0000(78)90014-4
↑ Wells, J.B. (1994). "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable". Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 176–185. doi:10.1109/LICS.1994.316068. ISBN 0-8186-6310-3. S2CID 15078292.
↑ Clement (1986). A Simple Applicative Language: Mini-ML. LFP'86. ACM. doi:10.1145/319838.319847. ISBN 978-0-89791-200-6.
↑ Vaughan, Jeff (July 23, 2008) [May 5, 2005]. "A proof of correctness for the Hindley–Milner type inference algorithm" (PDF). Archived from the original (PDF) on 2012-03-24. {{cite journal}}: Cite journal requires |journal= (help)
↑ Pottier, François (1998). Type Inference in the Presence of Subtyping: from Theory to Practice (Thesis). Retrieved 2021-08-10.
↑ Dolan, Stephen; Mycroft, Alan (2017). "Polymorphism, subtyping, and type inference in MLsub". POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. doi:10.1145/3009837.3009882.
↑ Parreaux, Lionel (2020). "The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy". 25th ACM SIGPLAN International Conference on Functional Programming - ICFP 2020, [Online event], August 24-26, 2020. doi:10.1145/3409006.
↑ Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "An extension of system F with subtyping". Information and Computation, vol. 9. North Holland, Amsterdam. pp. 4–56. doi:10.1006/inco.1994.1013.
↑ Daan Leijen, Extensible records with scoped labels, Institute of Information and Computing Sciences, Utrecht University, Draft, Revision: 76, July 23, 2005

Mairson, Harry G. (1990). "Deciding ML typability is complete for deterministic exponential time". Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. pp. 382–401. doi:10.1145/96709.96748. ISBN 978-0-89791-343-0. S2CID 75336. {{cite book}}: |journal= ignored (help)
Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P. (1990). ML typability is dexptime-complete. pp. 206–220. doi:10.1007/3-540-52590-4_50. ISBN 978-3-540-52590-5. {{cite book}}: |journal= ignored (help)

बाहरी संबंध

[5] Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community.

[8] Polytypes are called "type schemes" in the original article.

[9] The parametric types $C\ \tau \dots \tau$ were not present in the original paper on HM and are not needed to present the method. None of the inference rules below will take care or even note them. The same holds for the non-parametric "primitive types" in said paper. All the machinery for polymorphic type inference can be defined without them. They have been included here for sake of examples but also because the nature of HM is all about parametric types. This comes from the function type $\tau \rightarrow \tau$ , hard-wired in the inference rules, below, which already has two parameters and has been presented here as only a special case.

[10] Haskell provides the ScopedTypeVariables language extension allowing to bring all-quantified type variables into scope.

[1] Hindley, J. Roger (1969). "संयोजन तर्क में किसी वस्तु की प्रमुख प्रकार-योजना". Transactions of the American Mathematical Society. 146: 29–60. doi:10.2307/1995158. JSTOR 1995158.

[Milner-2] 2.0 ^2.1 ^2.2 Milner, Robin (1978). "प्रोग्रामिंग में टाइप पालीमॉर्फिज़्म का एक सिद्धांत". Journal of Computer and System Sciences. 17 (3): 348–374. CiteSeerX 10.1.1.67.5276. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.

[3] Damas, Luis (1985). प्रोग्रामिंग भाषाओं में असाइनमेंट टाइप करें (PhD thesis). University of Edinburgh. hdl:1842/13555. CST-33-85.

[Damas-4] 4.0 ^4.1 ^4.2 Damas, Luis; Milner, Robin (1982). कार्यात्मक कार्यक्रमों के लिए प्रमुख प्रकार-योजनाएँ (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. pp. 207–212. doi:10.1145/582153.582176. ISBN 978-0-89791-065-1.

[6] Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences, 17 (3): 348–375, doi:10.1016/0022-0000(78)90014-4

[7] Wells, J.B. (1994). "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable". Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 176–185. doi:10.1109/LICS.1994.316068. ISBN 0-8186-6310-3. S2CID 15078292.

[11] Clement (1986). A Simple Applicative Language: Mini-ML. LFP'86. ACM. doi:10.1145/319838.319847. ISBN 978-0-89791-200-6.

[x-12] Vaughan, Jeff (July 23, 2008) [May 5, 2005]. "A proof of correctness for the Hindley–Milner type inference algorithm" (PDF). Archived from the original (PDF) on 2012-03-24. {{cite journal}}: Cite journal requires |journal= (help)

[13] Pottier, François (1998). Type Inference in the Presence of Subtyping: from Theory to Practice (Thesis). Retrieved 2021-08-10.

[14] Dolan, Stephen; Mycroft, Alan (2017). "Polymorphism, subtyping, and type inference in MLsub". POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. doi:10.1145/3009837.3009882.

[15] Parreaux, Lionel (2020). "The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy". 25th ACM SIGPLAN International Conference on Functional Programming - ICFP 2020, [Online event], August 24-26, 2020. doi:10.1145/3409006.

[16] Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "An extension of system F with subtyping". Information and Computation, vol. 9. North Holland, Amsterdam. pp. 4–56. doi:10.1006/inco.1994.1013.

[17] Daan Leijen, Extensible records with scoped labels, Institute of Information and Computing Sciences, Utrecht University, Draft, Revision: 76, July 23, 2005

[1]

[2]

[3]

[4]

[note 1]

[5]

[6]

[note 2]

[note 3]

[note 4]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

Expressions
${\begin{array}{lrll}\\e&=&x&{\textrm {variable}}\\&\vert &e_{1}\ e_{2}&{\textrm {application}}\\&\vert &\lambda \ x\ .\ e&{\textrm {abstraction}}\\&\vert &{\mathtt {let}}\ x=e_{1}\ {\mathtt {in}}\ e_{2}&\\\\\end{array}}$
Types
${\begin{array}{llrll}\\{\textrm {mono}}&\tau &=&\alpha &\ {\textrm {variable}}\\&&\vert &C\ \tau \dots \tau &\ {\textrm {application}}\\{\textrm {poly}}&\sigma &=&\tau \\&&\vert &\forall \ \alpha \ .\ \sigma &\ {\textrm {quantifier}}\\\\\end{array}}$
Context and Typing
${\begin{array}{llrl}\\{\text{Context}}&\Gamma &=&\epsilon \ {\mathtt {(empty)}}\\&&\vert &\Gamma ,\ x:\sigma \\{\text{Typing}}&&=&\Gamma \vdash e:\sigma \\\\\end{array}}$
Free Type Variables
${\begin{array}{ll}\\{\text{free}}(\ \alpha \ )&=\ \left\{\alpha \right\}\\{\text{free}}(\ C\ \tau _{1}\dots \tau _{n}\ )&=\ \bigcup \limits _{i=1}^{n}{{\text{free}}(\ \tau _{i}\ )}\\{\text{free}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{free}}(\ \sigma \ )\\\\{\text{free}}(\ \forall \ \alpha \ .\ \sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ \left\{\alpha \right\}\\{\text{free}}(\ \Gamma \vdash e:\sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ {\text{free}}(\ \Gamma \ )\\\\\end{array}}$

The Syntax of Rules
${\begin{array}{lrl}{\text{Predicate}}&=&\sigma \sqsubseteq \sigma '\\&\vert \ &\alpha \not \in free(\Gamma )\\&\vert \ &x:\alpha \in \Gamma \\\\{\text{Judgment}}&=&{\text{Typing}}\\{\text{Premise}}&=&{\text{Judgment}}\ \vert \ {\text{Predicate}}\\{\text{Conclusion}}&=&{\text{Judgment}}\\\\{\text{Rule}}&=&\displaystyle {\frac {{\textrm {Premise}}\ \dots }{\textrm {Conclusion}}}\quad [{\mathtt {Name}}]\end{array}}$

Anonymous

Search

हिंडले-मिलनर टाइप सिस्टम

परिचय

एकरूपता बनाम बहुरूपता

मान लीजिए-बहुरूपता

सिंहावलोकन

हिंडले-मिलनर प्रकार प्रणाली

सिंटेक्स

मोनोटाइप्स

बहुप्रकार

प्रसंग और टाइपिंग

मुक्त प्रकार के चर

ऑर्डर टाइप करें

प्रमुख प्रकार

टाइपिंग में प्रतिस्थापन

निगमनात्मक प्रणाली

टाइपिंग नियम

मान लीजिए-बहुरूपता

सामान्यीकरण नियम

एक अनुमान एल्गोरिथ्म

नियमों को चुनने की स्वतंत्रता की डिग्री

सिंटैक्स-निर्देशित नियम प्रणाली

नियमों को लागू करने वाली स्वतंत्रता की डिग्री

एल्गोरिदम एक्स

एल्गोरिथ्म साबित करना

एल्गोरिथम Ω

प्रमाण दायित्व

एक्सटेंशन

पुनरावर्ती परिभाषाएँ

टाइपिंग नियम

परिणाम

ओवरलोडिंग

उच्च-क्रम प्रकार

उपप्रकार

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories