agda - टाइपसीज़ एक बुरी चीज क्यों है?




dependent-type idris (2)

Agda में, आप Set पर मिलान को पैटर्न नहीं कर सकते क्योंकि यह एक प्रेरक प्रकार नहीं है।

Agda और Idris दोनों ही प्रकार के मूल्यों पर प्रभावी रूप से मेल खाने वाले पैटर्न को प्रतिबंधित करते हैं। ऐसा लगता है कि अगाडा हमेशा पहले मामले पर मेल खाता है, जबकि इदरीस केवल एक त्रुटि फेंकता है।

तो, क्यों typeecase एक बुरी बात है? क्या यह निरंतरता को तोड़ता है? मैं विषय के बारे में अधिक जानकारी नहीं पा सका हूं।


कई लोग प्रकारों पर मिलान को बुरा मानते हैं क्योंकि यह प्रकारों के लिए पैरामीट्रिकिटी को तोड़ता है।

प्रकारों के लिए पैरामीट्रिकिटी वाली भाषा में, जब आप एक चर देखते हैं

f : forall a . a -> a

आप तुरंत f के संभावित मूल्यों के बारे में बहुत कुछ जानते हैं। सहज रूप से: f चूंकि एक फ़ंक्शन है, इसे लिखा जा सकता है:

f x = body

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

अब यदि f टाइप a पर मेल कर सकता है, तो f कई और कार्यान्वयन संभव हैं। इसलिए हम शक्तिशाली प्रमेय खो देंगे।