अवसंरचनात्मक प्रकार प्रणाली: Difference between revisions
No edit summary |
No edit summary |
||
| Line 2: | Line 2: | ||
अवसंरचनात्मक [[ प्रकार प्रणाली |प्रकार प्रणाली]] [[ अवसंरचनात्मक तर्क |अवसंरचनात्मक लॉजिक्स]] अनुरूप प्रकार प्रणाली का वर्ग है जहां एक या अधिक संरचनात्मक नियम अनुपस्थित हैं या केवल नियंत्रित परिस्थितियों में ही अनुमति दी जाती है। ऐसे प्रणाली स्थिती में होने वाले परिवर्तनों पर दृष्टि रखकर और अमान्य स्थितियों को रोककर प्रणाली संसाधनों जैसे फ़ाइलों, लॉक और मेमोरी तक पहुंच को बाधित करने के लिए उपयोगी होते हैं।।<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}} | ||
== विभिन्न अवसंरचनात्मक प्रकार की प्रणालियाँ == | == विभिन्न अवसंरचनात्मक प्रकार की प्रणालियाँ == | ||
| Line 68: | Line 68: | ||
रेखीय प्रकार की प्रणालियाँ [[बंद मोनोइडल श्रेणी]] की [[आंतरिक भाषा]] हैं, ठीक उसी तरह जैसे कि बस प्रकार किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक स्पष्ट रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद सममित मोनोइडल श्रेणियों की श्रेणी के बीच फंक्शंस का निर्माण कर सकता है।<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> | रेखीय प्रकार की प्रणालियाँ [[बंद मोनोइडल श्रेणी]] की [[आंतरिक भाषा]] हैं, ठीक उसी तरह जैसे कि बस प्रकार किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक स्पष्ट रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद सममित मोनोइडल श्रेणियों की श्रेणी के बीच फंक्शंस का निर्माण कर सकता है।<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> | ||
'''<br />लियाँ [[बंद मोनोइडल श्रेणी]] की [[आंतरिक भाषा]] हैं, ठीक उसी तरह जैसे कि बस प्रकार किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक स्पष्ट रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद''' | |||
=== ऐफिन प्रकार प्रणाली === | |||
=== ऐफिन प्रकार प्रणाली === | |||
ऐफिन प्रकार रैखिक प्रकारों का संस्करण है जो [[affine तर्क|ऐफिन तर्क]] के अनुरूप संसाधन को त्यागने (अथार्त उपयोग नहीं करने) की अनुमति देता है। ऐफिन संसाधन का अधिकतम बार उपयोग किया जा सकता है, जबकि रैखिक संसाधन का उपयोग ठीक बार किया जाना चाहिए। | ऐफिन प्रकार रैखिक प्रकारों का संस्करण है जो [[affine तर्क|ऐफिन तर्क]] के अनुरूप संसाधन को त्यागने (अथार्त उपयोग नहीं करने) की अनुमति देता है। ऐफिन संसाधन का अधिकतम बार उपयोग किया जा सकता है, जबकि रैखिक संसाधन का उपयोग ठीक बार किया जाना चाहिए। | ||
Revision as of 11:47, 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]
लियाँ बंद मोनोइडल श्रेणी की आंतरिक भाषा हैं, ठीक उसी तरह जैसे कि बस प्रकार किया हुआ लैम्ब्डा कैलकुलस कार्टेशियन बंद श्रेणियों की भाषा है। अधिक स्पष्ट रूप से, कोई रैखिक प्रकार की प्रणालियों की श्रेणी और बंद
ऐफिन प्रकार प्रणाली
ऐफिन प्रकार रैखिक प्रकारों का संस्करण है जो ऐफिन तर्क के अनुरूप संसाधन को त्यागने (अथार्त उपयोग नहीं करने) की अनुमति देता है। ऐफिन संसाधन का अधिकतम बार उपयोग किया जा सकता है, जबकि रैखिक संसाधन का उपयोग ठीक बार किया जाना चाहिए।
प्रासंगिक प्रकार प्रणाली
प्रासंगिक प्रकार प्रासंगिक तर्क से मेल खाते हैं जो विनिमय और संकुचन की अनुमति देता है, किंतु अशक्त नहीं होता है, जो कम से कम बार उपयोग किए जाने वाले प्रत्येक चर का अनुवाद करता है।
प्रोग्रामिंग लैंग्वेज
निम्नलिखित प्रोग्रामिंग भाषाएं रैखिक या एफ़िन प्रकारों का समर्थन करती हैं:
- सी ++
- एटीएस (प्रोग्रामिंग भाषा)
- स्वच्छ (प्रोग्रामिंग भाषा)
- इदरीस (प्रोग्रामिंग भाषा)
- पारा (प्रोग्रामिंग भाषा)
- एफ * (प्रोग्रामिंग भाषा) | एफ *
- LinearML
- Alms
- ग्लासगो हास्केल कंपाइलर (जीएचसी) 9.0.1 या इसके बाद के संस्करण के साथ हास्केल[8]
- Granule
- रस्ट (प्रोग्रामिंग भाषा)
- निम (प्रोग्रामिंग भाषा)
यह भी देखें
- प्रभाव प्रणाली
- रैखिक तर्क
- एफ़िन तर्क
संदर्भ
- ↑ 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.
- ↑ 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.
- ↑ "std::unique_ptr - cppreference.com". en.cppreference.com. Retrieved 2023-05-14.
- ↑ "must_use | Diagnostics - The Rust Reference". doc.rust-lang.org. Retrieved 2023-05-14.
- ↑ Vít, Radek (2021-02-10). "Move semantics in C++ and Rust: The case for destructive moves". Medium (in English). Retrieved 2023-05-14.
- ↑ Baez, John C.; Stay, Mike (2010). "Physics, Topology, Logic and Computation: A Rosetta Stone". In Springer (ed.). भौतिकी के लिए नई संरचनाएं (PDF). pp. 95–174.
- ↑ Ambler, S. (1991). सममित मोनोइडल बंद श्रेणियों में प्रथम क्रम तर्क (PhD). U. of Edinburgh.
- ↑ "6.4.19. Linear types — Glasgow Haskell Compiler 9.7.20230513 User's Guide". ghc.gitlab.haskell.org. Retrieved 2023-05-14.
