Data.Void.absurd कैसे ⊥ से अलग है?

Question

मैं आज Inverse of the absurd function पहले देखा था, और जब यह मेरे लिए स्पष्ट है कि drusba :: a -> Void के किसी भी संभावित कार्यान्वयन को समाप्त कभी नहीं होगा है, मुझे समझ नहीं आता क्यों एक ही absurd :: Void -> a का सच नहीं है (सभी के बाद, यह Void निर्माण करने के लिए असंभव है)। GHC कार्यान्वयन पर विचार करें:

newtype Void = Void Void 

absurd :: Void -> a 
absurd a = a `seq` spin a where 
    spin (Void b) = spin b 

spin, यह मेरे लिए, अंतहीन Void newtype रैपर की अनंत श्रृंखला को उजागर कर रहा है लगता है, और यहां तक ​​कि कभी वापस नहीं लेंगे, जब आप एक Void लगता है इसे पारित करने के सकता है। एक कार्यान्वयन कि पृथक किया जाएगा होगा कुछ की तरह:

absurd :: Void -> a 
absurd a = a `seq` undefined 

यह देखते हुए कि, क्यों हम कहते हैं कि absurd एक उचित समारोह Data.Void में रहने के लिए योग्य है कि है, लेकिन

drusba :: a -> Void 
drusba = undefined 

एक है फ़ंक्शन जिसे संभवतः परिभाषित नहीं किया जा सकता है? क्या यह निम्नलिखित की तरह कुछ है?

absurd कुल समारोह, जबकि drusba आंशिक है, (वास्तव में सभी) अपने डोमेन में आदानों कुछ के लिए नीचे परिणाम दे रहा है इसकी (खाली) डोमेन में किसी भी इनपुट के लिए एक गैर-नीचे परिणाम दे रही है।

Answer 1

Data.Voidvoid पैकेज से base से (जीएचसी 7.10) में base से स्थानांतरित हो गया। यदि आप void के लिए कैबल फ़ाइल देखते हैं तो आप देखेंगे कि इसमें केवल Data.Void पुराने base संस्करणों के लिए शामिल है। Now, Void is defined as chi suggests:

data Void 

absurd :: Void -> a 
absurd a = case a of {} 

जो पूरी तरह से मान्य है।

---

मुझे लगता है कि पुराने परिभाषा के पीछे विचार यह कुछ इस तरह है:

, प्रकार

data BadVoid = BadVoid BadVoid 

इस प्रकार का काम नहीं किया हो जाता है पर विचार करें, क्योंकि यह परिभाषित करने के लिए वास्तव में संभव है उस प्रकार के साथ एक गैर नीचे (coinductive) मूल्य:

badVoid = BadVoid badVoid 

हम से है कि इस समस्या को ठीक कर सकते हैं एक कठोरता एनोटेशन, जो (कम से कम एक तरह से) प्रकार बलों का उपयोग कर आगमनात्मक होने के लिए:

data Void = Void !Void 

मान्यताओं कि या वास्तव में पकड़ नहीं हो सकता है के तहत, लेकिन कम से कम नैतिक रूप से पकड़, हम वैध तरीके से किसी भी आगमनात्मक पर प्रेरण प्रदर्शन कर सकते हैं प्रकार। तो

spin (Void x) = spin x 

हमेशा करता है, तो समाप्त हो जाएगी, परिकल्पित है, हम प्रकार Void के लिए कुछ है।

अंतिम चरण newtype साथ एकल सख्त-निर्माता डेटाप्रकार जगह है:

newtype Void = Void Void 

यह हमेशा वैध है। spin की परिभाषा, तथापि, क्योंकि data और newtype के बीच अलग अलग पैटर्न मिलान अर्थ विज्ञान के अर्थ बदल गया है। अर्थ ठीक, spin शायद

spin !x = case x of Void x' -> spin x' 

(spin !(Void x) परहेज newtype निर्माणकर्ता और धमाके पैटर्न के बीच बातचीत में एक अब निश्चित बग स्कर्ट लिए लिखा गया है चाहिए संरक्षित करने के लिए, लेकिन GHC 7.10 के लिए (हेक्टेयर) इस फार्म नहीं करता है! 'टी वास्तव में वांछित त्रुटि संदेश है क्योंकि यह जो बिंदु absurd = spin पर एक अनंत लूप में "अनुकूलित" है) का उत्पादन।

शुक्र है, यह वास्तव में, अंत में कोई फर्क नहीं पड़ता क्योंकि पूरे वर्ष परिभाषा एक मूर्खतापूर्ण व्यायाम का एक सा है।

Answer 2

ऐतिहासिक कारणों से, किसी भी हास्केल डेटा (newtype सहित) प्रकार कम से कम एक निर्माता होना आवश्यक है।

इसलिए, "Haskell98" में Void को परिभाषित करने के लिए किसी को टाइप-स्तरीय रिकर्सन newtype Void = Void Void पर भरोसा करने की आवश्यकता है। इस प्रकार का कोई (गैर-नीचे) मान नहीं है।

absurd फ़ंक्शन को Void प्रकार के "अजीब" रूप से निपटने के लिए (मान स्तर) रिकर्सन पर भरोसा करना है।

कुछ जीएचसी एक्सटेंशन के साथ, अधिक आधुनिक हास्केल में, हम एक शून्य कन्स्ट्रक्टर डेटा प्रकार को परिभाषित कर सकते हैं, जो एक सैनर परिभाषा का कारण बनता है।

{-# LANGUAGE EmptyDataDecls, EmptyCase #-} 
data Void 
absurd :: Void -> a 
absurd x = case x of { } -- empty case 

मामले संपूर्ण है - यह Void के सभी निर्माताओं, उन सभी को शून्य संभाल करता है। इसलिए यह कुल है।

एग्डा या कोक जैसी कुछ अन्य कार्यात्मक भाषाओं में, ऊपर दिए गए मामले का एक संस्करण Void जैसे खाली प्रकारों से निपटने पर बेवकूफ है।