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

From Vigyanwiki
No edit summary
No edit summary
Line 1: Line 1:
{{Type systems}}
{{Type systems}}


सबस्ट्रक्चरल [[ प्रकार प्रणाली |प्रकार प्रणाली]] [[ अवसंरचनात्मक तर्क |अवसंरचनात्मक तर्क]] ्स के अनुरूप टाइप सिस्टम का परिवार है जहां या अधिक [[संरचनात्मक नियम]] अनुपस्थित हैं या केवल नियंत्रित परिस्थितियों में अनुमति दी गई है। ऐसी प्रणालियाँ [[सिस्टम संसाधन]]ों जैसे कि [[कम्प्यूटर फाइल]], लॉक (कंप्यूटर विज्ञान), और [[ स्मृति |स्मृति]] तक पहुँच को बाधित करने के लिए उपयोगी होती हैं, जो राज्य में होने वाले परिवर्तनों पर नज़र रखती हैं और अमान्य अवस्थाओं को रोकती हैं।<ref name="Walker">{{cite book |first=David |last=Walker |editor1-first=Benjamin C. |editor1-last=Pierce |editor1-link=Benjamin C. Pierce |year=2002 |title=प्रकार और प्रोग्रामिंग भाषाओं में उन्नत विषय|publisher=MIT Press |isbn=0-262-16228-8 |chapter=Substructural Type Systems |pages=3–43 |url=https://mitpress-request.mit.edu/sites/default/files/titles/content/9780262162289_sch_0001.pdf}}</ref>{{rp|p=4}}
 
अवसंरचनात्मक [[ प्रकार प्रणाली |प्रकार प्रणाली]] [[ अवसंरचनात्मक तर्क |अवसंरचनात्मक लॉजिक्स]] अनुरूप प्रकार प्रणाली  का वर्ग है जहां एक या अधिक संरचनात्मक नियम अनुपस्थित हैं या केवल नियंत्रित परिस्थितियों में ही अनुमति दी जाती है। ऐसे प्रणाली  स्थिती  में होने वाले परिवर्तनों पर दृष्टि रखकर और अमान्य स्थितियों को रोककर प्रणाली  संसाधनों जैसे फ़ाइलों, लॉक और मेमोरी तक पहुंच को बाधित करने के लिए उपयोगी होते हैं।।<ref name="Walker">{{cite book |first=David |last=Walker |editor1-first=Benjamin C. |editor1-last=Pierce |editor1-link=Benjamin C. Pierce |year=2002 |title=प्रकार और प्रोग्रामिंग भाषाओं में उन्नत विषय|publisher=MIT Press |isbn=0-262-16228-8 |chapter=Substructural Type Systems |pages=3–43 |url=https://mitpress-request.mit.edu/sites/default/files/titles/content/9780262162289_sch_0001.pdf}}</ref>{{rp|p=4}}


== विभिन्न अवसंरचनात्मक प्रकार की प्रणालियाँ ==
== विभिन्न अवसंरचनात्मक प्रकार की प्रणालियाँ ==
विनिमय, कमजोर पड़ने और संकुचन के कुछ संरचनात्मक नियमों को त्याग कर कई प्रकार की प्रणालियाँ उभरी हैं:
विनिमय अशक्त पड़ने और संकुचन के कुछ संरचनात्मक नियमों को त्याग कर कई प्रकार की प्रणालियाँ उभरी हैं:
{| class="wikitable"
{| class="wikitable"
|+
|+
!
!
!Exchange
!विनिमय
!Weakening
!अशक्ति
!Contraction
!संकुचन
!Use
!प्रयोग
|-
|-
!Ordered
!आर्डर
|{{sdash}}
|{{sdash}}
|{{sdash}}
|{{sdash}}
|{{sdash}}
|{{sdash}}
|Exactly once in order
|क्रम में पूर्ण रूप से एक बार
|-
|-
!Linear
!लीनियर
|Allowed
|अनुमत
|{{sdash}}
|{{sdash}}
|{{sdash}}
|{{sdash}}
|Exactly once
|पूर्ण रूप से एक बार
|-
|-
!Affine
!एफ़िन
|Allowed
|अनुमत
|Allowed
|अनुमत
|{{sdash}}
|{{sdash}}
|At most once
|अधिक से अधिक एक बार
|-
|-
!Relevant
!रिलेवेंट
|Allowed
|अनुमत
|{{sdash}}
|{{sdash}}
|Allowed
|अनुमत
|At least once
|कम से कम एक बार
|-
|-
!Normal
!नार्मल
|Allowed
|अनुमत
|Allowed
|अनुमत
|Allowed
|अनुमत
|Arbitrarily
|स्वेच्छया
|}
|}
*आदेशित प्रकार की प्रणालियाँ (विनिमय, कमज़ोरी और संकुचन त्यागें): प्रत्येक चर का उपयोग ठीक उसी क्रम में बार किया जाता है जिस क्रम में इसे पेश किया गया था।
*आदेशित प्रकार की प्रणालियाँ (विनिमय, दुर्बलता और संकुचन त्यागें): प्रत्येक चर का उपयोग ठीक उसी क्रम में बार किया जाता है जिस क्रम में इसे प्रस्तुत किया गया था।
*रैखिक प्रकार की प्रणालियाँ (विनिमय की अनुमति देती हैं, लेकिन न तो कमजोर होती हैं और न ही संकुचन): प्रत्येक चर का उपयोग ठीक बार किया जाता है।
*रैखिक प्रकार की प्रणालियाँ (विनिमय की अनुमति देती हैं, किंतु न तो अशक्त होती हैं और न ही संकुचन): प्रत्येक चर का उपयोग ठीक बार किया जाता है।
*एफ़ाइन प्रकार की प्रणालियाँ (विनिमय और कमजोर करने की अनुमति दें, लेकिन संकुचन नहीं): प्रत्येक चर का अधिकतम बार उपयोग किया जाता है।
*एफ़ाइन प्रकार की प्रणालियाँ (विनिमय और अशक्त करने की अनुमति दें, किंतु संकुचन नहीं): प्रत्येक चर का अधिकतम बार उपयोग किया जाता है।
*प्रासंगिक प्रकार की प्रणालियाँ (विनिमय और संकुचन की अनुमति दें, लेकिन कमजोर नहीं): प्रत्येक चर का उपयोग कम से कम बार किया जाता है।
*प्रासंगिक प्रकार की प्रणालियाँ (विनिमय और संकुचन की अनुमति दें, किंतु अशक्त नहीं): प्रत्येक चर का उपयोग कम से कम बार किया जाता है।
* सामान्य प्रकार की प्रणालियाँ (विनिमय, कमजोर और संकुचन की अनुमति दें): प्रत्येक चर का मनमाने ढंग से उपयोग किया जा सकता है।
* सामान्य प्रकार की प्रणालियाँ (विनिमय, अशक्त और संकुचन की अनुमति दें): प्रत्येक चर का इच्छानुसार रूप से उपयोग किया जा सकता है।


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


=== आदेशित प्रकार प्रणाली ===
=== आदेशित प्रकार प्रणाली ===
आदेशित प्रकार गैर-अनुवांशिक तर्क के अनुरूप होते हैं जहां विनिमय, संकुचन और कमजोर पड़ने को छोड़ दिया जाता है। इसका उपयोग [[स्टैक-आधारित मेमोरी आवंटन]] को मॉडल करने के लिए किया जा सकता है (रैखिक प्रकारों के विपरीत जो मॉडल [[हीप-आधारित मेमोरी आवंटन]] के लिए इस्तेमाल किया जा सकता है)।<ref name="Walker"/>{{rp|pp=30–31}} विनिमय संपत्ति के बिना, वस्तु का उपयोग केवल तभी किया जा सकता है जब मॉडल किए गए स्टैक के शीर्ष पर, जिसके बाद इसे बंद कर दिया जाता है, जिसके परिणामस्वरूप प्रत्येक चर को उसी क्रम में बार उपयोग किया जाता है जिस क्रम में इसे पेश किया गया था।
आदेशित प्रकार गैर-अनुवांशिक तर्क के अनुरूप होते हैं जहां विनिमय, संकुचन और अशक्त पड़ने को छोड़ दिया जाता है। इसका उपयोग [[स्टैक-आधारित मेमोरी आवंटन]] को मॉडल करने के लिए किया जा सकता है (रैखिक प्रकारों के विपरीत जो मॉडल [[हीप-आधारित मेमोरी आवंटन]] के लिए उपयोग किया जा सकता है)।<ref name="Walker"/>{{rp|pp=30–31}} विनिमय गुण  के बिना वस्तु का उपयोग केवल तभी किया जा सकता है जब मॉडल किए गए स्टैक के शीर्ष पर जिसके बाद इसे बंद कर दिया जाता है, जिसके परिणामस्वरूप प्रत्येक चर को उसी क्रम में बार उपयोग किया जाता है जिस क्रम में इसे प्रस्तुत किया गया था।
 
=== रैखिक प्रकार प्रणाली ===
रैखिक प्रकार रैखिक तर्क से मेल खाते हैं और यह सुनिश्चित करते हैं कि वस्तुओं का उपयोग ठीक एक बार किया जाता है। यह प्रणाली को किसी ऑब्जेक्ट को उसके उपयोग के बाद सुरक्षित रूप से हटाने की अनुमति देता है,,<ref name="Walker"/>{{rp|p=6}}  या सॉफ़्टवेयर इंटरफ़ेस डिज़ाइन करने की अनुमति देता है जो आश्वासन देता है कि संसाधन को बंद होने या किसी भिन्न स्थिति में स्थानांतरित होने के बाद उपयोग नहीं किया जा सकता है।<ref name="BernardyEtAl">{{cite journal |title=Linear Haskell: practical linearity in a higher-order polymorphic language |last1=Bernardy |first1=Jean-Philippe |last2=Boespflug |first2=Mathieu |last3=Newton |first3=Ryan R |last4=Peyton Jones |first4=Simon |author4-link=Simon Peyton Jones |last5=Spiwack |first5=Arnaud |journal=Proceedings of the ACM on Programming Languages |volume=2 |year=2017 |pages=1–29 |doi=10.1145/3158093 |arxiv=1710.09756 |s2cid=9019395 |url=https://dl.acm.org/doi/pdf/10.1145/3158093}}</ref>
 
स्वच्छ प्रोग्रामिंग भाषा समवर्तीता, इनपुट/आउटपुट और सरणियों के इन-प्लेस अपडेट का समर्थन करने के लिए विशिष्टता प्रकारों (रैखिक प्रकारों का एक प्रकार) का उपयोग करती है।<ref name="Walker" />{{rp|p=43}}
 
रैखिक प्रकार की प्रणालियाँ [[संदर्भ (कंप्यूटर विज्ञान)]] की अनुमति देती हैं, किंतु [[अलियासिंग (कंप्यूटिंग)]] की नहीं इसे प्रयुक्त करने के लिए, [[असाइनमेंट (कंप्यूटर विज्ञान)]] के दाईं ओर दिखाई देने के बाद संदर्भ सीमा (प्रोग्रामिंग) से बाहर हो जाता है, इस प्रकार यह सुनिश्चित करता है कि किसी वस्तु का केवल ही संदर्भ बार में उपस्थित है। ध्यान दें कि फ़ंक्शन (कंप्यूटर प्रोग्रामिंग) के लिए [[पैरामीटर (कंप्यूटर प्रोग्रामिंग)]] के रूप में संदर्भ पास करना असाइनमेंट का रूप है क्योंकि फ़ंक्शन पैरामीटर को फ़ंक्शन के अंदर मान असाइन किया जाएगा, और इसलिए संदर्भ के इस तरह के उपयोग से यह सीमा से बाहर हो जाता है।
 
एक रेखीय प्रकार प्रणाली [[C++]] के<code>[[unique_ptr]]</code> [[वर्ग (कंप्यूटर प्रोग्रामिंग)]],  समान है  जो सूचक की तरह व्यवहार करता है किंतु केवल असाइनमेंट में स्थानांतरित किया जा सकता है (अथार्त, कॉपी नहीं किया गया)। चूँकि  रैखिकता बाधा [[संकलन समय]] पर जांच की जाती है, अमान्य  <code>unique_ptr</code>  को डीरेफ़रेंस करने से रन टाइम पर अपरिभाषित व्यवहार होता है।<ref>{{Cite web |title=std::unique_ptr - cppreference.com |url=https://en.cppreference.com/w/cpp/memory/unique_ptr |access-date=2023-05-14 |website=en.cppreference.com}}</ref> इसी तरह, [[ जंग (प्रोग्रामिंग भाषा) |रस्ट (प्रोग्रामिंग भाषा)]] भाषा को लिंट एनोटेशन के माध्यम से रैखिक प्रकारों के लिए आंशिक समर्थन प्राप्त है<ref>{{Cite web |title=must_use {{!}} Diagnostics - The Rust Reference |url=https://doc.rust-lang.org/reference/attributes/diagnostics.html#the-must_use-attribute |access-date=2023-05-14 |website=doc.rust-lang.org}}</ref> किंतु [[C++]] से अलग चर से स्थानांतरित फिर से उपयोग नहीं किया जा सकता है।<ref>{{Cite web |last=Vít |first=Radek |date=2021-02-10 |title=Move semantics in C++ and Rust: The case for destructive moves |url=https://radekvit.medium.com/move-semantics-in-c-and-rust-the-case-for-destructive-moves-d816891c354b |access-date=2023-05-14 |website=Medium |language=en}}</ref>


=== रैखिक प्रकार सिस्टम ===
एकल-संदर्भ गुण रैखिक प्रकार की प्रणालियों को [[ क्वांटम कम्प्यूटिंग |क्वांटम कम्प्यूटिंग]] के लिए प्रोग्रामिंग भाषाओं के रूप में उपयुक्त बनाती है, क्योंकि यह क्वांटम अवस्था के [[नो-क्लोनिंग प्रमेय]] को दर्शाती है। [[श्रेणी सिद्धांत]] के दृष्टिकोण से, नो-क्लोनिंग कथन है कि कोई विकर्ण कारक नहीं है जो अवस्था को डुप्लिकेट कर सकता है; इसी तरह, [[संयोजन तर्क]] के दृष्टिकोण से, कोई के-कॉम्बिनेटर नहीं है जो अवस्था को नष्ट कर सकता है । सरल रूप से प्रकार किए गए लैम्ब्डा कैलकुलस के दृष्टिकोण से, चर <code>x</code> अवधि में ठीक बार प्रकट हो सकता है।<ref name="Baez">{{cite book |last1=Baez |first1=John C. |last2=Stay |first2=Mike |url=http://math.ucr.edu/home/baez/rosetta/rose3.pdf |chapter=Physics, Topology, Logic and Computation: A Rosetta Stone |date=2010 |title=भौतिकी के लिए नई संरचनाएं|editor=Springer |pages=95–174}}</ref>
रैखिक प्रकार [[रैखिक तर्क]] से मेल खाते हैं और यह सुनिश्चित करते हैं कि वस्तुओं का बार उपयोग किया जाता है। यह सिस्टम को इसके उपयोग के बाद किसी वस्तु को सुरक्षित रूप से मेमोरी प्रबंधन करने की अनुमति देता है,<ref name="Walker"/>{{rp|p=6}} या [[एपीआई]] डिजाइन करने के लिए जो किसी संसाधन की गारंटी देता है कि इसे बार बंद कर दिया गया है या किसी भिन्न राज्य में स्थानांतरित कर दिया गया है।<ref name="BernardyEtAl">{{cite journal |title=Linear Haskell: practical linearity in a higher-order polymorphic language |last1=Bernardy |first1=Jean-Philippe |last2=Boespflug |first2=Mathieu |last3=Newton |first3=Ryan R |last4=Peyton Jones |first4=Simon |author4-link=Simon Peyton Jones |last5=Spiwack |first5=Arnaud |journal=Proceedings of the ACM on Programming Languages |volume=2 |year=2017 |pages=1–29 |doi=10.1145/3158093 |arxiv=1710.09756 |s2cid=9019395 |url=https://dl.acm.org/doi/pdf/10.1145/3158093}}</ref>
[[स्वच्छ (प्रोग्रामिंग भाषा)]] समरूपता, इनपुट/आउटपुट, और [[ऐरे (डेटा संरचना)]] के इन-प्लेस अपडेट का समर्थन करने में सहायता के लिए [[विशिष्टता प्रकार]] (रैखिक प्रकार का प्रकार) का उपयोग करता है।<ref name="Walker"/>{{rp|p=43}}


रैखिक प्रकार की प्रणालियाँ [[संदर्भ (कंप्यूटर विज्ञान)]] की अनुमति देती हैं, लेकिन [[अलियासिंग (कंप्यूटिंग)]] की नहीं। इसे लागू करने के लिए, [[असाइनमेंट (कंप्यूटर विज्ञान)]] के दाईं ओर दिखाई देने के बाद संदर्भ दायरे (प्रोग्रामिंग) से बाहर हो जाता है, इस प्रकार यह सुनिश्चित करता है कि किसी वस्तु का केवल ही संदर्भ बार में मौजूद है। ध्यान दें कि फ़ंक्शन (कंप्यूटर प्रोग्रामिंग) के लिए [[पैरामीटर (कंप्यूटर प्रोग्रामिंग)]] के रूप में संदर्भ पास करना असाइनमेंट का रूप है, क्योंकि फ़ंक्शन पैरामीटर को फ़ंक्शन के अंदर मान असाइन किया जाएगा, और इसलिए संदर्भ के इस तरह के उपयोग से यह भी जाता है दायरे से बाहर।
रेखीय प्रकार की प्रणालियाँ [[बंद मोनोइडल श्रेणी]] की [[आंतरिक भाषा]] हैं, ठीक उसी तरह जैसे कि बस प्रकार किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक स्पष्ट रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद सममित मोनोइडल श्रेणियों की श्रेणी के बीच फंक्शंस का निर्माण कर सकता है।<ref name="Ambler">{{cite thesis |title=सममित मोनोइडल बंद श्रेणियों में प्रथम क्रम तर्क|last=Ambler |first=S. |date=1991 |publisher=U. of Edinburgh |type=PhD |url=http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-194/}}</ref>


एक रेखीय प्रकार प्रणाली [[C++]] के समान है <code>[[unique_ptr]]</code> [[वर्ग (कंप्यूटर प्रोग्रामिंग)]], जो सूचक की तरह व्यवहार करता है लेकिन केवल असाइनमेंट में स्थानांतरित किया जा सकता है (यानी, कॉपी नहीं किया गया)। हालांकि रैखिकता बाधा [[संकलन समय]] पर जांच की जाती है, अमान्य को संदर्भित करना <code>unique_ptr</code> [[रनटाइम (कार्यक्रम जीवनचक्र चरण)]] पर अपरिभाषित व्यवहार का कारण बनता है।<ref>{{Cite web |title=std::unique_ptr - cppreference.com |url=https://en.cppreference.com/w/cpp/memory/unique_ptr |access-date=2023-05-14 |website=en.cppreference.com}}</ref> इसी तरह, [[ जंग (प्रोग्रामिंग भाषा) |जंग (प्रोग्रामिंग भाषा)]] भाषा को लिंट एनोटेशन के माध्यम से रैखिक प्रकारों के लिए आंशिक समर्थन प्राप्त है<ref>{{Cite web |title=must_use {{!}} Diagnostics - The Rust Reference |url=https://doc.rust-lang.org/reference/attributes/diagnostics.html#the-must_use-attribute |access-date=2023-05-14 |website=doc.rust-lang.org}}</ref> लेकिन सी ++ से अलग चर से स्थानांतरित फिर से उपयोग नहीं किया जा सकता है।<ref>{{Cite web |last=Vít |first=Radek |date=2021-02-10 |title=Move semantics in C++ and Rust: The case for destructive moves |url=https://radekvit.medium.com/move-semantics-in-c-and-rust-the-case-for-destructive-moves-d816891c354b |access-date=2023-05-14 |website=Medium |language=en}}</ref>
एकल-संदर्भ संपत्ति रैखिक प्रकार की प्रणालियों को [[ क्वांटम कम्प्यूटिंग |क्वांटम कम्प्यूटिंग]] के लिए प्रोग्रामिंग भाषाओं के रूप में उपयुक्त बनाती है, क्योंकि यह क्वांटम राज्यों के [[नो-क्लोनिंग प्रमेय]] को दर्शाती है। [[श्रेणी सिद्धांत]] के दृष्टिकोण से, नो-क्लोनिंग कथन है कि कोई विकर्ण फ़ैक्टर नहीं है जो राज्यों को डुप्लिकेट कर सकता है; इसी तरह, [[संयोजन तर्क]] के दृष्टिकोण से, कोई के-कॉम्बिनेटर नहीं है जो राज्यों को नष्ट कर सके। सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस के दृष्टिकोण से, चर <code>x</code> अवधि में ठीक बार प्रकट हो सकता है।<ref name="Baez">{{cite book |last1=Baez |first1=John C. |last2=Stay |first2=Mike |url=http://math.ucr.edu/home/baez/rosetta/rose3.pdf |chapter=Physics, Topology, Logic and Computation: A Rosetta Stone |date=2010 |title=भौतिकी के लिए नई संरचनाएं|editor=Springer |pages=95–174}}</ref>
रेखीय प्रकार की प्रणालियाँ [[बंद मोनोइडल श्रेणी]] की [[आंतरिक भाषा]] हैं, ठीक उसी तरह जैसे कि केवल टाइप किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक सटीक रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद सममित मोनोइडल श्रेणियों की श्रेणी के बीच फंक्शंस का निर्माण कर सकता है।<ref name="Ambler">{{cite thesis |title=सममित मोनोइडल बंद श्रेणियों में प्रथम क्रम तर्क|last=Ambler |first=S. |date=1991 |publisher=U. of Edinburgh |type=PhD |url=http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-194/}}</ref>




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


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


== प्रोग्रामिंग लैंग्वेज ==
== प्रोग्रामिंग लैंग्वेज ==
Line 78: Line 83:
* स्वच्छ (प्रोग्रामिंग भाषा)
* स्वच्छ (प्रोग्रामिंग भाषा)
* [[इदरीस (प्रोग्रामिंग भाषा)]]
* [[इदरीस (प्रोग्रामिंग भाषा)]]
* बुध (प्रोग्रामिंग भाषा)
* पारा (प्रोग्रामिंग भाषा)
* [[एफ * (प्रोग्रामिंग भाषा)]] | एफ *
* [[एफ * (प्रोग्रामिंग भाषा)]] | एफ *
* [https://github.com/pikatchu/LinearML LinearML]
* [https://github.com/pikatchu/LinearML LinearML]
Line 84: Line 89:
* ग्लासगो [[हास्केल]] कंपाइलर (जीएचसी) 9.0.1 या इसके बाद के संस्करण के साथ हास्केल<ref>{{Cite web |title=6.4.19. Linear types — Glasgow Haskell Compiler 9.7.20230513 User's Guide |url=https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html |access-date=2023-05-14 |website=ghc.gitlab.haskell.org}}</ref>
* ग्लासगो [[हास्केल]] कंपाइलर (जीएचसी) 9.0.1 या इसके बाद के संस्करण के साथ हास्केल<ref>{{Cite web |title=6.4.19. Linear types — Glasgow Haskell Compiler 9.7.20230513 User's Guide |url=https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html |access-date=2023-05-14 |website=ghc.gitlab.haskell.org}}</ref>
* [https://granule-project.github.io/ Granule]
* [https://granule-project.github.io/ Granule]
* जंग (प्रोग्रामिंग भाषा)
* रस्ट (प्रोग्रामिंग भाषा)
* [[निम (प्रोग्रामिंग भाषा)]]
* [[निम (प्रोग्रामिंग भाषा)]]
{{div col end}}
{{div col end}}
Line 91: Line 96:
* [[प्रभाव प्रणाली]]
* [[प्रभाव प्रणाली]]
* रैखिक तर्क
* रैखिक तर्क
* तर्क तर्क
* एफ़िन तर्क


== संदर्भ ==
== संदर्भ ==

Revision as of 11:45, 27 June 2023

Type systems
General concepts
Major categories
Minor categories


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

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

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

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

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

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

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

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

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

स्वच्छ प्रोग्रामिंग भाषा समवर्तीता, इनपुट/आउटपुट और सरणियों के इन-प्लेस अपडेट का समर्थन करने के लिए विशिष्टता प्रकारों (रैखिक प्रकारों का एक प्रकार) का उपयोग करती है।[1]: 43 

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

एक रेखीय प्रकार प्रणाली C++ केunique_ptr वर्ग (कंप्यूटर प्रोग्रामिंग), समान है जो सूचक की तरह व्यवहार करता है किंतु केवल असाइनमेंट में स्थानांतरित किया जा सकता है (अथार्त, कॉपी नहीं किया गया)। चूँकि रैखिकता बाधा संकलन समय पर जांच की जाती है, अमान्य unique_ptr को डीरेफ़रेंस करने से रन टाइम पर अपरिभाषित व्यवहार होता है।[3] इसी तरह, रस्ट (प्रोग्रामिंग भाषा) भाषा को लिंट एनोटेशन के माध्यम से रैखिक प्रकारों के लिए आंशिक समर्थन प्राप्त है[4] किंतु C++ से अलग चर से स्थानांतरित फिर से उपयोग नहीं किया जा सकता है।[5]

एकल-संदर्भ गुण रैखिक प्रकार की प्रणालियों को क्वांटम कम्प्यूटिंग के लिए प्रोग्रामिंग भाषाओं के रूप में उपयुक्त बनाती है, क्योंकि यह क्वांटम अवस्था के नो-क्लोनिंग प्रमेय को दर्शाती है। श्रेणी सिद्धांत के दृष्टिकोण से, नो-क्लोनिंग कथन है कि कोई विकर्ण कारक नहीं है जो अवस्था को डुप्लिकेट कर सकता है; इसी तरह, संयोजन तर्क के दृष्टिकोण से, कोई के-कॉम्बिनेटर नहीं है जो अवस्था को नष्ट कर सकता है । सरल रूप से प्रकार किए गए लैम्ब्डा कैलकुलस के दृष्टिकोण से, चर x अवधि में ठीक बार प्रकट हो सकता है।[6]

रेखीय प्रकार की प्रणालियाँ बंद मोनोइडल श्रेणी की आंतरिक भाषा हैं, ठीक उसी तरह जैसे कि बस प्रकार किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक स्पष्ट रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद सममित मोनोइडल श्रेणियों की श्रेणी के बीच फंक्शंस का निर्माण कर सकता है।[7]


ऐफिन प्रकार प्रणाली

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

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

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

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

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

यह भी देखें

संदर्भ

  1. ↑ 1.0 1.1 1.2 1.3 Walker, David (2002). "Substructural Type Systems". In Pierce, Benjamin C. (ed.). प्रकार और प्रोग्रामिंग भाषाओं में उन्नत विषय (PDF). MIT Press. pp. 3–43. ISBN 0-262-16228-8.
  2. ↑ Bernardy, Jean-Philippe; Boespflug, Mathieu; Newton, Ryan R; Peyton Jones, Simon; Spiwack, Arnaud (2017). "Linear Haskell: practical linearity in a higher-order polymorphic language". Proceedings of the ACM on Programming Languages. 2: 1–29. arXiv:1710.09756. doi:10.1145/3158093. S2CID 9019395.
  3. ↑ "std::unique_ptr - cppreference.com". en.cppreference.com. Retrieved 2023-05-14.
  4. ↑ "must_use | Diagnostics - The Rust Reference". doc.rust-lang.org. Retrieved 2023-05-14.
  5. ↑ Vít, Radek (2021-02-10). "Move semantics in C++ and Rust: The case for destructive moves". Medium (in English). Retrieved 2023-05-14.
  6. ↑ Baez, John C.; Stay, Mike (2010). "Physics, Topology, Logic and Computation: A Rosetta Stone". In Springer (ed.). भौतिकी के लिए नई संरचनाएं (PDF). pp. 95–174.
  7. ↑ Ambler, S. (1991). सममित मोनोइडल बंद श्रेणियों में प्रथम क्रम तर्क (PhD). U. of Edinburgh.
  8. ↑ "6.4.19. Linear types — Glasgow Haskell Compiler 9.7.20230513 User's Guide". ghc.gitlab.haskell.org. Retrieved 2023-05-14.
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=अवसंरचनात्मक_प्रकार_प्रणाली&oldid=199683’