सेरोकेल में, हम न केवल वाणिज्यिक परियोजनाओं में लगे हुए हैं, बल्कि बेहतर के लिए दुनिया को बदलने का भी प्रयास करते हैं। उदाहरण के लिए, हम सभी हास्केलिस्ट - ग्लासगो हास्केल कंपाइलर (जीएचसी) के मुख्य उपकरण को बेहतर बनाने पर काम कर रहे हैं। हमने रिचर्ड एसेनबर्ग के काम के प्रभाव के तहत टाइप सिस्टम के विस्तार पर ध्यान केंद्रित किया, "हास्केल में निर्भर प्रकार: सिद्धांत और अभ्यास । "

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

मामलों की वर्तमान स्थिति

आश्रित प्रकार वे हैं जिन्हें मैं हास्केल में सबसे ज्यादा याद करता हूं। आइए चर्चा करें कि क्यों। कोड से हम चाहते हैं:

• प्रदर्शन, अर्थात्, निष्पादन की गति और कम मेमोरी खपत;
• स्थिरता और समझने में आसानी;
• इसे संकलित करने की विधि द्वारा शुद्धता की गारंटी।

मौजूदा प्रौद्योगिकियों के साथ, सभी तीन विशेषताओं को प्राप्त करना बहुत कम संभव है, लेकिन हास्केल पर निर्भर प्रकारों के लिए समर्थन के साथ, कार्य सरल है।

हास्केल मानक: एर्गोनॉमिक्स + प्रदर्शन

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

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

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

कचरा बीनने वालों के पास भाषाएं बची हैं, जिन्हें हम आगे उनकी प्रणाली के आधार पर दो श्रेणियों में विभाजित करेंगे।

गतिशील रूप से टाइप की गई (या बल्कि मोनोटाइप्ड ) भाषाएं, जैसे कि जावास्क्रिप्ट या क्लोजर, स्थैतिक विश्लेषण प्रदान नहीं करती हैं, और इसलिए कोड की शुद्धता में विश्वास का समान स्तर प्रदान नहीं कर सकती (और नहीं, परीक्षण प्रकारों को प्रतिस्थापित नहीं कर सकते हैं - आपको दोनों की आवश्यकता है) !)।

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

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

हास्केल लगभग एक सही भाषा की तरह लगता है जब तक आपको एहसास नहीं होता है कि यह एजडा जैसे प्रमेय प्रूफ साधनों की तुलना में स्थैतिक सत्यापन के मामले में अपनी पूरी क्षमता से दूर है।

जहां हास्केल प्रकार प्रणाली पर्याप्त शक्तिशाली नहीं है, उसके एक साधारण उदाहरण के रूप में, Prelude (या एक primitive पैकेज से एक सरणी अनुक्रमणिका) से सूची अनुक्रमणिका पर विचार करें:

 (!!) :: [a] -> Int -> a indexArray :: Array a -> Int -> a 

इन प्रकार के हस्ताक्षर में कुछ भी आवश्यकता को दर्शाता है कि सूचकांक गैर-नकारात्मक होना चाहिए और संग्रह की लंबाई से कम होना चाहिए। उच्च विश्वसनीयता आवश्यकताओं वाले सॉफ़्टवेयर के लिए यह अस्वीकार्य है।

एजडा: एर्गोनॉमिक्स + शुद्धता

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

प्रोग्रामर के लिए, हालांकि, प्रमेयों को साबित करने का साधन एक अविश्वसनीय प्रकार की प्रणाली (और संभवतः एक एकीकृत विकास वातावरण) के साथ गूढ़ प्रोग्रामिंग भाषा के लिए संकलक से इतना अलग नहीं है, और औसत दर्जे (या यहां तक ​​कि अनुपस्थित) बाकी सब कुछ। प्रमेय साबित करने का एक साधन, वास्तव में, प्रोग्रामिंग भाषाएं हैं, जिनमें से लेखकों ने अपना सारा समय एक टाइपिंग सिस्टम विकसित करने में बिताया और यह भूल गए कि कार्यक्रमों को अभी भी चलाने की आवश्यकता है।

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

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

