निर्भर प्रकार - प्रोग्रामिंग भाषाओं का भविष्य

सभी को नमस्कार!

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

कभी-कभी ऐसा लगता है मानो प्रोग्रामिंग लैंग्वेज 60 के दशक से ज्यादा नहीं बदली हैं। जब वे मुझे इस बारे में बताते हैं, तो मुझे अक्सर याद आता है कि अब हमारे पास कितने शांत उपकरण और क्षमताएं हैं, और वे हमारे जीवन को कैसे सरल बनाते हैं। ऑफहैंड: ये एकीकृत डिबगर्स, और यूनिट टेस्ट, और स्टैटिक एनालाइज़र, और कूल आईडीई, साथ ही टाइप किए गए एरे और बहुत कुछ हैं। भाषाओं का विकास एक लंबी और प्रगतिशील प्रक्रिया है, और ऐसी कोई "सिल्वर बुलेट" नहीं हैं जिसके साथ भाषाओं का विकास एक बार और सभी के लिए बदल जाएगा।

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

प्रकारों की दुनिया

टाइपिंग उन चीजों में से एक है जो हमारी सोच से इतनी अविभाज्य हैं कि हम शायद ही इस प्रकार की अवधारणा के बारे में सोचते हैं? 1 int क्यों है, लेकिन यदि आप इस मूल्य को उद्धरण चिह्नों में रखते हैं - और यह एक string में बदल जाता है? संक्षेप में एक "प्रकार" क्या है? जैसा कि प्रोग्रामिंग में अक्सर होता है, उत्तर प्रश्न के शब्दों पर निर्भर करता है।

प्रकार विविध हैं। कुछ प्रकार की प्रणालियों में, प्रकार और मूल्यों के बीच बहुत स्पष्ट सीमाएं हैं। तो, 3, 2, और 1 integer मान हैं, लेकिन integer मान नहीं है। यह निर्माण भाषा में "एम्बेडेड" है और मूल रूप से अर्थ से अलग है। लेकिन, वास्तव में, ऐसा अंतर आवश्यक नहीं है और केवल हमें सीमित कर सकता है।

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

 if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") } 

हालाँकि, जब आप User प्रकार के साथ ऐसा करने का प्रयास करते हैं, तो आप केवल प्रकार के नामों और संभवतः संपत्ति के नामों की तुलना कर सकते हैं। चूंकि यह एक प्रकार है, उदाहरण के लिए, आप इसके गुणों के मूल्यों की जांच नहीं कर सकते।

 if typeof(user) == User { print("Well, it's a user. That's all I know") } 

यदि उपयोगकर्ताओं की केवल गैर-रिक्त सूची प्राप्त करने में सक्षम कोई फ़ंक्शन होता तो यह कितना अच्छा होता? या एक फ़ंक्शन जो ईमेल पते को केवल तभी स्वीकार करेगा जब वह सही प्रारूप में दर्ज हो? इन उद्देश्यों के लिए, आपको "गैर-रिक्त सरणी" या "ईमेल पता" प्रकार की आवश्यकता होगी। इस मामले में, यह एक मूल्य-निर्भर प्रकार है, अर्थात्। निर्भर प्रकार के बारे में। मुख्यधारा की भाषाओं में, यह संभव नहीं है।

ताकि प्रकार का उपयोग किया जा सके, संकलक को उनकी जांच करनी चाहिए। यदि आप दावा करते हैं कि चर में पूर्णांक है, तो बेहतर होगा कि इसमें कोई string न हो, अन्यथा कंपाइलर शपथ लेगा। सिद्धांत रूप में, यह अच्छा है, क्योंकि यह हमें लुभाने की अनुमति नहीं देता है। चेकिंग प्रकार काफी सरल है: यदि कोई फ़ंक्शन integer देता है, और हम इसमें "Marin" वापस करने का प्रयास करते हैं, तो यह एक त्रुटि है।

हालांकि, निर्भर प्रकारों के साथ, चीजें अधिक जटिल हो जाती हैं। समस्या यह है जब वास्तव में संकलक प्रकारों की जांच करता है। वह यह कैसे सुनिश्चित कर सकता है कि सरणी में बिल्कुल तीन मान हैं, यदि प्रोग्राम अभी भी नहीं चल रहा है? यह कैसे सुनिश्चित करें कि एक पूर्णांक 3 से अधिक है, अगर इसे अभी भी सौंपा नहीं गया है? इस के लिए जादू है ... या, दूसरे शब्दों में, गणित । यदि यह गणितीय रूप से साबित हो सकता है कि संख्याओं का सेट हमेशा 3 से अधिक है, तो संकलक इसे सत्यापित कर सकता है।

स्टूडियो में मैथ्स!

