पैरामीट्रिक बहुरूपता

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

पैरामीट्रिक बहुरूपता की तुलना तदर्थ बहुरूपता से की जा सकती है। पैरामीट्रिक रूप से बहुरूपी परिभाषाएँ 'एकसमान' हैं: वे जिस प्रकार के तात्कालिक हैं, उसकी परवाह किए बिना समान रूप से व्यवहार करते हैं। इसके विपरीत, तदर्थ बहुरूपी परिभाषाओं को प्रत्येक प्रकार के लिए अलग परिभाषा दी जाती है। इस प्रकार, तदर्थ बहुरूपता आम तौर पर केवल सीमित संख्या में ऐसे विशिष्ट प्रकारों का समर्थन कर सकता है, क्योंकि प्रत्येक प्रकार के लिए अलग कार्यान्वयन प्रदान किया जाना है।

मूल परिभाषा

उन कार्यों को लिखना संभव है जो उनके तर्कों के प्रकारों पर निर्भर नहीं होते हैं। उदाहरण के लिए, पहचान समारोह ${\mathsf {id}}(x)=x$ बस अपना तर्क अपरिवर्तित लौटाता है। यह स्वाभाविक रूप से संभावित प्रकार के परिवार को जन्म देता है, जैसे ${\mathsf {Int}}\to {\mathsf {Int}}$, ${\mathsf {Bool}}\to {\mathsf {Bool}}$, ${\mathsf {String}}\to {\mathsf {String}}$, और इसी तरह। पैरामीट्रिक बहुरूपता अनुमति देता है ${\mathsf {id}}$ सार्वभौमिक परिमाणीकरण प्रकार चर पेश करके एकल, सबसे सामान्य एकीकृत प्रकार दिया जाना:

${\mathsf {id}}:\forall \alpha .\alpha \to \alpha$

इसके बाद किसी भी ठोस प्रकार को प्रतिस्थापित करके बहुरूपी परिभाषा को तत्काल किया जा सकता है $\alpha$, संभावित प्रकार के पूरे परिवार की उपज। पहचान कार्य विशेष रूप से चरम उदाहरण है, लेकिन कई अन्य कार्य भी पैरामीट्रिक बहुरूपता से लाभान्वित होते हैं। उदाहरण के लिए, ए ${\mathsf {append}}$ फ़ंक्शन जो दो लिंक की गई सूची को जोड़ता है, सूची के तत्वों का निरीक्षण नहीं करता है, केवल सूची संरचना ही। इसलिए, ${\mathsf {append}}$ प्रकार का समान परिवार दिया जा सकता है, जैसे $(([{\mathsf {Int}}],[{\mathsf {Int}}])\to [{\mathsf {Int}}])$, $(([{\mathsf {Bool}}],[{\mathsf {Bool}}])\to [{\mathsf {Bool}}])$, और इसी तरह, कहाँ $[T]$ प्रकार के तत्वों की सूची को दर्शाता है $T$. इसलिए सबसे सामान्य प्रकार है

${\mathsf {append}}:\forall \alpha .([\alpha ],[\alpha ])\to [\alpha ]$

जिसे परिवार में किसी भी प्रकार से तत्काल किया जा सकता है।

Parametrically बहुरूपी कार्य जैसे ${\mathsf {id}}$ और ${\mathsf {append}}$ कहा जाता है कि मनमानी प्रकार पर पैरामिट्रीकृत किया जाता है $\alpha$. दोनों ${\mathsf {id}}$ और ${\mathsf {append}}$ ही प्रकार पर परिचालित किया जाता है, लेकिन कार्यों को मनमाने ढंग से कई प्रकारों पर परिचालित किया जा सकता है। उदाहरण के लिए, द ${\mathsf {fst}}$ और ${\mathsf {snd}}$ उत्पाद प्रकार के पहले और दूसरे तत्वों को क्रमशः लौटाने वाले कार्यों को निम्न प्रकार दिया जा सकता है:

${\begin{aligned}{\mathsf {fst}}&:\forall \alpha .\forall \beta .(\alpha ,\beta )\to \alpha \\{\mathsf {snd}}&:\forall \alpha .\forall \beta .(\alpha ,\beta )\to \beta \end{aligned}}$

अभिव्यक्ति में ${\mathsf {fst}}((3,{\mathsf {true}}))$, $\alpha$ पर प्रवर्तित किया जाता है ${\mathsf {Int}}$ और $\beta$ पर प्रवर्तित किया जाता है ${\mathsf {Bool}}$ को कॉल में ${\mathsf {fst}}$, तो समग्र अभिव्यक्ति का प्रकार है ${\mathsf {Int}}$.

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

इतिहास

