कैसे अधिक अमान्य राज्यों को और भी अधिक अकथनीय बनाने के लिए

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

संक्षेप में, वह लेख किसी संस्था को मेलिंग एड्रेस और ईमेल एड्रेस के साथ-साथ अतिरिक्त शर्त के साथ चर्चा करता है कि इनमें से कम से कम एक एड्रेस होना चाहिए। इस स्थिति को किस प्रकार के स्तर पर व्यक्त करना प्रस्तावित है? इस पते को इस प्रकार लिखना प्रस्तावित है:

type ContactInfo = | EmailOnly of EmailContactInfo | PostOnly of PostalContactInfo | EmailAndPost of EmailContactInfo * PostalContactInfo 

इस दृष्टिकोण में क्या समस्याएं हैं?

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

शेयर

इस समस्या को कैसे हल करें? आइए कल्पना करने की कोशिश करें। पहले हम पता वर्ग को विघटित करते हैं और अलग करते हैं (उदाहरण के लिए, कार्यालय में मेल / ईमेल / डेस्क नंबर) और इस वर्ग के अनुरूप सामग्री।

 data AddrType = Post | Email | Office 

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

यदि हमने कुछ सामान्य OOP भाषा के कुछ निर्माता के रनटाइम में संबंधित स्थिति की जाँच की, तो हम सिर्फ एक फ़ंक्शन लिखेंगे

 valid :: [AddrType] -> Bool valid xs = let hasNoDups = nub xs == xs --      hasPost = Post `elem` xs hasEmail = Email `elem` xs hasOffice = Office `elem` xs in hasNoDups && (hasPost || (hasEmail && hasOffice)) 

और अगर False लौटाता है तो उसे कुछ फाँसी की सजा दी जाएगी।

क्या हम संकलन करते समय टाइमर की मदद से इसके समान स्थिति की जांच कर सकते हैं? यह पता चला है कि हाँ, हम कर सकते हैं, अगर भाषा का प्रकार सिस्टम पर्याप्त अभिव्यंजक है, और बाकी लेख हम इस दृष्टिकोण को चुनेंगे।

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

 valid : List AddrType -> Bool 

अब याद रखें कि एड्रेस क्लासेस के अलावा, हमें उनकी सामग्री की भी आवश्यकता है, और एड्रेस क्लास पर फ़ील्ड की निर्भरता को एनएडीटी के रूप में एनकोड करें:

 data AddrFields : AddrType -> Type where PostFields : (city : String) -> (street : String) -> AddrFields Post EmailFields : (email : String) -> AddrFields Email OfficeFields : (floor : Int) -> (desk : Nat) -> AddrFields Office 

यही है, अगर हमें AddrFields t के fields मान दिया जाता है, तो हम जानते हैं कि t कुछ AddrType AddrType और उन fields में इस विशेष वर्ग के अनुरूप फ़ील्ड्स का एक सेट होता है।

 addrFields : AddrType -> Type addrFields Post = PostFields addrFields Email = EmailFields addrFields Office = OfficeFields 

इस मॉडल में पूरा पता क्या है? यह पता वर्ग और संबंधित क्षेत्रों की एक जोड़ी है:

 Addr : Type Addr = (t : AddrType ** AddrFields t) 

टाइप थ्योरी के प्रशंसक कहेंगे कि यह एक अस्तित्व पर निर्भर प्रकार है: यदि हमें कुछ प्रकार के Addr का मान दिया जाता है, तो इसका अर्थ है कि AddrType का एक मान t और AddrFields t फ़ील्ड का एक समान सेट है। स्वाभाविक रूप से, एक अलग वर्ग के पते एक ही प्रकार के होते हैं:

 someEmailAddr : Addr someEmailAddr = (Email ** EmailFields "that@feel.bro") someOfficeAddr : Addr someOfficeAddr = (Office ** OfficeFields (-2) 762) 

इसके अलावा, अगर EmailFields हमें दिया जाता है, तो एकमात्र पता वर्ग जो उपयुक्त है, वह Email , इसलिए आप इसे छोड़ सकते हैं, टाइमर इसे स्वयं प्रिंट करेगा:

 someEmailAddr : Addr someEmailAddr = (_ ** EmailFields "that@feel.bro") someOfficeAddr : Addr someOfficeAddr = (_ ** OfficeFields (-2) 762) 

