सांख्यिकीय रूप से सुरक्षित टाइपिंग आ ला पायथन

हाय, हैब्र।

दूसरे दिन, मेरे एक शौक प्रोजेक्ट में, टास्क मेट्रिक्स का भंडार लिखने का हुआ।

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

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

तो, पहले हम समस्या का सूत्रीकरण करते हैं। हमें कुछ वस्तुओं को पहले अज्ञात प्रकारों के मूल्यों के साथ जोड़ने में सक्षम होने की आवश्यकता है। या, दूसरे शब्दों में, यह आवश्यक है कि पहले के अज्ञात प्रकार के मान किसी प्रकार के मानचित्र में कुंजियों के रूप में कार्य करते हैं।

स्वाभाविक रूप से, हम पागल नहीं हैं और हमें किसी भी प्रकार के मूल्यों के समर्थन की आवश्यकता नहीं होगी। हमें आदेश देने के अर्थ में प्रकार (भले ही अज्ञात) का समर्थन करने की आवश्यकता है। हास्केल शब्दों में, इसका मतलब है कि हम उन प्रकारों का समर्थन करते हैं जो Ord a वर्ग को लागू करते हैं।

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

जब कुछ प्रकार के वर्ग को लागू करने के लिए ज्ञात मूल्यों को संग्रहीत करने की बात आती है, तो आमतौर पर हास्केल में अस्तित्वगत प्रकार का उपयोग किया जाता है:

 data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd 

इसलिए, यदि हमें SomeOrd प्रकार का ऑब्जेक्ट दिया जाता है और हमने इसके लिए पैटर्न मिलान किया है:

 foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ... 

उसके बाद (1) हम यह नहीं जानते हैं कि किस प्रकार की val है, लेकिन हम जानते हैं (और, सबसे महत्वपूर्ण बात, टाइमर भी जानता है) कि val ऑर्डेक्लास को लागू करता है।

हालांकि, यदि वर्ग के प्रकार कार्य दो (या अधिक) तर्क देते हैं, तो इस तरह के रिकॉर्ड का उपयोग बहुत कम होता है:

 tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ? 

Ord विधियों का उपयोग करने के लिए, यह आवश्यक है कि val और val एक ही प्रकार के हैं, लेकिन यह बिल्कुल भी नहीं है! यह पता चला है कि हमारे SomeOrd बेकार है। क्या करें?

इस तथ्य के बावजूद कि हास्केल एक आक्रामक भाषा है जो आक्रामक प्रकार के उन्मूलन के साथ है (संकलन के बाद, वे सामान्य रूप से वहां नहीं होते हैं), कंपाइलर अभी भी रनटाइम प्रकार के प्रतिनिधि उत्पन्न कर सकता है यदि इसके बारे में पूछा जाए। प्रकार का रोल प्रतिनिधि टाइप टाइप a का मान TypeRep a , और प्रार्थना जनरेशन का जवाब टाइप करने Typeable टाइपकास्ट द्वारा दिया Typeable ।

इसके अलावा, अगर हमारे पास rep1 :: TypeRep a, rep2 :: TypeRep b दो अलग-अलग उदाहरण हैं rep1 :: TypeRep a, rep2 :: TypeRep b , तो हम उनकी तुलना कर सकते हैं और जांच सकते हैं कि वे एक ही प्रकार का प्रतिनिधित्व करते हैं या नहीं। इसके अलावा, अगर वे वास्तव में एक ही प्रकार का प्रतिनिधित्व करते हैं, तो जाहिर है कि b के साथ a संयोग है। और, सबसे महत्वपूर्ण बात यह है कि समानता के लिए प्रकार के निरूपण की जाँच का कार्य एक परिणाम देता है जो इस प्रकार के टाइपकर्ता को समझा सकता है:

 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) 

यहाँ क्या बकवास लिखी गई है?

सबसे पहले, eqTypeRep एक फ़ंक्शन है।

दूसरे, यह बहुरूपी है, लेकिन न केवल प्रकार से, बल्कि इन प्रकारों की किस्मों द्वारा भी। यह भाग forall k1 k2 (a :: k1) (b :: k2) द्वारा इंगित किया गया है - इसका अर्थ है कि a और b न केवल Int या [String] जैसे सामान्य प्रकार हो सकते हैं, बल्कि उदाहरण के लिए, कुख्यात निर्माणकर्ता (देखें) DataKinds और हास्केल प्रमाणित करने के अन्य प्रयास)। लेकिन हमें यह सब करने की जरूरत नहीं है।

तीसरा, यह संभावित विभिन्न प्रकारों के दो रनटाइम निरूपण को स्वीकार करता है, TypeRep a और TypeRep b ।

चौथा, यह Maybe (a :~~: b) प्रकार का मान लौटाता है Maybe (a :~~: b) । सबसे दिलचस्प बात यहाँ होती है।

यदि प्रकार मेल नहीं खाते हैं, तो फ़ंक्शन सामान्य Nothing लौटाता है, और सब कुछ ठीक है। यदि प्रकार मेल खाते हैं, तो फ़ंक्शन Just val , जहां val टाइप a :~~: b । आइए देखें कि यह किस प्रकार का है:

 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is -- inhabited by a terminating value if and only if @a@ is the same type as @b@. -- -- @since 4.10.0.0 data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a 

