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

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

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

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

	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

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

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

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

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

रैखिक प्रकार सिस्टम

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

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

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

Affine प्रकार सिस्टम

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

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

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

प्रोग्रामिंग लैंग्वेज

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

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

यह भी देखें

• प्रभाव प्रणाली
• रैखिक तर्क
• तर्क तर्क