हम एक सहायक फ़ंक्शन लिखते हैं जो पता सूची से पता कक्षाओं की संबंधित सूची देता है, और तुरंत इसे एक मनमाना फ़ाइटर पर काम करने के लिए सामान्यीकृत करता है:

 types : Functor f => f Addr -> f AddrType types = map fst 

यहां, अस्तित्वगत Addr प्रकार एक परिचित जोड़े की तरह व्यवहार करता है: विशेष रूप से, आप इसके पहले घटक AddrType (कार्य के साथ कार्य के लिए पूछ सकते हैं: मैं दूसरे घटक के लिए क्यों नहीं पूछ सकता?)।

उठाना

अब हम अपनी कहानी के एक प्रमुख भाग पर चलते हैं। इसलिए, हमारे पास List Addr पते और कुछ valid : List AddrType -> Bool विधेय की valid : List AddrType -> Bool , जिनकी सूची के लिए निष्पादन हम इस प्रकार के स्तर पर गारंटी देना चाहते हैं। हम उन्हें कैसे जोड़ सकते हैं? बेशक, एक और प्रकार!

 data ValidatedAddrList : List Addr -> Type where MkValidatedAddrList : (lst : List Addr) -> (prf : valid (types lst) = True) -> ValidatedAddrList lst 

अब हम यहां जो लिखा है उसका विश्लेषण करेंगे।

data ValidatedAddrList : List Addr -> Type where इसका अर्थ है कि ValidatedAddrList टाइप किया गया है, वास्तव में, एड्रेस लिस्ट द्वारा।

आइए इस प्रकार के एकमात्र MkValidatedAddrList निर्माता के हस्ताक्षर को देखें: (lst : List Addr) -> (prf : valid (types lst) = True) -> ValidatedAddrList lst type (lst : List Addr) -> (prf : valid (types lst) = True) -> ValidatedAddrList lst । यही है, यह lst पतों की कुछ सूची लेता है और प्रकार के valid (types lst) = True का एक और prf तर्क valid (types lst) = True । इस प्रकार का क्या अर्थ है? तो इसका मतलब है कि बाईं ओर का मूल्य = के दाईं ओर के मूल्य के बराबर है, अर्थात, valid (types lst) , वास्तव में, सत्य है।

यह कैसे काम करता है? हस्ताक्षर = (x : A) -> (y : B) -> Type दिखता है। यही है, = दो मनमाना मूल्य लेता है x और y (संभवतः विभिन्न प्रकार A और B , जिसका अर्थ है कि आईडी में असमानता विषम है, और यह कि यह सिद्धांत के दृष्टिकोण से कुछ अस्पष्ट है, लेकिन यह एक और चर्चा का विषय है)। तब क्या समानता प्रदर्शित करता है? और इस तथ्य के कारण कि एकमात्र निर्माता = - लगभग (x : A) -> x = x हस्ताक्षर के साथ वापस। यही है, अगर हमारे पास टाइप x = y का मान है, तो हम जानते हैं कि यह Refl (क्योंकि कोई अन्य निर्माता नहीं हैं) का उपयोग करके बनाया गया था, जिसका अर्थ है कि x वास्तव में y बराबर है।

ध्यान दें कि यही कारण है कि हास्केल में हम हमेशा सबसे अच्छा दिखावा करेंगे कि हम कुछ साबित कर रहे हैं, क्योंकि हास्केल ने undefined कि किसी भी प्रकार का निवास है, इसलिए उपरोक्त तर्क वहां काम नहीं करता है: किसी भी x , y टाइप x = y का y शब्द x = y को undefined के माध्यम से बनाया जा सकता है (या अनंत पुनरावृत्ति के माध्यम से, यह कहें कि बड़े और प्रकार के सिद्धांत के संदर्भ में यह समान है)।

हम यह भी ध्यान देते हैं कि यहाँ समानता का मतलब Haskell के Eq या C ++ में किसी भी operator== अर्थ में नहीं है, बल्कि इससे कहीं अधिक सख्त है: संरचनात्मक, जो, सरलीकरण का अर्थ है कि दोनों मूल्यों का एक ही रूप है । यही है, उसे धोखा देने के लिए तो बस काम नहीं करता है। लेकिन समानता के मुद्दे परंपरागत रूप से एक अलग लेख के लिए तैयार किए जाते हैं।