यहाँ हास्केल ऑपरेटर (!!) समान एक लुकअप फंक्शन टाइप है:

 lookup : ∀ (xs : List A) → Fin (length xs) → A 

यहां पहला पैरामीटर टाइप List A , जो हास्केल में [a] मेल खाता है। हालाँकि, हम इसे शेष प्रकार के हस्ताक्षर के लिए संदर्भित करने के लिए नाम xs देते हैं। हास्केल में, हम केवल शब्द स्तर पर फ़ंक्शन के तर्कों तक पहुँच सकते हैं:

 (!!) :: [a] -> Int -> a --   xs  (!!) = \xs i -> ... --   xs  

लेकिन Agda में, हम इस xs मान को उस प्रकार के स्तर पर संदर्भित कर सकते हैं, जो हम दूसरे lookup पैरामीटर, Fin (length xs) । एक फ़ंक्शन जो प्रकार के स्तर पर अपने पैरामीटर को संदर्भित करता है, उसे एक निर्भर फ़ंक्शन कहा जाता है और यह निर्भर प्रकारों का एक उदाहरण है।

lookup में दूसरा पैरामीटर n ~ length xs लिए Fin n प्रकार का है। Fin n प्रकार का मान रेंज [0, n) में एक संख्या से मेल खाता है, इसलिए Fin (length xs) एक गैर-ऋणात्मक संख्या है जो इनपुट सूची की लंबाई से कम है। यह वही है जो हमें किसी सूची आइटम के वैध सूचकांक को प्रस्तुत करने की आवश्यकता है। मोटे तौर पर, lookup ["x","y","z"] 2 टाइप चेकिंग पास करेगा, लेकिन lookup ["x","y","z"] 42 फेल होगा।

जब यह एजडा कार्यक्रम चलाने की बात आती है, तो हम MAlonzo बैकएंड का उपयोग करके हास्केल में उन्हें संकलित कर सकते हैं। लेकिन उत्पन्न कोड का प्रदर्शन असंतोषजनक होगा। यह MAlonzo की गलती नहीं है: उसे कई unsafeCoerce सम्मिलित unsafeCoerce ताकि GHC कोड पहले से ही Agda द्वारा सत्यापित unsafeCoerce । लेकिन वही unsafeCoerce प्रदर्शन को कम करता है (इस लेख की चर्चा के बाद, यह पता चला है कि प्रदर्शन की समस्याएं अन्य कारणों से हो सकती हैं - लेखक का नोट) ।

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

एक्सटेंशन के साथ हास्केल: सुधार + प्रदर्शन

आश्रित प्रकार के साथ भाषाओं की स्थिर गारंटी के लिए, GHC ने एक लंबा सफर तय किया है। टाइप सिस्टम की अभिव्यक्ति को बढ़ाने के लिए इसमें एक्सटेंशन जोड़े गए थे। मैंने Haskell का उपयोग तब शुरू किया जब GHC 7.4 संकलक का नवीनतम संस्करण था। फिर भी, इसके पास उन्नत प्रकार-स्तरीय प्रोग्रामिंग के लिए मुख्य एक्सटेंशन थे: RankNTypes , GADTs , TypeFamilies , DataKinds और PolyKinds ।

फिर भी, हास्केल में अभी भी पूर्ण-निर्भर आश्रित प्रकार नहीं हैं: न तो आश्रित कार्य (Π-type) और न ही आश्रित जोड़े (dependent-types)। दूसरी ओर, कम से कम हमारे पास उनके लिए एन्कोडिंग है!

वर्तमान अभ्यास इस प्रकार हैं:

• निजी प्रकार के परिवारों के रूप में एन्कोड प्रकार के स्तर,
• असंतृप्त कार्यों को सक्षम करने के लिए क्रियाशीलता का उपयोग करें,
• एकल प्रकारों का उपयोग करके शब्दों और प्रकारों के बीच की खाई को पाटें

यह एक महत्वपूर्ण मात्रा में अनावश्यक कोड की ओर जाता है, लेकिन singletons लाइब्रेरी लाइब्रेरी टेम्पलेट हास्केल के माध्यम से अपनी पीढ़ी को स्वचालित करता है।

