haskell - आश्रित प्रकार: निर्भर जोड़ी प्रकार एक विवाद संघ के समान कैसे है?




agda dependent-type (4)

मैं आश्रित प्रकार का अध्ययन कर रहा हूं और मैं निम्नलिखित समझता हूं:

  1. सार्वभौमिक मात्रा को एक निर्भर कार्य प्रकार के रूप में क्यों दर्शाया जाता है। ∀(x:A).B(x) अर्थ है "सभी प्रकार के x के लिए A प्रकार B(x) का मान है" । इसलिए इसे एक फ़ंक्शन के रूप में दर्शाया जाता है, जब टाइप A किसी भी मान x को दिए गए प्रकार B(x) का मान देता है।
  2. क्यों मौजूद मात्रात्मक मात्रा को एक निर्भर जोड़ी प्रकार के रूप में दर्शाया जाता है। ∃(x:A).B(x) अर्थ है "टाइप A का एक x मौजूद है जिसके लिए B(x) प्रकार का मान है । इसलिए इसे एक जोड़ी के रूप में दर्शाया जाता है जिसका पहला तत्व टाइप A का एक विशेष मान x है और जिसका दूसरा तत्व प्रकार B(x) का मान है।

इसके अलावा: यह भी दिलचस्प है कि सार्वभौमिक मात्रा हमेशा भौतिक निहितार्थ के साथ प्रयोग की जाती है जबकि अस्तित्वत्मक मात्रा हमेशा लॉजिकल संयोजन के साथ प्रयोग की जाती है।

वैसे भी, निर्भर प्रकारों पर विकिपीडिया लेख कहता है कि:

आश्रित प्रकार के विपरीत निर्भर जोड़ी प्रकार , निर्भर योग प्रकार या सिग्मा-प्रकार है । यह तांबे या विघटन संघ के समान है।

यह कैसे है कि एक जोड़ी प्रकार (जो आमतौर पर एक उत्पाद प्रकार है) एक विवाद संघ के समान है (जो एक योग प्रकार है)? यह हमेशा मुझे भ्रमित कर दिया है।

इसके अलावा, आश्रित कार्य प्रकार उत्पाद प्रकार के समान कैसे है?


अच्छा प्रश्न। यह नाम मार्टिन-लोफ से निकला था, जिसने पीआई प्रकार के लिए "सेट के परिवार के कार्टेशियन उत्पाद" शब्द का उपयोग किया था। निम्नलिखित नोट्स देखें, उदाहरण के लिए: http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf बिंदु तब होता है जब एक पीआई प्रकार सिद्धांत रूप में होता है एक घातीय के लिए, आप हमेशा एन-आरी उत्पाद के रूप में घातीय दिखाई दे सकते हैं जहां n एक्सपोनेंट है। अधिक ठोस रूप से, गैर-निर्भर कार्य ए -> बी को घातीय प्रकार बी ^ ए या एक अनंत उत्पाद पीआई_ {ए इन ए} बी = बी एक्स बी एक्स बी एक्स ... एक्स बी (एक बार) के रूप में देखा जा सकता है। एक आश्रित उत्पाद इस अर्थ में संभावित रूप से अनंत उत्पाद Pi_ {ए में ए} बी (ए) = बी (ए_1) एक्स बी (ए 2) x ... x बी (a_n) (एक बार में प्रत्येक a_i के लिए) है।

निर्भर राशि के लिए तर्क समान हो सकता है, क्योंकि आप एक उत्पाद को एन-आरी योग के रूप में देख सकते हैं जहां n उत्पाद के कारकों में से एक है।


एक आश्रित जोड़ी एक प्रकार के साथ टाइप की जाती है और उस प्रकार के मानों से किसी अन्य प्रकार के फ़ंक्शन को टाइप किया जाता है। आश्रित जोड़ी के पहले प्रकार के मूल्य के जोड़े के मूल्य और पहले मान पर लागू दूसरे प्रकार का मान होता है।

data Sg (S : Set) (T : S -> Set) : Set where
  Ex : (s : S) -> T s -> Sg S T

हम सिग्मा प्रकार के रूप में कैनोनिक रूप से व्यक्त किए जाने के तरीके को दिखाकर योग प्रकारों को पुनः प्राप्त कर सकते हैं: यह केवल Sg Bool (choice ab) जहां

choice : a -> a -> Bool -> a
choice l r True  = l
choice l r False = r

बूलियन के कैनोलिक एलिमिनेटर है।

eitherIsSg : {a b : Set} -> Either a b -> Sg Bool (choice a b)
eitherIsSg (Left  a) = Sg True  a
eitherIsSg (Right b) = Sg False b

sgIsEither : {a b : Set} -> Sg Bool (choice a b) -> Either a b
sgIsEither (Sg True  a) = Left  a
sgIsEither (Sg False b) = Right b

भ्रम एक Σ प्रकार की संरचना के लिए समान शब्दावली का उपयोग करने से उत्पन्न होता है और इसके मूल्य कैसा दिखते हैं।

Σ (x: ए) बी (x) का मान एक जोड़ी (ए, बी) है जहां एएए और बीबीबी (ए) । दूसरे तत्व का प्रकार पहले के मान पर निर्भर करता है।

यदि हम Σ (x: ए) बी (एक्स) की संरचना को देखते हैं, तो यह सभी संभावित x∈A के लिए बी (एक्स) का एक पृथक संघ (coproduct) है।

यदि बी (एक्स) स्थिर है ( एक्स से स्वतंत्र) तो Σ (x: ए) बी बस होगा | ए | बी की प्रतियां, वह एबीबी (2 प्रकार का उत्पाद) है।

यदि हम Π (x: ए) बी (x) की संरचना को देखते हैं, तो यह सभी संभावित x∈A के लिए बी (x) का उत्पाद है। इसके मूल्यों को | ए | के रूप में देखा जा सकता है -उपल्स जहां एक- वें घटक प्रकार बी (ए) है

यदि बी (एक्स) निरंतर ( एक्स से स्वतंत्र) है तो Π (x: ए) बी केवल ए → बी होगा - से बी के कार्य, जो सेट-सिद्धांत नोटेशन का उपयोग करके बीए ( बी से ) है - उत्पाद का | ए | बी की प्रतियां

तो Σ (x∈A) बी (एक्स) एक | ए | है - ए के तत्वों द्वारा अनुक्रमित प्रतिलिपि, जबकि Π (x∈A) बी (एक्स) एक | ए | ए के तत्वों द्वारा अनुक्रमित उत्पाद।


यह इस बिंदु पर अन्य उत्तरों के साथ शायद अनावश्यक है, लेकिन यहां इस मुद्दे का मूल है:

यह कैसे है कि एक जोड़ी प्रकार (जो आमतौर पर एक उत्पाद प्रकार है) एक विवाद संघ के समान है (जो एक योग प्रकार है)? यह हमेशा मुझे भ्रमित कर दिया है।

लेकिन एक उत्पाद क्या है लेकिन बराबर संख्याओं का योग है? उदाहरण के लिए 4 × 3 = 3 + 3 + 3 + 3।

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







curry-howard