समानता की हमारी समझ को मजबूत करने के लिए, हम valid फ़ंक्शन के लिए इकाई परीक्षण लिखते हैं:

 testPostValid : valid [Post] = True testPostValid = Refl testEmptyInvalid : valid [] = False testEmptyInvalid = Refl testDupsInvalid : valid [Post, Post] = False testDupsInvalid = Refl testPostEmailValid : valid [Post, Email] = True testPostEmailValid = Refl 

ये परीक्षण अच्छे हैं कि आपको उन्हें चलाने की भी आवश्यकता नहीं है, यह पर्याप्त है कि टाइपर ने उन्हें जांचा। वास्तव में, आइए True को False बदलें, उदाहरण के लिए, उनमें से सबसे पहले और देखें कि क्या होता है:

 testPostValid : valid [Post] = False testPostValid = Refl 

टाइपरखेर शपथ लेता है

जैसी उम्मीद थी। अद्भुत।

सरल

अब हमारे ValidatedAddrList थोड़ा ValidatedAddrList ।

सबसे पहले, True साथ एक निश्चित मूल्य की तुलना करने का पैटर्न काफी सामान्य है, इसलिए एक विशेष प्रकार है, So इसके लिए आईडी में: आप So x को x = True समानार्थक शब्द के रूप में ले सकते हैं। चलो मान्यकृत की परिभाषा तय करें:

 data ValidatedAddrList : List Addr -> Type where MkValidatedAddrList : (lst : List Addr) -> (prf : So (valid $ types lst)) -> ValidatedAddrList lst 

इसके अलावा, So एक सुविधाजनक सहायक फ़ंक्शन choose , जो संक्षेप में चेक को प्रकारों के स्तर तक बढ़ाता है:

 > :doc choose Data.So.choose : (b : Bool) -> Either (So b) (So (not b)) Perform a case analysis on a Boolean, providing clients with a So proof 

यह हमारे लिए उपयोगी होगा जब हम ऐसे कार्यों को लिखते हैं जो इस प्रकार को संशोधित करते हैं।

दूसरे, कभी-कभी (विशेष रूप से संवादात्मक विकास में) आइडल अपने दम prf उचित prf मूल्य पा सकते हैं। आदेश में कि ऐसे मामलों में इसे हाथ से बनाने के लिए आवश्यक नहीं था, एक समान संश्लिष्ट चीनी है:

 data ValidatedAddrList : List Addr -> Type where MkValidatedAddrList : (lst : List Addr) -> {auto prf : So (valid $ types lst)} -> ValidatedAddrList lst 

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

तो यह नया ValidatedAddrList हमें क्या देता है? और यह इस तरह की श्रृंखला को तर्क देता है: val ValidatedAddrList lst का मान है। इसका मतलब यह है कि lst पतों की एक सूची है, और इसके अलावा, val MkValidatedAddrList कंस्ट्रक्टर का उपयोग करके बनाया गया था, जिसके लिए हमने यह बहुत ही MkValidatedAddrList और एक अन्य प्रकार का prf मान पारित किया है So (valid $ types lst) , जो लगभग valid (types lst) = True । और इसलिए कि हम prf निर्माण कर सकते हैं, हमें जरूरत है, वास्तव में, यह साबित करने के लिए कि यह समानता रखती है।

और सबसे खूबसूरत बात यह है कि यह सब एक झांकी द्वारा जांचा जाता है। हां, वैधता जाँच रनटाइम में करनी होगी (क्योंकि पते किसी फ़ाइल या नेटवर्क से पढ़े जा सकते हैं), लेकिन टाइमर यह सुनिश्चित करेगा कि यह जाँच की जाए: इसके बिना, ValidatedAddrList बनाना असंभव है। कम से कम आइडियल में। हास्केल में, अफसोस।

डालने

सत्यापन की अनिवार्यता को सत्यापित करने के लिए, हम सूची में एक पता जोड़ने के लिए एक फ़ंक्शन लिखने का प्रयास करेंगे। पहला प्रयास:

 insert : (addr : Addr) -> ValidatedAddrList lst -> ValidatedAddrList (addr :: lst) insert addr (MkValidatedAddrList lst) = MkValidatedAddrList (addr :: lst) 