तो सबसे साहसी और निर्णायक अब हास्केल में निर्भर प्रकारों को कोड कर सकते हैं। प्रदर्शन के रूप में, यहाँ Agda पर संस्करण के समान lookup फ़ंक्शन का कार्यान्वयन है:

 {-# OPTIONS -Wall -Wno-unticked-promoted-constructors -Wno-missing-signatures #-} {-# LANGUAGE LambdaCase, DataKinds, PolyKinds, TypeFamilies, GADTs, ScopedTypeVariables, EmptyCase, UndecidableInstances, TypeSynonymInstances, FlexibleInstances, TypeApplications, TemplateHaskell #-} module ListLookup where import Data.Singletons.TH import Data.Singletons.Prelude singletons [d| data N = Z | SN len :: [a] -> N len [] = Z len (_:xs) = S (len xs) |] data Fin n where FZ :: Fin (S n) FS :: Fin n -> Fin (S n) lookupS :: SingKind a => SList (xs :: [a]) -> Fin (Len xs) -> Demote a lookupS SNil = \case{} lookupS (SCons x xs) = \case FZ -> fromSing x FS i' -> lookupS xs i' 

और यहाँ GHCi सत्र दिखा रहा है कि लुकअप वास्तव में ऐसे इंडेक्स को अस्वीकार करता है जो बहुत बड़े हैं:

 GHCi, version 8.6.2: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling ListLookup ( ListLookup.hs, interpreted ) Ok, one module loaded. *ListLookup> :set -XTypeApplications -XDataKinds *ListLookup> lookupS (sing @["x", "y", "z"]) FZ "x" *ListLookup> lookupS (sing @["x", "y", "z"]) (FS FZ) "y" *ListLookup> lookupS (sing @["x", "y", "z"]) (FS (FS FZ)) "z" *ListLookup> lookupS (sing @["x", "y", "z"]) (FS (FS (FS FZ))) <interactive>:5:34: error: • Couldn't match type ''S n0' with ''Z' Expected type: Fin (Len '["x", "y", "z"]) Actual type: Fin ('S ('S ('S ('S n0)))) • In the second argument of 'lookupS', namely '(FS (FS (FS FZ)))' In the expression: lookupS (sing @["x", "y", "z"]) (FS (FS (FS FZ))) In an equation for 'it': it = lookupS (sing @["x", "y", "z"]) (FS (FS (FS FZ))) 

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

इस विशेष मामले में, हम लंबाई-अनुक्रमित वैक्टर का उपयोग करके कम जटिलता के साथ एक ही परिणाम प्राप्त कर सकते हैं। हालांकि, Agda से प्रत्यक्ष कोड अनुवाद उन समस्याओं को बेहतर ढंग से प्रकट करता है जो आपको अन्य परिस्थितियों में होनी चाहिए।

यहाँ उनमें से कुछ हैं:

• टाइपिंग का संबंध a :: t और प्रपत्र t :: k का गंतव्य संबंध t :: k अलग हैं। 5 :: Integer शब्दों में सत्य है, लेकिन प्रकारों में नहीं। "hi" :: Symbol प्रकारों में सच है, लेकिन शब्दों में नहीं। यह विचारों और प्रकारों को मैप करने के लिए Demote टाइप Demote आवश्यकता है।
• मानक पुस्तकालय Int का उपयोग सूची सूचियों के प्रतिनिधित्व के रूप में करता है (और singletons ऊंचे परिभाषाओं में Nat का उपयोग करता है)। Int और Nat गैर-आगमनात्मक प्रकार हैं। प्राकृतिक संख्याओं की एकात्मक एन्कोडिंग की तुलना में अधिक कुशल होने के बावजूद, वे Fin या lookupS जैसे प्रेरक परिभाषाओं के साथ बहुत अच्छी तरह से काम नहीं करते हैं। इस वजह से, हम length को len रूप में फिर से परिभाषित करते हैं।
• हस्केल में कार्यों के प्रकारों के स्तर को बढ़ाने के लिए कोई अंतर्निहित तंत्र नहीं है। singletons उन्हें निजी प्रकार के परिवारों के रूप में एन्कोड करते हैं और प्रकार के परिवारों के आंशिक उपयोग की कमी को रोकने के लिए क्रियाशीलता को लागू करते हैं। यह एन्कोडिंग जटिल है। इसके अलावा, हमें एक टेम्प्लेट हास्केल उद्धरण में len परिभाषा len थी, ताकि singletons अपने प्रकार के स्तर के समकक्ष, Len उत्पन्न करें।
• कोई अंतर्निहित आश्रित कार्य नहीं हैं। शब्दों और प्रकारों के बीच अंतर को पाटने के लिए इकाई प्रकारों का उपयोग करना पड़ता है। सामान्य सूची के बजाय, हम SList को lookupS इनपुट में पास करते हैं। इसलिए, हमें एक ही बार में सूचियों की कई परिभाषाओं को ध्यान में रखना चाहिए। यह कार्यक्रम के निष्पादन के दौरान ओवरहेड की ओर भी जाता है। वे यूनिट प्रकारों ( toSing , fromSing ) के सामान्य मूल्यों और मूल्यों के बीच रूपांतरण के कारण उत्पन्न होते हैं और रूपांतरण प्रक्रिया ( SingKind प्रतिबंध) के हस्तांतरण के कारण।

असुविधा कम समस्या है। इससे भी बदतर, ये भाषा सुविधाएँ अविश्वसनीय हैं। उदाहरण के लिए, मैंने 2016 में समस्या # 12564 वापस की, और उसी वर्ष के # 12088 भी हैं। दोनों समस्याएं पाठ्यपुस्तकों के उदाहरणों (जैसे अनुक्रमण सूचियों) से अधिक उन्नत कार्यक्रमों के कार्यान्वयन में बाधा डालती हैं। ये जीएचसी कीड़े अभी भी तय नहीं हैं, और इसका कारण, मुझे ऐसा लगता है, डेवलपर्स के पास पर्याप्त समय नहीं है। जीएचसी पर सक्रिय रूप से काम करने वाले लोगों की संख्या आश्चर्यजनक रूप से बहुत कम है, इसलिए कुछ चीजें आसपास नहीं मिलती हैं।

सारांश

मैंने पहले उल्लेख किया था कि हम कोड से सभी तीन गुण चाहते हैं, इसलिए यहां एक तालिका है जो वर्तमान स्थिति को दर्शाती है:

उज्जवल भविष्य

उपलब्ध तीन विकल्पों में से प्रत्येक की अपनी कमियां हैं। हालाँकि, हम उन्हें ठीक कर सकते हैं:

• मानक हास्केल लें और singletons माध्यम से असुविधाजनक कोडिंग के बजाय सीधे निर्भर प्रकार जोड़ें। (आसान काम से कहा।)
• Agda ले लो और इसके लिए एक कुशल कोड जनरेटर और RTS लागू करें। (आसान काम से कहा।)
• एक्सटेंशन के साथ हास्केल लें, बग को ठीक करें और निर्भर प्रकारों के कोडिंग को सरल बनाने के लिए नए एक्सटेंशन जोड़ना जारी रखें। (आसान काम से कहा।)

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

सिंगलेट्स से छुटकारा

प्रगति का एक अच्छा संकेतक singletons पुस्तकालय का सरलीकरण है। जैसा कि आश्रित प्रकारों को हास्केल में लागू किया जाता है, वर्कअराउंड और singletons में लागू विशेष मामलों की विशेष हैंडलिंग की अब आवश्यकता नहीं है। अंततः, इस पैकेज की आवश्यकता पूरी तरह से गायब हो जाएगी। उदाहरण के लिए, 2016 में, -XTypeInType एक्सटेंशन का उपयोग करते -XTypeInType मैंने केप्रॉक्सी को SingKind और SomeSing से हटा दिया । यह परिवर्तन प्रकारों और प्रकारों के मिलन से संभव हुआ। पुरानी और नई परिभाषाओं की तुलना करें:

 class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where type DemoteRep kparam :: * fromSing :: SingKind (a :: k) -> DemoteRep kparam toSing :: DemoteRep kparam -> SomeSing kparam type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k) data SomeSing (kproxy :: KProxy k) where SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k) 