अब बात करते हैं। मान लीजिए कि हमें a :~~: b का वैल्यू वैल्यू मिलता है। इसे कैसे बनाया जा सकता है? एकमात्र तरीका HRefl कंस्ट्रक्टर के साथ है, और इस कंस्ट्रक्टर को आइकन के दोनों किनारों पर यह आवश्यक है :~~: यह समान होना चाहिए। इसलिए, b के साथ a संयोग है। इसके अलावा, अगर हम val पर zapternnom-match करते हैं, तो taypcheker को इसके बारे में भी पता चल जाएगा। इसलिए, हाँ, eqTypeRep फ़ंक्शन प्रमाण देता है कि दो संभावित भिन्न प्रकार समान हैं यदि वे वास्तव में समान हैं।

हालांकि, ऊपर के पैराग्राफ में, मैंने झूठ बोला था। कोई हमें हास्केल में कुछ लिखने से नहीं रोक रहा है

 wrong :: Int :~~: String wrong = wrong --    

या

 wrong :: Int :~~: String wrong = undefined 

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

यही कारण है कि प्रलेखन के टुकड़े में बस ऊपर उद्धृत किया गया है, समाप्ति मूल्य का उल्लेख किया गया है। ऊपर wrong के कार्यान्वयन के दोनों संस्करण इस बहुत ही समाप्ति मूल्य का उत्पादन नहीं करते हैं, जो हमें थोड़ा सा कारण और आत्मविश्वास देता है: यदि हास्केल पर हमारा कार्यक्रम समाप्त हो गया (और undefined में नहीं चला गया), तो इसका परिणाम लिखित प्रकारों से मेल खाता है। यहाँ, हालाँकि, आलस्य से संबंधित कुछ विवरण हैं, लेकिन हम इस विषय को नहीं खोलेंगे।

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

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

यह हमारे आवरण प्रकार के निम्नलिखित कार्यान्वयन की ओर ले जाता है:

 data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val 

अब हम एक फंक्शन लिखते हैं जो निम्नलिखित कार्य करता है:

1. प्रकार Dyn दो मूल्य;
2. एक फ़ंक्शन जो किसी भी प्रकार के दो मूल्यों के लिए कुछ पैदा करता है,
   forall (जब इसके लिए जिम्मेदार है) बनाने के दौरान केवल स्थिरांक के आधार पर,
   और जिसे कहा जाता है यदि दोनों Dyn एक ही प्रकार के मूल्यों को संग्रहीत करते हैं;
3. और फ़ॉलबैक फ़ंक्शन, जिसे पिछले एक के बजाय कहा जाता है, यदि प्रकार अभी भी अलग हैं:

 withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

SomeTypeRep किसी के लिए TypeRep a ऊपर एक अस्तित्वगत आवरण a ।

अब हम लागू कर सकते हैं, उदाहरण के लिए, समानता की जाँच और तुलना:

 instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare 

यहां हमने इस तथ्य का लाभ उठाया कि SomeTypeRep की एक दूसरे के साथ तुलना की जा सकती है, इसलिए ऑर्डर करने के लिए फालबैक फ़ंक्शन की compare भी की जाती है।

हो गया।

केवल अब यह सामान्य नहीं करना पाप है: ध्यान दें कि Dyn भीतर, toDyn , withDyns हम विशेष रूप से Ord उपयोग नहीं करते हैं, और यह स्थिरांक का कोई अन्य सेट हो सकता है, इसलिए हम ConstraintKinds एक्सटेंशन को सक्षम कर सकते हैं और Dyn मापदंडों का Dyn विशिष्ट सेट के Dyn पैरामीटर को सामान्य कर सकते हैं जो हम हमारे विशिष्ट कार्य में आवश्यक:

 data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

फिर Dyn Ord हमारी Dyn Monoid प्रकार होगा, और, कहेंगे, Dyn Monoid आपको मनमाने तरीके से Dyn Monoid स्टोर करने और उनके साथ कुछ Dyn Monoid की अनुमति देगा।

आइए हम अपने नए Dyn लिए आवश्यक उदाहरण लिखें:

 instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare 

... केवल यह काम नहीं करता है टाइपकर्ता को यह नहीं पता है कि Dyn Ord Eq भी लागू करता है,
इसलिए आपको पूरी पदानुक्रम की प्रतिलिपि बनानी होगी:

 instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare 

अच्छा, अब पक्का।

... शायद, एक आधुनिक हास्केल में, आप इसे बना सकते हैं ताकि टाइमर ही फॉर्म के उदाहरणों को प्रदर्शित करे

 instance C_i (Dyn (C_1, ... C_n)) where ... 

क्योंकि वहाँ कुछ प्रोलिकल निकलता है, लेकिन मैंने इसे अभी तक पूरा नहीं किया है, मुझे इसे चुनने के लिए बैठना होगा। देखते रहो।

और यह भी, यदि आप ध्यान से स्क्विंट करते हैं, तो आप देख सकते हैं कि हमारा Dyn गुप्त भाषाओं के प्रकार (ty : Type ** val : ty) की एक निर्भर जोड़ी की तरह संदिग्ध रूप से दिखता है। लेकिन केवल मेरे लिए जानी जाने वाली भाषाओं में, इस प्रकार का मिलान करना असंभव है, क्योंकि पारमार्थिकता (जो इस मामले में, IMHO, बहुत व्यापक रूप से व्याख्या की जाती है), लेकिन यहां यह संभव लगता है।

लेकिन सबसे महत्वपूर्ण बात - अब आप सुरक्षित रूप से Map (Dyn Ord) SomeValue जैसे कुछ भी कर सकते हैं और कुंजी के रूप में किसी भी मान का उपयोग कर सकते हैं, जब तक कि वे स्वयं तुलना का समर्थन करते हैं। उदाहरण के लिए, मीट्रिक विवरण के साथ पहचानकर्ताओं को कुंजी के रूप में इस्तेमाल किया जा सकता है, लेकिन यह अगले लेख के लिए एक विषय है।