आश्रित और उप-संरचनात्मक प्रकार

आश्रित प्रकार मानों पर प्रकारों को निर्भर करने देते हैं, जिससे सटीक विशिष्टताएँ सक्षम होती हैं, जबकि रैखिक और एफाइन प्रकार जैसे उप-संरचनात्मक प्रकार संसाधनों का उपयोग कैसे किया जाता है, इसे नियंत्रित करते हैं।

Definition

आश्रित प्रकार वे प्रकार होते हैं जो मानों पर निर्भर करते हैं, जिससे सटीक गुणों को प्रकार स्तर पर बताया और जांचा जा सकता है; उप-संरचनात्मक प्रकार प्रणालियाँ यह प्रतिबंधित करती हैं कि चर (संसाधनों) को कैसे दोहराया या छोड़ा जा सकता है, जिसमें रैखिक प्रकारों को प्रत्येक का ठीक एक बार उपयोग करने की आवश्यकता होती है।

Scope

यह विषय उन्नत टाइपिंग विषयों को शामिल करता है जो पारंपरिक प्रणालियों से परे जाते हैं: आश्रित प्रकार, जिसमें प्रकार प्रोग्राम मानों का उल्लेख कर सकते हैं, जिससे प्रकारों को पूर्ण विशिष्टताओं को व्यक्त करने और प्रमाण के रूप में कार्य करने की अनुमति मिलती है; और उप-संरचनात्मक प्रकार (रैखिक, एफाइन, स्वामित्व), जो संकुचन और कमजोर पड़ने के संरचनात्मक नियमों को प्रतिबंधित करते हैं ताकि संसाधन उपयोग, उपनाम और जीवनकाल को ट्रैक किया जा सके। यह करी-हावर्ड पत्राचार और प्रूफ असिस्टेंट से जुड़ता है।

Core questions

• पूर्ण प्रोग्राम विशिष्टताओं को व्यक्त करने के लिए प्रकार मानों पर कैसे निर्भर कर सकते हैं?
• आश्रित प्रकारों और रचनात्मक प्रमाणों के बीच क्या संबंध है?
• रैखिक और एफाइन प्रकार संसाधनों, स्वामित्व और मेमोरी सुरक्षा को कैसे मॉडल करते हैं?
• इन समृद्ध प्रणालियों की निर्णयक्षमता और उपयोगिता में क्या व्यापार-बंद हैं?

Key theories

अंतर्ज्ञानवादी (आश्रित) प्रकार सिद्धांत

मार्टिन-लोफ का प्रकार सिद्धांत प्रोग्रामिंग और रचनात्मक तर्क को एकीकृत करता है ताकि प्रकार प्रस्ताव हों और प्रोग्राम प्रमाण हों, जो आश्रित प्रकार की भाषाओं और प्रूफ असिस्टेंट के लिए आधार प्रदान करता है।

रैखिक तर्क और रैखिक प्रकार

गिरार्ड का रैखिक तर्क संरचनात्मक नियमों को नियंत्रित करके शास्त्रीय और अंतर्ज्ञानवादी तर्क को परिष्कृत करता है, और वाडलर ने दिखाया कि इस पर निर्मित रैखिक प्रकार इन-प्लेस अपडेट और संसाधन उपयोग को सुरक्षित रूप से प्रबंधित कर सकते हैं।

उप-संरचनात्मक प्रणालियों के लिए स्थैतिकी

हार्पर उप-संरचनात्मक और अन्य उन्नत प्रकार प्रणालियों के मेटाथ्योरी को एक समान स्थैतिकी-और-गतिशीलता ढांचे के भीतर विकसित करता है, उनकी सुदृढ़ता और संसाधन व्याख्या को स्पष्ट करता है।

Clinical relevance

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

History

मार्टिन-लोफ के अंतर्ज्ञानवादी प्रकार सिद्धांत (1970-1980 के दशक) ने आश्रित प्रकारों और प्रस्ताव-के-रूप-में-प्रकार के दृष्टिकोण को स्थापित किया, जिससे Coq, Agda और Lean जैसे प्रूफ असिस्टेंट का विकास हुआ। गिरार्ड के 1987 के रैखिक तर्क ने संसाधन-संवेदनशील तर्क पेश किया; वाडलर के रैखिक प्रकार इसे भाषा डिजाइन में लाए, और स्वामित्व और उधार-जांच विषयों ने बाद में सिस्टम प्रोग्रामिंग में उप-संरचनात्मक विचारों को मुख्यधारा में ला दिया।

Debates

अभिव्यंजकता बनाम उपयोगिता और निर्णयक्षमता

आश्रित प्रकार की और उप-संरचनात्मक प्रणालियाँ बहुत मजबूत गारंटी व्यक्त कर सकती हैं, लेकिन वे प्रोग्रामर पर बोझ बढ़ाती हैं और प्रकार की जाँच को अनिर्णायक या बोझिल बना सकती हैं, जिससे यह बहस छिड़ जाती है कि कितनी शक्ति लागत के लायक है।

Key figures

• Per Martin-Löf
• Jean-Yves Girard
• Philip Wadler
• Robert Harper

Seminal works

• martinlof1984
• girard1987
• wadler1990
• harper2016

Frequently asked questions

आश्रित प्रकार क्या है?

एक आश्रित प्रकार एक ऐसा प्रकार है जिसकी परिभाषा एक मान पर निर्भर करती है, जैसे कि एक विशिष्ट लंबाई के सदिशों का प्रकार, जो प्रकार प्रणाली को समृद्ध अपरिवर्तनीयताओं को लागू करने देता है जिन्हें सामान्य प्रकार व्यक्त नहीं कर सकते हैं।

रैखिक प्रकार क्या गारंटी देते हैं?

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