पुरानी परिभाषाओं में, k विशेष रूप से व्यू पोजीशन में होता है, फॉर्म t :: k के एनोटेशन के दाईं ओर। हम kparam :: KProxy k उपयोग kparam :: KProxy k को k को प्रकारों में स्थानांतरित करने k लिए।

 class SingKind k where type DemoteRep k :: * fromSing :: SingKind (a :: k) -> DemoteRep k toSing :: DemoteRep k -> SomeSing k type Demote (a :: k) = DemoteRep k data SomeSing k where SomeSing :: Sing (a :: k) -> SomeSing k 

नई परिभाषाओं में, k स्वतंत्र रूप से दृश्य और प्रकार के पदों के बीच चलता है, इसलिए हमें KProxy आवश्यकता नहीं है। इसका कारण यह है कि, जीएचसी 8.0 से शुरू होकर, प्रकार और प्रकार एक ही सिंटैक्टिक श्रेणी में आते हैं।

मानक हास्केल में तीन पूरी तरह से अलग दुनिया हैं: शब्द, प्रकार और विचार। यदि आप जीएचसी 7.10 के स्रोत कोड को देखते हैं, तो आप विचारों के लिए एक अलग पार्सर और एक अलग चेक देख सकते हैं। जीएचसी 8.0 अब उनके पास नहीं है: प्रकार और विचारों के लिए पार्सर और सत्यापन आम हैं।

एक्सटेंशन के साथ हास्केल में, दृश्य केवल वह भूमिका है जिसमें प्रकार है:

 f :: T z -> ... -- 'z'   g :: T (a :: z) -> ... -- 'z'   h :: T z -> T (a :: z) -> ... -- 'z'   ,   

जीएचसी 8.08.4 में, अभी भी प्रकार और प्रकार में नाम संकल्प के बीच कुछ अंतर थे। लेकिन मैंने उन्हें जीएचसी 8.6 तक छोटा कर दिया: मैंने StarIsType एक्सटेंशन बनाया और StarIsType में PolyKinds कार्यक्षमता पेश की। मैंने शेष मतभेदों को जीएचसी 8.8 के लिए चेतावनी के रूप में बनाया , और जीएचसी 8.10 में उन्हें पूरी तरह से समाप्त कर दिया ( इस पैराग्राफ का अनुवाद अद्यतन किया गया है, मूल रूप में किए गए कार्यों को भविष्य के कार्यों के रूप में वर्णित किया गया है - लेखक का नोट )।

अगला कदम क्या है? आइए एक नज़र SingKind के नवीनतम संस्करण में SingKind पर:

 class SingKind k where type Demote k = (r :: Type) | r -> k fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k 

Demote टाइप Demote लिए टाइपिंग रिलेशन के बीच विसंगतियों Demote होना आवश्यक a :: t और फॉर्म का गंतव्य रिश्ता t :: k । सबसे अधिक बार (बीजीय डेटा प्रकारों के लिए), Demote एक पहचान मानचित्रण है:

• type Demote Bool = Bool
• type Demote [a] = [Demote a]
• type Demote (Either ab) = Either (Demote a) (Demote b)

इसलिए, Demote (Either [Bool] Bool) = Either [Bool] Bool । यह अवलोकन हमें निम्नलिखित सरलीकरण करने के लिए प्रेरित करता है:

 class SingKind k where fromSing :: Sing (a :: k) -> k toSing :: k -> SomeSing k 

जरूरत नहीं है! और, वास्तव में, यह दोनों Either [Bool] Bool और अन्य बीजीय डेटा प्रकारों के साथ काम करेगा। व्यवहार में, हालांकि, हम गैर-बीजीय डेटा प्रकारों के साथ काम कर रहे हैं: Integer, Natural , Char , Text , और इसी तरह। यदि प्रजातियों के रूप में उपयोग किया जाता है, तो वे आबादी नहीं हैं: 1 :: Natural शब्दों के स्तर पर सच है, लेकिन प्रकारों के स्तर पर नहीं। इस वजह से, हम ऐसी परिभाषाओं के साथ काम कर रहे हैं:

 type Demote Nat = Natural type Demote Symbol = Text 