गणितीय प्रेरण का उपयोग साक्ष्य बनाने के लिए किया जाता है। प्रेरण हमें बिना शर्त के एक बयान की सच्चाई की पुष्टि करने की अनुमति देता है। उदाहरण के लिए, हम यह साबित करना चाहते हैं कि निम्नलिखित गणितीय सूत्र किसी भी सकारात्मक संख्या के लिए है:

 1 + 2 + 3 + ... + x = x * (x + 1) / 2 

संभावित x की अनंत संख्या है, इसलिए हमें सभी नंबरों को मैन्युअल रूप से जांचने में बहुत लंबा समय लगेगा। सौभाग्य से, यह आवश्यक नहीं है। हमें सिर्फ दो चीजें साबित करने की जरूरत है:

1. यह कथन पहले दिन के लिए मनाया जाता है। (आमतौर पर यह 0 या 1 है)
2. यदि यह कथन संख्या n लिए सही है, तो यह अगले संख्या n + 1 लिए सही होगा

चूंकि कथन पहली संख्या और सभी निम्नलिखित संख्याओं के लिए मनाया जाता है, इसलिए हम जानते हैं कि यह सभी संभव संख्याओं के लिए सही है।

यह साबित करना मुश्किल नहीं है:

 1 = 1 * (1 + 1) / 2 1 = 1 

अब हमें यह भी साबित करना है कि बयान अन्य सभी नंबरों के लिए है। ऐसा करने के लिए, मान लीजिए कि यह कुछ संख्या n के लिए काम करता है, और फिर सुनिश्चित करें कि यह n + 1 के लिए भी काम करता है।

यह मानते हुए कि निम्नलिखित अभिव्यक्ति सत्य है:

 1 + 2 + 3 + ... + n = n * (n + 1) / 2 

इसे n + 1 :

 (1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2 

इस प्रकार, हम उपरोक्त समानता के "(1 + 2 + 3 + ... + n)" प्रतिस्थापित कर सकते हैं:

 (n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2) 

और सरल करें

 (n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1) 

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

इस दृष्टिकोण की सुंदरता इस तथ्य में निहित है कि किसी भी गणितीय प्रमाण को कंप्यूटर प्रोग्राम के रूप में जारी किया जा सकता है - और यह वही है जो हमें चाहिए!

वापस प्रोग्रामिंग के लिए

इसलिए, हमने पाया कि कुछ चीजों को पहले साबित किया जा सकता है, और फिर विशिष्ट मूल्यों पर आगे बढ़ सकते हैं। एक प्रोग्रामिंग भाषा में ऐसा करने के लिए, आपको इन कथनों को कोड में व्यक्त करने के लिए एक तरीका चाहिए जो कि टाइप सिस्टम में ही लिखा जाएगा, यानी टाइप सिस्टम को सुधारना होगा।

एक उदाहरण पर विचार करें। यहां हमारे पास एक एपेंड फ़ंक्शन है जो दो सरणियों को लेता है और उन्हें जोड़ती है। एक नियम के रूप में, इस तरह के एक समारोह के हस्ताक्षर कुछ इस तरह दिखाई देंगे:

 append: (arr1: Array, arr2: Array) -> Array 

हालाँकि, केवल हस्ताक्षर को देखकर, हम सही कार्यान्वयन के बारे में सुनिश्चित नहीं हो सकते हैं। तथ्य यह है कि फ़ंक्शन एक सरणी लौटाता है इसका मतलब यह नहीं है कि उसने कुछ किया था। परिणाम की जांच करने का एक तरीका यह सुनिश्चित करना है कि परिणामी सरणी की लंबाई पैरामीटर सरणियों की लंबाई के योग के बराबर है।

 newArray = append([1], [2, 3]) assert(length(newArray) == 3) 

लेकिन इसे रन टाइम पर चेक क्यों करें यदि आप एक बाधा बना सकते हैं जो संकलन समय पर जाँच की जाएगी:

 append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2) 

हम घोषणा करते हैं कि append एक फ़ंक्शन है जो दो Array तर्क देता है और एक नया Array तर्क देता है, जिसे हमने newArray कहा जाता है। केवल इस बार हम एक चेतावनी जोड़ते हैं कि नए सरणी की लंबाई फ़ंक्शन के सभी तर्कों की लंबाई के बराबर होनी चाहिए। रनटाइम के दौरान हमारे पास जो स्टेटमेंट था वह कंपाइल टाइम में टाइप करने के लिए बदल जाता है।

उपरोक्त कोड प्रकारों की दुनिया को संदर्भित करता है, न कि मूल्यों को, अर्थात == चिन्ह लौटे प्रकार की length की तुलना को इंगित करता है, न कि इसके मूल्य को। काम करने के लिए इस तरह के तंत्र के लिए, लौटे प्रकार की लंबाई हमें वास्तविक संख्या के बारे में कुछ जानकारी देनी चाहिए।

