5
विकिपीडिया में, bottom type को "उस प्रकार के रूप में परिभाषित किया गया है जिसका कोई मूल्य नहीं है"। हालांकि, अगर b यह खाली प्रकार है, तो उत्पाद प्रकार (b,b) कोई मूल्य नहीं है, लेकिन b से अलग लगता है। मैं सहमत हूं कि नीचे निर्वासित है, लेकिन मुझे नहीं लगता कि यह संपत्ति इसे परिभाषित करने के लिए पर्याप्त है।नीचे का प्रकार क्या है?
Curry-Howard correspondence तक, नीचे गणितीय झूठीता से जुड़ा हुआ है। अब एक तार्किक सिद्धांत है जिसमें कहा गया है कि झूठी से किसी भी प्रस्ताव का पालन किया जाता है। करी-हावर्ड द्वारा, इसका मतलब है कि forall a. bottom -> a टाइप किया गया है, यानि f :: forall a. bottom -> a फ़ंक्शंस का एक परिवार मौजूद है।
f क्या कार्य हैं? क्या वे नीचे परिभाषित करने में मदद करते हैं, शायद सभी प्रकार के अनंत उत्पाद ?
मैं प्रोपोज़िशनल पथरी में सूत्रों के 3 प्रकार देखते हैं। 1) Tautologies, जो एक हेटिंग बीजगणित में हर व्याख्या में सच हैं। 2) सूत्र जो अस्वीकार हैं, वे हर हेटिंग व्याख्याओं में झूठे हैं। 3) सूत्र जो मूल्य व्याख्या पर निर्भर करते हैं। करी-हॉवर्ड मामलों 2 और 3 दोनों खाली प्रकार के अनुरूप हैं। हालांकि मुझे लगता है कि खाली मामले के बीच 2 मामले को अलग किया जाना चाहिए: केवल उन प्रकारों को नीचे बुलाया जाना चाहिए। –