नहीं, टाइपो-चेकर उंगलियों पर देता है (हालांकि बहुत पठनीय नहीं है, valid की लागत बहुत जटिल है):

हम इसकी प्रतिलिपि कैसे प्राप्त करें? उपरोक्त choose अलावा कोई नहीं। दूसरा प्रयास:

 insert : (addr : Addr) -> ValidatedAddrList lst -> ValidatedAddrList (addr :: lst) insert addr (MkValidatedAddrList lst) = case choose (valid $ types (addr :: lst)) of Left l => MkValidatedAddrList (addr :: lst) Right r => ?rhs 

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

 insert : (addr : Addr) -> ValidatedAddrList lst -> Maybe (ValidatedAddrList (addr :: lst)) insert addr (MkValidatedAddrList lst) = case choose (valid $ types (addr :: lst)) of Left l => Just $ MkValidatedAddrList (addr :: lst) Right r => Nothing 

यह टाइल है और जैसा होना चाहिए, काम करता है।

लेकिन अब निम्नलिखित बहुत स्पष्ट समस्या उत्पन्न नहीं होती है, जो वास्तव में, मूल लेख में थी। इस फ़ंक्शन का प्रकार इस तरह के कार्यान्वयन को लिखना बंद नहीं करता है:

 insert : (addr : Addr) -> ValidatedAddrList lst -> Maybe (ValidatedAddrList (addr :: lst)) insert addr (MkValidatedAddrList lst) = Nothing 

यही है, हम हमेशा कहते हैं कि हम पते की एक नई सूची नहीं बना सकते। Taypchekaetsya? हां। क्या यह सही है? खैर, शायद ही। क्या इससे बचा जा सकता है?

यह पता चला है कि यह संभव है, और हमारे पास इसके लिए सभी आवश्यक उपकरण हैं। यदि सफल है, तो एक ValidatedAddrList रिटर्न insert , जिसमें इस सफलता का प्रमाण है। तो सुरुचिपूर्ण समरूपता जोड़ें और फ़ंक्शन को भी विफलता का प्रमाण देने के लिए कहें!

 insert : (addr : Addr) -> ValidatedAddrList lst -> Either (So (not $ valid $ types (addr :: lst))) (ValidatedAddrList (addr :: lst)) insert addr (MkValidatedAddrList lst) = case choose (valid $ types (addr :: lst)) of Left l => Right $ MkValidatedAddrList (addr :: lst) Right r => Left r 

अब हम सिर्फ ले नहीं सकते और हमेशा Nothing लौटा सकते।

आप पते हटाने के कार्यों और पसंद के लिए भी ऐसा कर सकते हैं।

देखते हैं कि अब यह सब आखिर में कैसा दिखता है।

आइए एक खाली पता सूची बनाने का प्रयास करें:

यह असंभव है, एक खाली सूची मान्य नहीं है।

सिर्फ एक मेलिंग पते की सूची के बारे में कैसे?

ठीक है, चलो मेलिंग पते को उस सूची में सम्मिलित करने का प्रयास करें जिसमें पहले से ही मेलिंग पता है:

आइए ईमेल डालने की कोशिश करें:

अंत में, सब कुछ उम्मीद के मुताबिक काम करता है।

Ffuh। मुझे लगा कि यह तीन लाइनें होंगी, लेकिन यह थोड़ी लंबी हो गई। इसलिए यह पता लगाने के लिए कि हम हास्केल में कितनी दूर जा सकते हैं, हम अगले लेख में होंगे। इस बीच, थोड़ा

प्रतिबिंबित

क्या, अंत में, इस तरह के एक निर्णय का लाभ लेख में दिए गए की तुलना में है, जिसे हमने शुरुआत में संदर्भित किया था?