इस समस्या का हल आदिम प्रकार को उठाना है। उदाहरण के लिए, Text इस तरह परिभाषित किया गया है:

 -- | A space efficient, packed, unboxed Unicode text type. data Text = Text {-# UNPACK #-} !Array -- payload (Word16 elements) {-# UNPACK #-} !Int -- offset (units of Word16, not Char) {-# UNPACK #-} !Int -- length (units of Word16, not Char) data Array = Array ByteArray# data Int = I# Int# 

यदि हम ByteArray# और Int# को ठीक प्रकार से बढ़ाते हैं, तो हम Symbol बजाय Text उपयोग कर सकते हैं। Natural और संभवतः अन्य प्रकार के एक जोड़े के साथ ऐसा करने से, आप Demote से छुटकारा पा सकते हैं, है ना?

काश, ऐसा नहीं होता। उपरोक्त में, मैंने सबसे महत्वपूर्ण डेटा प्रकार: फ़ंक्शंस के लिए एक अंधे आँख को बदल दिया। उनके पास एक विशेष Demote उदाहरण भी है:

 type Demote (k1 ~> k2) = Demote k1 -> Demote k2 type a ~> b = TyFun ab -> Type data TyFun :: Type -> Type -> Type 

~> यह एक प्रकार है जिसके साथ निजी-प्रकार के परिवारों और क्रियाशीलता के आधार पर सिंगल-लेवल फ़ंक्शन एकल प्रकारों में एन्कोडेड होते हैं।

सबसे पहले, यह एक अच्छा विचार की तरह लग सकता है ~> और -> , क्योंकि दोनों का अर्थ फ़ंक्शन का प्रकार (प्रकार) है। समस्या यह है कि -> प्रकार स्थिति में और -> दृश्य स्थिति में अलग-अलग चीजों का मतलब है। शब्द स्तर पर, a से b तक के सभी कार्य a -> b प्रकार के हैं। टाइप स्तर पर, केवल a से b तक के कंस्ट्रक्टर टाइप a -> b , लेकिन वे टाइप के पर्याय नहीं होते हैं और न ही टाइप के परिवार। प्रकारों को कम करने के लिए, GHC मान लेता है कि f ~ g और a ~ b का पालन fa ~ gb , जो निर्माणकर्ताओं के लिए सही है, लेकिन कार्यों के लिए नहीं - इसीलिए एक सीमा है।

इसलिए, कार्यों को प्रकारों के स्तर तक बढ़ाने के लिए, लेकिन प्रकार की सुरक्षा को बनाए रखने के लिए, हमें निर्माणकर्ताओं को एक अलग प्रकार पर ले जाना होगा। हम इसे a :-> b , क्योंकि यह वास्तव में सच होगा कि f ~ g और a ~ b follow from fa ~ gb । अन्य कार्य अभी भी प्रकार के होंगे a -> b । उदाहरण के लिए, Just :: a :-> Maybe a , लेकिन Just :: a :-> Maybe a ही समय में Just :: a :-> Maybe a isJust :: Maybe a -> Bool ।

जब Demote समाप्त हो जाता है, तो अंतिम कदम खुद Sing छुटकारा पाने के लिए है। ऐसा करने के लिए, हमें एक नए क्वांटिफायर की आवश्यकता है, जो forall और -> बीच एक संकर है। आइए इसस्ट फ़ंक्शन पर एक नज़र डालें:

 isJust :: forall a. Maybe a -> Bool isJust = \x -> case x of Nothing -> False Just _ -> True 

isJust फ़ंक्शन isJust a और फिर मान x :: Maybe a साथ टाइप किया जाता a x :: Maybe a । इन दो मापदंडों में अलग-अलग गुण हैं:

• मुखरता। isJust (Just "hello") कॉल में, हम x = Just "hello" स्पष्ट रूप से पास करते हैं, और a = String संकलक द्वारा isJust (Just "hello") रूप से आउटपुट होता है। आधुनिक हास्केल में, हम दोनों मापदंडों के स्पष्ट पारित होने को भी मजबूर कर सकते हैं: isJust @String (Just "hello") ।
• प्रासंगिकता। कोड में isJust के इनपुट के लिए दिया गया मान भी कार्यक्रम के निष्पादन के दौरान प्रेषित किया जाएगा: हम case से मिलान करने के लिए एक पैटर्न का प्रदर्शन करते हैं यह सत्यापित करने के लिए कि यह Nothing या Just । इसलिए, मान को प्रासंगिक माना जाता है। लेकिन इसका प्रकार मिटा दिया जाता है और पैटर्न के साथ तुलना नहीं की जा सकती है: फ़ंक्शन Maybe Int , Maybe String , Maybe Bool , आदि। इसलिए, यह अप्रासंगिक माना जाता है। इस संपत्ति को पैरामीट्रिकिटी भी कहा जाता है।
• निर्भरता। forall a. t forall a. t , टाइप t a को संदर्भित कर सकता a , और इसलिए, विशेष रूप से पारित a पर निर्भर करता a । उदाहरण के लिए, isJust @String प्रकार का है Maybe String -> Bool , और isJust @Int प्रकार का है Maybe Int -> Bool । इसका मतलब यह है कि forall एक आश्रित मात्रात्मक है। मान पैरामीटर के साथ अंतर पर ध्यान दें: इससे कोई फर्क नहीं पड़ता कि हम कॉल करते isJust Nothing या isJust (Just …) , परिणाम प्रकार हमेशा Bool । इसलिए, -> एक स्वतंत्र क्वांटिफायर है।

Sing को बाहर निकालने के लिए, हमें एक क्वांटिफायर स्पष्ट और प्रासंगिक चाहिए, जैसे a -> b , और एक ही समय पर निर्भर है, जैसे कि forall (a :: k). t forall (a :: k). t । इसे foreach (a :: k) -> t रूप में निरूपित करें। SingI को बाहर SingI , हम एक अंतर्निहित प्रासंगिक आश्रित क्वांटिफायर, SingI foreach (a :: k). t भी पेश करते हैं foreach (a :: k). t foreach (a :: k). t । नतीजतन, singletons की ज़रूरत नहीं होगी क्योंकि हमने भाषा पर निर्भर कार्यों को जोड़ा है।

निर्भर प्रकारों के साथ हास्केल पर एक संक्षिप्त नज़र

प्रकारों के प्रकार और lookupS क्वांटिफायर के कार्यों के उदय के साथ, हम lookupS को फिर से lookupS सकते हैं:

 data N = Z | SN len :: [a] -> N len [] = Z len (_:xs) = S (len xs) data Fin n where FZ :: Fin (S n) FS :: Fin n -> Fin (S n) lookupS :: foreach (xs :: [a]) -> Fin (len xs) -> a lookupS [] = \case{} lookupS (x:xs) = \case FZ -> x FS i' -> lookupS xs i' 

संक्षेप में, कोड नहीं था, फिर भी निरर्थक कोड को छिपाने में singletons बहुत अच्छे थे। हालाँकि, नया कोड बहुत सरल है: अब SingKind , SList , SNil , fromSing , fromSing । TemplateHaskell का कोई उपयोग नहीं है, क्योंकि अब हम Len प्रकार के परिवार बनाने के बजाय सीधे len फ़ंक्शन को कॉल कर सकते हैं। प्रदर्शन भी बेहतर होगा, क्योंकि अब आपको बदलने की आवश्यकता नहीं है।

हमें अभी भी Int बजाय एक निर्धारित रूप से परिभाषित N को वापस करने के लिए len रूप में length को फिर से परिभाषित करना है। शायद हास्केल पर निर्भर प्रकारों को जोड़ने के ढांचे में इस समस्या पर विचार नहीं किया जाना चाहिए, क्योंकि Agda lookup फ़ंक्शन में एक इंडिविजुअल रूप से परिभाषित N का भी उपयोग करता है।

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

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

कोश