हैकेल उदाहरणों के लिए आवेदक कानूनों के सबूत

Question

क्या आस्केटिव टाइपक्लास के सभी हास्केल उदाहरण हैं जिन्हें हम हास्केल प्लेटफ़ॉर्म के साथ प्राप्त करते हैं, सभी आवेदक कानूनों को पूरा करने के लिए साबित हुए हैं? यदि हां, तो हम उन सबूत कहां पाते हैं?

Control.Applicative का स्रोत कोड इस बात का कोई सबूत नहीं है कि विभिन्न मामलों के लिए आवेदक कानून हैं। यह सिर्फ कहा गया है कि

-- | A functor with application. 
-- 
--Instances should satisfy the following laws: 

यह तो सिर्फ टिप्पणी में कानून में कहा गया है।

मुझे अन्य टाइपक्लास (वैकल्पिक और मोनाड) के उदाहरणों के लिए भी एक समान मामला मिला।

क्या इन पुस्तकालयों के उपयोगकर्ता स्वयं इन कानूनों को सत्यापित करना चाहते हैं?

लेकिन मैं सोच रहा था कि डेवलपर्स द्वारा इन कानूनों के कठोर सबूत दिए गए हैं या नहीं?

फिर से, मुझे पता है कि आईओ मोनाड के लिए एप्लाकेट (या मोनाड) कानूनों का एक कठोर सबूत, जिसमें सामान्य रूप से बाहरी दुनिया के साथ बात करना शामिल है, बहुत जटिल हो सकता है।

धन्यवाद।

Answer 1

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

मुझे पूरा यकीन है कि इन प्रकार के सबूत मानक स्थान पर पत्थर में नक़्क़ाशी नहीं किए गए हैं। ज्यादातर सबूतों को समुदाय के विभिन्न उत्सुक सदस्यों द्वारा बार-बार दोहराया गया है और मृत्यु के लिए जांच की गई है, इसलिए कुछ समय बाद हम जानते हैं कि कौन से कार्यान्वयन करते हैं और उनके कानूनों को पूरा नहीं करते हैं।

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

हालांकि, मुझे लगता है कि जब संभव हो, तो मूल भंडार में मशीन-चेक किए गए सबूत शामिल हो सकते हैं ताकि उपयोगकर्ता उन्हें आवश्यकतानुसार संदर्भित कर सकें।

Answer 2

उत्कृष्ट पुस्तकालय checkers है जो कानूनों की जांच के लिए क्विक चेक गुण प्रदान करता है।

Answer 3

प्रयोगात्मक पुस्तकालय ghc-proofs आप के लिए इस तरह के कानूनों को सत्यापित करने के संकलक का उपयोग करने की अनुमति देता है:

app_law_2 a b (c :: Succs a) = pure (.) <*> a <*> b <*> c 
          === a <*> (b <*> c) 

यह केवल कुछ मामलों में काम करता है, एक के रूप में इस तरह के in my blog post वर्णित है, और सबसे अच्छा एक प्रयोग के रूप में देखा जाता है , एक तैयार उपकरण नहीं है।