पैरामीट्रिक बहुरूपता को पहली बार 1975 में एमएल प्रोग्रामिंग भाषा में प्रोग्रामिंग भाषाओं के लिए पेश किया गया था। आज यह मानक एमएल, OCaml, F Sharp (प्रोग्रामिंग लैंग्वेज)|F#, Ada (प्रोग्रामिंग लैंग्वेज), हास्केल (प्रोग्रामिंग भाषा), मरकरी (प्रोग्रामिंग लैंग्वेज), विजुअल प्रोलॉग, स्काला (प्रोग्रामिंग भाषा), जूलिया (प्रोग्रामिंग लैंग्वेज) में मौजूद है। , पायथन (प्रोग्रामिंग भाषा), टाइपप्रति, सी ++ और अन्य। जावा (प्रोग्रामिंग भाषा), सी शार्प (प्रोग्रामिंग लैंग्वेज) | सी #, विजुअल बेसिक .NET और वस्तु पास्कल में से प्रत्येक ने पैरामीट्रिक बहुरूपता के लिए जेनरिक पेश किए हैं। प्रकार के बहुरूपता के कुछ कार्यान्वयन सतही रूप से पैरामीट्रिक बहुरूपता के समान हैं, जबकि तदर्थ पहलुओं को भी प्रस्तुत करते हैं। उदाहरण C++ टेम्पलेट विशेषज्ञता है।

विधेयता, अभेद्यता, और उच्च-श्रेणी बहुरूपता

रैंक -1 (विधेयात्मक) बहुरूपता

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

भविष्यवाणी का परिणाम यह है कि सभी प्रकारों को ऐसे रूप में लिखा जा सकता है जो सभी परिमाणकों को सबसे बाहरी (प्रेनेक्स) स्थिति में रखता है। उदाहरण के लिए, पर विचार करें ${\mathsf {append}}$ ऊपर वर्णित कार्य, जिसमें निम्न प्रकार हैं:

${\mathsf {append}}:\forall \alpha .([\alpha ],[\alpha ])\to [\alpha ]$

इस फ़ंक्शन को सूचियों की जोड़ी पर लागू करने के लिए, ठोस प्रकार $T$ चर के लिए प्रतिस्थापित किया जाना चाहिए $\alpha$ ऐसा है कि परिणामी फ़ंक्शन प्रकार तर्कों के प्रकार के अनुरूप है। अप्रतिबंधित प्रणाली में, $T$ किसी भी प्रकार का हो सकता है, जिसमें प्रकार भी शामिल है जो स्वयं बहुरूपी है; इस प्रकार ${\mathsf {append}}$ किसी भी प्रकार के तत्वों के साथ सूचियों के जोड़े पर लागू किया जा सकता है - यहां तक ​​​​कि बहुरूपी कार्यों की सूचियों पर भी ${\mathsf {append}}$ अपने आप। भाषा एमएल में बहुरूपता विधेय है। ऐसा इसलिए है क्योंकि भविष्यवाणी, अन्य प्रतिबंधों के साथ, प्रकार प्रणाली को इतना सरल बनाती है कि पूर्ण प्रकार का अनुमान हमेशा संभव होता है।

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

उच्च-रैंक बहुरूपता

