उपसंरचनात्मक प्रकार की प्रणाली

सबस्ट्रक्चरल प्रकार प्रणाली अवसंरचनात्मक तर्क ्स के अनुरूप टाइप सिस्टम का एक परिवार है जहां एक या अधिक संरचनात्मक नियम अनुपस्थित हैं या केवल नियंत्रित परिस्थितियों में ही अनुमति दी जाती है। ऐसी प्रणालियाँ राज्य में होने वाले परिवर्तनों पर नज़र रखकर और अमान्य स्थितियों को रोककर कम्प्यूटर फाइल, लॉक (कंप्यूटर विज्ञान), और स्मृति जैसे सिस्टम संसाधनों तक पहुंच को बाधित करने के लिए उपयोगी होती हैं।

विभिन्न अवसंरचनात्मक प्रकार की प्रणालियाँ

विनिमय, क्षीणन और संकुचन के कुछ संरचनात्मक नियमों को त्यागकर कई प्रकार की प्रणालियाँ उभरी हैं:

	Exchange	Weakening	Contraction	Use
Ordered	—	—	—	Exactly once in order
Linear	Allowed	—	—	Exactly once
Affine	Allowed	Allowed	—	At most once
Relevant	Allowed	—	Allowed	At least once
Normal	Allowed	Allowed	Allowed	Arbitrarily

• आदेशित प्रकार की प्रणालियाँ (विनिमय, कमज़ोरी और संकुचन को त्यागें): प्रत्येक चर का उपयोग उसी क्रम में ठीक एक बार किया जाता है जिस क्रम में इसे पेश किया गया था।
• रैखिक प्रकार की प्रणालियाँ (विनिमय की अनुमति देती हैं, लेकिन न तो कमजोर होती हैं और न ही संकुचन): प्रत्येक चर का उपयोग बिल्कुल एक बार किया जाता है।
• एफ़िन प्रकार की प्रणालियाँ (विनिमय और कमज़ोर होने की अनुमति देती हैं, लेकिन संकुचन की नहीं): प्रत्येक चर का उपयोग अधिकतम एक बार किया जाता है।
• प्रासंगिक प्रकार की प्रणालियाँ (विनिमय और संकुचन की अनुमति देती हैं, लेकिन कमज़ोर नहीं): प्रत्येक चर का उपयोग कम से कम एक बार किया जाता है।
• सामान्य प्रकार की प्रणालियाँ (विनिमय, कमज़ोरी और संकुचन की अनुमति): प्रत्येक चर का उपयोग मनमाने ढंग से किया जा सकता है।

एफ़िन प्रकार की प्रणालियों के लिए स्पष्टीकरण को सबसे अच्छी तरह से समझा जा सकता है यदि इसे "एक चर की प्रत्येक घटना का अधिकतम एक बार उपयोग किया जाता है" के रूप में दोहराया जाए।

आदेशित प्रकार प्रणाली

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

रैखिक प्रकार की प्रणालियाँ

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

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

एक रैखिक प्रकार की प्रणाली C++ के समान है unique_ptr क्लास (कंप्यूटर प्रोग्रामिंग), जो एक पॉइंटर की तरह व्यवहार करता है लेकिन इसे किसी असाइनमेंट में केवल स्थानांतरित किया जा सकता है (यानी, कॉपी नहीं किया जा सकता)। यद्यपि संकलन समय पर रैखिकता बाधा की जांच की जाती है, लेकिन इसे अमान्य कर दिया जाता है unique_ptr रनटाइम (प्रोग्राम जीवनचक्र चरण) पर अपरिभाषित व्यवहार का कारण बनता है। इसी प्रकार, रस्ट (प्रोग्रामिंग भाषा) भाषा को लिंट एनोटेशन के उपयोग के माध्यम से रैखिक प्रकारों का आंशिक समर्थन प्राप्त है लेकिन C++ से भिन्न वेरिएबल से स्थानांतरित किए गए वेरिएबल का दोबारा उपयोग नहीं किया जा सकता है। एकल-संदर्भ संपत्ति रैखिक प्रकार की प्रणालियों को क्वांटम कम्प्यूटिंग के लिए प्रोग्रामिंग भाषाओं के रूप में उपयुक्त बनाती है, क्योंकि यह क्वांटम राज्यों के नो-क्लोनिंग प्रमेय को दर्शाती है। श्रेणी सिद्धांत के दृष्टिकोण से, नो-क्लोनिंग एक कथन है कि कोई विकर्ण फ़ैक्टर नहीं है जो राज्यों की नकल कर सके; इसी प्रकार, संयोजनात्मक तर्क के दृष्टिकोण से, कोई K-संयोजक नहीं है जो राज्यों को नष्ट कर सके। सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस दृष्टिकोण से, एक चर x एक पद में बिल्कुल एक बार प्रकट हो सकता है। रैखिक प्रकार की प्रणालियाँ बंद मोनोइडल श्रेणी की आंतरिक भाषा हैं, ठीक उसी तरह जैसे कि बस टाइप किया गया लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक सटीक रूप से, कोई रैखिक प्रकार प्रणालियों की श्रेणी और बंद सममित मोनोइडल श्रेणियों की श्रेणी के बीच ऑपरेटर का निर्माण कर सकता है।

एफ़िन प्रकार की प्रणालियाँ

एफ़िन प्रकार रैखिक प्रकारों का एक संस्करण है जो एफ़िन तर्क के अनुरूप किसी संसाधन को त्यागने (यानी उपयोग नहीं करने) की अनुमति देता है। एक एफ़िन संसाधन का उपयोग अधिकतम एक बार किया जा सकता है, जबकि एक रैखिक संसाधन का उपयोग ठीक एक बार किया जाना चाहिए।

प्रासंगिक प्रकार प्रणाली

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

प्रोग्रामिंग भाषाएँ

निम्नलिखित प्रोग्रामिंग भाषाएँ रैखिक या एफ़िन प्रकारों का समर्थन करती हैं:

• सी++
• एटीएस (प्रोग्रामिंग भाषा)
• स्वच्छ (प्रोग्रामिंग भाषा)
• इदरीस (प्रोग्रामिंग भाषा)
• बुध (प्रोग्रामिंग भाषा)
• एफ* (प्रोग्रामिंग भाषा)|एफ*
• LinearML
• Alms
• ग्लासगो हास्केल कंपाइलर (जीएचसी) 9.0.1 या इसके बाद के संस्करण के साथ हास्केल
• ग्रेन्युल
• जंग (प्रोग्रामिंग भाषा)
• निम (प्रोग्रामिंग भाषा)

यह भी देखें

• प्रभाव प्रणाली
• रेखीय तर्क
• तर्क को ठीक करें