प्रकार प्रणालियाँ
प्रकार प्रणालियाँ औपचारिक अनुशासन हैं जो प्रोग्राम अभिव्यक्तियों को उनके द्वारा परिकलित मानों के प्रकारों के आधार पर वर्गीकृत करती हैं, जिससे प्रोग्राम चलने से पहले ही त्रुटियों के व्यापक वर्गों को रोका जा सकता है।
Definition
एक प्रकार प्रणाली कुछ प्रोग्राम व्यवहारों की अनुपस्थिति को सिद्ध करने के लिए एक सुगम वाक्यात्मक विधि है, जो अभिव्यक्तियों को उनके द्वारा परिकलित मानों के प्रकारों के अनुसार वर्गीकृत करती है।
Scope
यह क्षेत्र प्रकार प्रणालियों के सिद्धांत और डिज़ाइन को शामिल करता है: स्थैतिक बनाम गतिशील टाइपिंग, पैरामीट्रिक और एड हॉक पॉलीमॉर्फिज्म, सबटाइपिंग, प्रकार अनुमान, और निर्भर और सबस्ट्रक्चरल प्रकार जैसी उन्नत प्रणालियाँ। यह प्रकार की सुदृढ़ता, करी-हावर्ड पत्राचार के माध्यम से प्रकारों और तर्क के बीच संबंध, और टाइपिंग अनुशासन कैसे गारंटी और निर्णयशीलता के विरुद्ध अभिव्यंजकता का व्यापार करते हैं, को संबोधित करता है।
Sub-topics
Core questions
- एक प्रकार प्रणाली क्या गारंटी प्रदान करती है, और प्रकार की सुदृढ़ता क्या है?
- पॉलीमॉर्फिज्म और सबटाइपिंग सुरक्षा का त्याग किए बिना अभिव्यंजकता को कैसे बढ़ाते हैं?
- क्या प्रकारों का स्वचालित रूप से अनुमान लगाया जा सकता है, और अनुमान कब निर्णायक होता है?
- पूर्ण विशिष्टताओं तक, प्रकार कितनी दूर तक समृद्ध प्रोग्राम गुणों को एन्कोड कर सकते हैं?
Key theories
- प्रगति और संरक्षण के माध्यम से प्रकार की सुदृढ़ता
- राइट और फेलेसेन का वाक्यात्मक दृष्टिकोण एक प्रकार प्रणाली को सुदृढ़ सिद्ध करता है, यह स्थापित करके कि अच्छी तरह से टाइप्ड प्रोग्राम अटकते नहीं हैं: मूल्यांकन के तहत प्रकार संरक्षित होते हैं और अच्छी तरह से टाइप्ड पद हमेशा प्रगति कर सकते हैं।
- पॉलीमॉर्फिज्म और अमूर्तन की टाइपोलॉजी
- कार्डेलि और वेगनर टाइपिंग अवधारणाओं के स्थान को व्यवस्थित करते हैं, एक एकीकृत ढांचे के भीतर पैरामीट्रिक और एड हॉक पॉलीमॉर्फिज्म, समावेशन (सबटाइपिंग), और डेटा अमूर्तन को अलग करते हैं।
- प्रोग्रामिंग-भाषा नींव के रूप में प्रकार सिद्धांत
- हार्पर एक समान स्थैतिक-और-गतिशील कार्यप्रणाली विकसित करते हैं जिसमें भाषा सुविधाओं को टाइपिंग और मूल्यांकन नियमों द्वारा परिभाषित किया जाता है, प्रकार सिद्धांत को भाषा डिज़ाइन के लिए आयोजन नींव के रूप में मानते हुए।
Clinical relevance
प्रकार प्रणालियाँ सबसे व्यापक रूप से तैनात औपचारिक विधियों में से हैं: वे संकलन समय पर त्रुटियों को पकड़ती हैं, इंटरफेस का दस्तावेजीकरण करती हैं, सुरक्षित रीफैक्टरिंग को सक्षम करती हैं, और संपादक टूलिंग को संचालित करती हैं। जेनेरिक्स, क्रमिक टाइपिंग और स्वामित्व प्रकार जैसी प्रगति सीधे मुख्यधारा की औद्योगिक भाषाओं में आ गई हैं।
History
टाइप्ड भाषाएँ अल्गोल और सरल टाइप्ड लैम्ब्डा कैलकुलस जैसे शुरुआती प्रणालियों के साथ उभरीं। मिलनर का पॉलीमॉर्फिक प्रकार अनुमान (1978) एमएल का आधार बना; गिरार्ड और रेनॉल्ड्स ने स्वतंत्र रूप से पैरामीट्रिक पॉलीमॉर्फिज्म के लिए सिस्टम एफ तैयार किया। कार्डेलि और वेगनर के 1985 के सर्वेक्षण ने इस क्षेत्र को व्यवस्थित किया, और प्रगति-और-संरक्षण विधि (1994) मानक सुदृढ़ता तकनीक बन गई जिसे पियर्स और हार्पर ने बाद में पाठ्यपुस्तकों में प्रतिष्ठित किया।
Debates
- स्थैतिक बनाम गतिशील टाइपिंग
- एक लंबे समय से चली आ रही बहस स्थैतिक टाइपिंग की प्रारंभिक त्रुटि का पता लगाने और दस्तावेजीकरण को गतिशील टाइपिंग के लचीलेपन और तीव्र पुनरावृति के मुकाबले तौलती है, जिसमें क्रमिक टाइपिंग को एक समाधान के रूप में पेश किया जाता है।
Key figures
- Benjamin Pierce
- Robert Harper
- Luca Cardelli
- Robin Milner
- Matthias Felleisen
Related topics
Seminal works
- pierce2002
- harper2016
- cardelli1985
- wright1994
Frequently asked questions
- एक प्रकार प्रणाली के सुदृढ़ होने का क्या अर्थ है?
- सुदृढ़ता का अर्थ है कि अच्छी तरह से टाइप्ड प्रोग्राम उन त्रुटियों को प्रदर्शित नहीं कर सकते जिन्हें प्रकार प्रणाली रोकने के लिए डिज़ाइन की गई है, आमतौर पर यह दर्शाकर सिद्ध किया जाता है कि मूल्यांकन के दौरान प्रकार संरक्षित होते हैं और अच्छी तरह से टाइप्ड प्रोग्राम कभी अटकते नहीं हैं।
- क्या गतिशील रूप से टाइप्ड भाषाओं में प्रकार प्रणालियाँ होती हैं?
- उनके पास प्रकार होते हैं और रनटाइम प्रकार की जाँच करते हैं, लेकिन उनमें एक स्थैतिक प्रकार प्रणाली की कमी होती है जो निष्पादन से पहले खराब-टाइप्ड प्रोग्राम को अस्वीकार करती है; प्रकार की त्रुटियाँ इसके बजाय रनटाइम दोषों के रूप में सामने आती हैं।