कुछ प्रकार के सिस्टम इम्प्रिडिकेटिव फंक्शन टाइप कंस्ट्रक्टर का समर्थन करते हैं, भले ही अन्य प्रकार के कंस्ट्रक्टर प्रेडिक्टिव रहते हैं। उदाहरण के लिए, प्रकार $(\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T$ ऐसी प्रणाली में अनुमति है जो उच्च-श्रेणी के बहुरूपता का समर्थन करती है, भले ही $[\forall \alpha .\alpha \rightarrow \alpha ]$ नहीं हो सकता। प्रकार को रैंक k का कहा जाता है (कुछ निश्चित पूर्णांक k के लिए) यदि इसकी जड़ से a तक कोई रास्ता नहीं है $\forall$ क्वांटिफायर k या अधिक तीरों के बाईं ओर जाता है, जब पेड़ के रूप में टाइप किया जाता है। प्रकार की प्रणाली को रैंक-के बहुरूपता का समर्थन करने के लिए कहा जाता है यदि यह रैंक के साथ के से कम या उसके बराबर के प्रकारों को स्वीकार करता है। उदाहरण के लिए, प्रकार की प्रणाली जो रैंक -2 बहुरूपता का समर्थन करती है, अनुमति देगी $(\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T$ लेकिन नहीं $((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T$. प्रकार की प्रणाली जो मनमाना रैंक के प्रकारों को स्वीकार करती है, उसे रैंक-एन बहुरूपी कहा जाता है।

रैंक-2 बहुरूपता के लिए प्रकार अनुमान निर्णायक है, लेकिन रैंक-3 और उससे ऊपर के लिए, यह नहीं है।

प्रतिकूल बहुरूपता

इम्प्रिडिकेटिव पोलिमोर्फिज्म (जिसे प्रथम श्रेणी का पॉलीमॉर्फिज्म भी कहा जाता है) पैरामीट्रिक पॉलीमॉर्फिज्म का सबसे शक्तिशाली रूप है। औपचारिक तर्क में, परिभाषा को अप्रतिबंधात्मकता कहा जाता है यदि यह स्व-संदर्भित है; टाइप थ्योरी में, यह प्रकार के क्वांटिफायर के डोमेन में होने की क्षमता को संदर्भित करता है। यह पॉलिमॉर्फिक प्रकारों सहित किसी भी प्रकार के चर के किसी भी प्रकार के इन्स्टेन्शियशन की अनुमति देता है। पूर्ण प्रतिबाधा का समर्थन करने वाली प्रणाली का उदाहरण सिस्टम एफ है, जो तत्काल करने की अनुमति देता है $\forall \alpha .\alpha \to \alpha$ किसी भी प्रकार से, स्वयं सहित।

टाइप थ्योरी में, सबसे अधिक बार अध्ययन किए जाने वाले इम्प्रेडिकेटिव टाइप लैम्ब्डा कैलकुलस | टाइप किए गए λ-कैलकुली लैम्ब्डा घन, विशेष रूप से सिस्टम एफ पर आधारित होते हैं।

परिबद्ध पैरामीट्रिक बहुरूपता

Main article: Bounded quantification

1985 में, लुका कार्डेली और पीटर वेगनर ने प्रकार के मापदंडों पर सीमा की अनुमति देने के लाभों को पहचाना। कई परिचालनों के लिए डेटा प्रकारों के कुछ ज्ञान की आवश्यकता होती है, लेकिन अन्यथा पैरामीट्रिक रूप से कार्य कर सकते हैं। उदाहरण के लिए, यह जाँचने के लिए कि क्या कोई वस्तु किसी सूची में शामिल है, हमें समानता के लिए वस्तुओं की तुलना करने की आवश्यकता है। मानक एमएल में, फॉर्म के टाइप पैरामीटर a प्रतिबंधित हैं ताकि समानता ऑपरेशन उपलब्ध हो, इस प्रकार फ़ंक्शन में a × a list → bool और a केवल परिभाषित प्रकार का प्रकार हो सकता है समानता। हास्केल (प्रोग्रामिंग लैंग्वेज) में, वर्ग टाइप करें से संबंधित प्रकारों की आवश्यकता के द्वारा बाउंडिंग हासिल की जाती है; इस प्रकार ही फ़ंक्शन का प्रकार होता है ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ हास्केल में। पैरामीट्रिक बहुरूपता का समर्थन करने वाली अधिकांश वस्तु-उन्मुख प्रोग्रामिंग भाषाओं में, मापदंडों को किसी दिए गए प्रकार के उपप्रकारों के लिए विवश किया जा सकता है (उपप्रकार बहुरूपता और सामान्य प्रोग्रामिंग पर लेख देखें)।

यह भी देखें

• पैरामीट्रिकिटी
• बहुरूपी पुनरावर्तन
• टाइप क्लास # हायर-किंडेड पॉलीमोर्फिज्म
• विशेषता (कंप्यूटर प्रोग्रामिंग)

संदर्भ

• Hindley, J. Roger (1969), "The principal type scheme of an object in combinatory logic", Transactions of the American Mathematical Society, 146: 29–60, doi:10.2307/1995158, JSTOR 1995158, MR 0253905.
• Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics (in français). Vol. 63. Amsterdam. pp. 63–92. doi:10.1016/S0049-237X(08)70843-7. ISBN 9780720422597.
• Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (Ph.D. thesis) (in français), Université Paris 7.
• Reynolds, John C. (1974), "Towards a Theory of Type Structure", Colloque Sur la Programmation, Lecture Notes in Computer Science, Paris, 19: 408–425, doi:10.1007/3-540-06859-7_148, ISBN 978-3-540-06859-4.
• Milner, Robin (1978). "A Theory of Type Polymorphism in Programming" (PDF). Journal of Computer and System Sciences. 17 (3): 348–375. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.
• Cardelli, Luca; Wegner, Peter (December 1985). "On Understanding Types, Data Abstraction, and Polymorphism" (PDF). ACM Computing Surveys. 17 (4): 471–523. CiteSeerX 10.1.1.117.695. doi:10.1145/6041.6042. ISSN 0360-0300. S2CID 2921816.
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.