F * .Net के लिए आश्रित प्रकारों के साथ एक नई भाषा है

परिचय

F * एक नई भाषा है, जो प्रोग्राम गुणों का प्रमाण बनाने के लिए Microsoft रिसर्च के आंतों में विकसित प्रकारों के साथ है। F * .Net बाइटकोड में संकलित करता है और F # सहित अन्य भाषाओं के साथ पारदर्शी रूप से एकीकृत करता है, जिसके आधार पर इसे बनाया गया है। आप ब्राउज़र में एफ * की कोशिश कर सकते हैं या कंपाइलर और संबंधित उदाहरणों के अल्फा संस्करण को डाउनलोड कर सकते हैं। Coq प्रणाली में औपचारिककरण F * सभी के लिए उपलब्ध है।


तो, नई भाषा की मुख्य विशेषताएं:

• स्व-प्रमाणन: F * tymphekher एफ * का उपयोग करके सत्यापित। इसके बारे में यहाँ और पढ़ें।
• वर्तमान में, जावास्क्रिप्ट फ्रंट-एंड वेब अनुप्रयोगों के निर्माण के लिए वास्तविक वास्तविक भाषा बन गई है। कई आधुनिक भाषाएं जावास्क्रिप्ट में संकलित हो सकती हैं। Microsoft रिसर्च इंजीनियरों ने एक कंपाइलर बनाया, जो जावास्क्रिप्ट में F * के काफी बड़े सब्मिट को संकलित करने की क्षमता रखता है। इसका मतलब है कि प्रोग्रामर वेब पेज पर एफ * में अपने कार्यक्रम को तैनात कर सकता है और गारंटी ले सकता है कि उसका कोड सही तरीके से काम करता है। विवरण यहाँ पढ़ा जा सकता है ।
• एक बोली "मोनाडिक एफ *" है , जो दीजकस्ट्रा मोनड का उपयोग करके एक नई सत्यापन पद्धति लागू करता है।

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



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

विभिन्न कार्यात्मक प्रोग्रामिंग भाषा विभिन्न प्रकार की प्रणालियों का समर्थन करती हैं जो लैम्बडा क्यूब में प्रदर्शित होती हैं। Λp Co Coq और Agda द्वारा समर्थित सबसे उन्नत टाइपिंग सिस्टम है।

लेकिन हमारी भेड़ों के पास वापस जाएँ और भाषा F * का संक्षिप्त विवरण देने की कोशिश करें।

यूरोप भर में सरपट

एफ * पर कार्यक्रम मॉड्यूल से मिलकर बनता है। प्रत्येक मॉड्यूल को मॉड्यूल कीवर्ड का उपयोग करके घोषित किया जाता है, जो मॉड्यूल के नाम को निर्दिष्ट करता है। एक उदाहरण:

 मॉड्यूल हैलोवर्ल्ड
 चलो _ = प्रिंट करें "हैलो वर्ल्ड!"

मॉड्यूल के अंत में फॉर्म लेट _ = e का एक कंस्ट्रक्टर इसके मुख्य कार्य को परिभाषित करता है।

F * प्रकार के प्रोग्राम गुणों का वर्णन करने के लिए उपयोग किया जाता है। उदाहरण के लिए, टाइप 0 की अभिव्यक्ति एक इंट से मेल खा सकती है। प्रिम्स मॉड्यूल (हास्केल प्रस्ताव का एक एनालॉग) कई बुनियादी प्रकारों को परिभाषित करता है, जैसे इकाई, इंट, स्ट्रिंग, आदि। निम्न उदाहरण अभिव्यक्ति के प्रकार को निर्दिष्ट करने के कई तरीके दिखाता है:

 चलो यू = () (<: यूनिट)
 चलो z = (0 <: int)
 Let z ': int = 1 - 1 
 Let z '' = (1 - 1 <: int)
 आज्ञा देना: स्ट्रिंग = "हैलो"

प्रिम्स मॉड्यूल कुछ उपयोगी डेटा प्रकारों को परिभाषित करता है, जैसे बहुरूपी सूची:

 सूची प्रकार 'a =
   |  निल: सूची 'ए
   |  विपक्ष: 'ए -> सूची' ए -> सूची 'ए

सामान्य तौर पर, एफ * में प्रोग्रामिंग कोक की तरह है - एक प्रोग्रामर एक प्रकार की एक प्रेरक परिभाषा दे सकता है और इन प्रकारों पर कार्यों को परिभाषित कर सकता है। आइए कुछ उपयोगी लिखने की कोशिश करें:

 let खाली_सूची = नील
 चलो खाली_सूची_सुगार = []

 चलो विपक्ष = विपक्ष 1 निल
 चलो cons_sugar = 1 :: []

 सूची_3 = विपक्ष 0 (विपक्ष 1 (विपक्ष 2 निल))
 let_3_sugar = [0; 1; 2]

 आज्ञा देना लंबाई = कार्य 
   |  [] -> ०
   |  _ :: tl -> 1 + (लंबाई tl)

 rec nth n = कार्य करते हैं 
   |  [] -> विफल "पर्याप्त तत्व नहीं"
   |  HD :: tl -> यदि n = 0 है तो hd nth (n - 1) tl

फिर से, सिंथेटिक चीनी को पेश करने के लिए Coq और इसकी अधिसूचनाओं के साथ स्पष्ट समानताएं हैं।

जिस प्रकार प्रकार भावों के गुणों का वर्णन करते हैं, उसी प्रकार के गुणों का वर्णन करने के लिए F * तरह का उपयोग करता है। अधिकांश प्रोग्रामिंग भाषाओं में, सॉर्ट निहित हैं। एक नियम के रूप में, केवल एक प्रकार की विविधता है - * (उच्चारण "स्टार")। बुनियादी डेटा प्रकार, जैसे इंट या स्ट्रिंग, प्रकार * के होते हैं। एफ * में, टाइप किस्में अधिक स्पष्ट हैं - आपके पास एक से अधिक आधार विविधता होनी चाहिए। इसलिए, प्राइमरी मॉड्यूल मूल प्रकार से संबंधित विविधता को निर्धारित करता है एस।

 प्रकार इकाई: एस
 प्रकार int: S
 प्रकार स्ट्रिंग: एस

यदि विविधता स्पष्ट रूप से निर्दिष्ट नहीं है और उपयोग के संदर्भ के अनुसार टाइपकर्ता द्वारा नहीं काटा जा सकता है, तो यह प्रकार स्वचालित रूप से विविधता एस प्राप्त करता है।

अधिक स्पष्ट रूप से, सूची प्रकार इस प्रकार निर्दिष्ट किया जा सकता है:

 प्रकार सूची: S => S =
    |  निल: 'ए: एस -> सूची' ए
    |  विपक्ष: 'ए: एस ->' ए -> सूची 'ए -> सूची' ए

यहां हम दो निर्माणकर्ताओं के साथ एक नई सूची प्रकार परिभाषित करते हैं। निल कंस्ट्रक्टर एकल तर्क लेता है - टाइप 'ए' टाइप एस।

प्रारंभिक परिणाम

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