1. यह, फिर से, और अधिक स्केलेबल है। जटिल सत्यापन कार्यों को लिखना आसान है।
2. यह अधिक पृथक है। क्लाइंट कोड को यह पता नहीं होना चाहिए कि सत्यापन फ़ंक्शन के अंदर क्या है, जबकि मूल लेख से ContactInfo फॉर्म को इसे बांधने की आवश्यकता है।
3. सत्यापन तर्क को सामान्य और परिचित कार्यों के रूप में लिखा जाता है, ताकि इसे सही समय परीक्षण के साथ विचारशील पढ़ने और परीक्षण के साथ ठीक से जांचा जा सके, बजाय डेटा प्रकार के फॉर्म से सत्यापन के अर्थ को प्राप्त करने के जो पहले से सत्यापित परिणाम का प्रतिनिधित्व करता है।
4. यह उन कार्यों के व्यवहार को अधिक सटीक रूप से निर्दिष्ट करना संभव बनाता है जो हमारे लिए विशेष रूप से डेटा प्रकार के साथ काम करते हैं, विशेष रूप से परीक्षण पास करने में विफलता के मामले में। उदाहरण के लिए, परिणाम के रूप में लिखी गई insert गलत तरीके से लिखना असंभव है । इसी तरह, कोई insertOrReplace , insertOrIgnore और insertOrReplace लिख सकता है, जिसका व्यवहार टाइप में पूरी तरह से निर्दिष्ट है।

OOP समाधान की तुलना में लाभ क्या है?

 class ValidatedAddrListClass { public: ValidatedAddrListClass(std::vector<Addr> addrs) { if (!valid(addrs)) throw ValidationError {}; } }; 

1. कोड अधिक संशोधित और सुरक्षित है। उपरोक्त मामले में, एक चेक एक क्रिया है जिसे एक बार जांचा जाता है, और जिसके बारे में वे बाद में भूल जाते हैं। सब कुछ ईमानदारी और इस समझ पर आधारित है कि यदि आपके पास ValidatedAddrListClass , तो इसके कार्यान्वयन ने एक बार वहां जांच की थी। वर्ग से इस चेक के तथ्य को एक निश्चित मूल्य के रूप में नहीं चुना जा सकता है। कुछ प्रकार के मूल्य के मामले में, इस मूल्य को कार्यक्रम के विभिन्न हिस्सों के बीच स्थानांतरित किया जा सकता है, जिसका उपयोग अधिक जटिल मूल्यों (उदाहरण के लिए, फिर से, इस चेक को अस्वीकार करने के लिए किया जाता है), जांच (अगला पैराग्राफ देखें), और आम तौर पर वैसा ही करें जैसा हम करते थे। मूल्यों के साथ।
2. इस तरह के चेक का उपयोग (निर्भर) पैटर्न मिलान में किया जा सकता है। सच है, इस फ़ंक्शन के मामले में valid नहीं valid और न ही idris के मामले में, यह दर्दनाक रूप से जटिल है, और मूर्खतापूर्ण रूप से सुस्त है ताकि पैटर्न के लिए उपयोगी जानकारी को valid संरचना से निकाला जा सके। फिर भी, valid को थोड़ा अधिक अनुकूल पैटर्न-मिलान शैली में फिर से लिखा जा सकता है, लेकिन यह इस लेख के दायरे से परे है और आमतौर पर अपने आप में तुच्छ नहीं है।

नुकसान क्या हैं?

मुझे केवल एक गंभीर मौलिक दोष दिखाई देता है: valid बहुत मूर्खतापूर्ण कार्य है। यह केवल एक बिट जानकारी देता है - चाहे डेटा सत्यापन से गुजरा हो या नहीं। होशियार प्रकार के मामले में, हम कुछ और दिलचस्प हासिल कर सकते हैं।

उदाहरण के लिए, कल्पना करें कि पते की विशिष्टता के लिए आवश्यकता टीके से गायब हो गई है। इस मामले में, यह स्पष्ट है कि मौजूदा पते की सूची में एक नया पता जोड़ने से सूची अमान्य नहीं होगी, इसलिए हम इस प्रकार के साथ एक फ़ंक्शन लिखकर इस सिद्धांत को साबित कर सकते हैं So (valid $ types lst) -> So (valid $ types $ addr :: lst) , और इसका उपयोग करें, उदाहरण के लिए, टाइप-सेफ लिखने के लिए हमेशा सफल

 insert : (addr : Addr) -> ValidatedAddrList lst -> ValidatedAddrList (addr :: lst) 

लेकिन, अफसोस, पुनरावृत्ति और प्रेरण की तरह प्रमेय, और हमारी समस्या में कोई सुंदर प्रेरक संरचना नहीं है, इसलिए, मेरी राय में, ओक बूलियन valid के साथ कोड भी अच्छा है।