इस तरह के तंत्र के संचालन को सुनिश्चित करने के लिए, आपको यह सुनिश्चित करने की आवश्यकता है कि प्रत्येक संख्या एक अलग प्रकार की है। एक प्रकार में केवल एक मान हो सकता है: 1. यही बात दो, तीन और अन्य सभी संख्याओं पर लागू होती है। स्वाभाविक रूप से, इस तरह के काम बहुत थका देने वाले होते हैं, लेकिन यह ऐसे काम के लिए है, जो हमारे पास प्रोग्रामिंग है। आप एक कंपाइलर लिख सकते हैं जो हमारे लिए ऐसा करेगा।

ऐसा करने के बाद, आप 1, 2, 3 और तत्वों की एक अलग संख्या वाले सरणियों के लिए अलग प्रकार बना सकते हैं। ArrayOfOne , ArrayOfTwo , आदि।

इस प्रकार, आप लंबाई फ़ंक्शन को परिभाषित कर सकते हैं, जो उपरोक्त सरणी प्रकारों में से एक लेगा और आश्रित प्रकार का One जो ArrayOfOne , Two ArrayOfTwo , आदि। प्रत्येक संख्या के लिए।

अब हमारे पास सरणी की किसी भी विशिष्ट लंबाई के लिए एक अलग प्रकार है, हम सत्यापित कर सकते हैं (संकलन के समय) कि दोनों सरणियाँ समान लंबाई की हैं। ऐसा करने के लिए, उनके प्रकारों की तुलना करें। और चूंकि प्रकार किसी अन्य के समान मूल्य हैं, इसलिए आप उन्हें संचालन असाइन कर सकते हैं। आप यह निर्दिष्ट करके दो विशिष्ट प्रकारों को जोड़ सकते हैं कि ArrayOfTwo के बराबर ArrayOfOne और ArrayOfTwo का ArrayOfThree ।

यह सभी जानकारी है कि संकलक को यह सुनिश्चित करने की आवश्यकता है कि आपके द्वारा लिखा गया कोड सही है।

मान लें कि हम ArrayOfThree प्रकार का एक चर बनाना चाहते हैं:

 result: ArrayOfThree = append([1], [2, 3]) 

कंपाइलर यह निर्धारित कर सकता है कि [1] का केवल एक मूल्य है, इसलिए आप ArrayOfOne टाइप कर सकते हैं। यह ArrayOfTwo [2, 3] को भी असाइन कर सकता है।

संकलक जानता है कि परिणाम का प्रकार पहले और दूसरे तर्क के प्रकारों के योग के बराबर होना चाहिए। वह यह भी जानता है कि ArrayOfOne + ArrayOfTwo, ArrayOfThree के बराबर है, अर्थात, वह जानता है कि पहचान के दाईं ओर की पूरी अभिव्यक्ति ArrayOfThree है। यह बाईं ओर की अभिव्यक्ति से मेल खाता है, और संकलक प्रसन्न है।

यदि हमने निम्नलिखित लिखा है:

 result: ArrayOfTwo = append([1], [2, 3]) 

तब कंपाइलर पूरी तरह से असंतुष्ट हो जाएगा, क्योंकि यह पता चल जाएगा कि प्रकार गलत है।

आश्रित टाइपिंग बहुत शांत है

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

निर्भर प्रकारों का उपयोग करना, आप लगभग कुछ भी व्यक्त कर सकते हैं। फैक्टरियल फ़ंक्शन केवल प्राकृतिक संख्याओं को स्वीकार करेगा, login फ़ंक्शन खाली लाइनों को स्वीकार नहीं करेगा, removeLast फ़ंक्शन केवल गैर-खाली सरणियों को स्वीकार करेगा। इसके अलावा, कार्यक्रम शुरू करने से पहले यह सब जाँच लिया जाता है।

रनटाइम चेक के साथ समस्या यह है कि यदि प्रोग्राम पहले से ही चल रहा है तो वे विफल हो जाते हैं। यह सामान्य है यदि प्रोग्राम केवल आपके द्वारा चलाया जाता है, लेकिन उपयोगकर्ता द्वारा नहीं। आश्रित प्रकार आपको इस तरह के चेक को स्तर के स्तर पर ले जाने की अनुमति देते हैं, इसलिए प्रोग्राम निष्पादन के दौरान इस तरह की विफलता असंभव हो जाती है।

मुझे लगता है कि निर्भर टाइपिंग मुख्यधारा की प्रोग्रामिंग भाषाओं का भविष्य है, और मैं इसके लिए इंतजार नहीं कर सकता!

→ इदरीस

→ F *

→ जावास्क्रिप्ट पर निर्भर प्रकार जोड़ना