क्या कोई चीज़ "सेमी-मोनैड" या "काउंटर-मोनड" कहती है?

Question

ठीक है, मैं हास्केल मोनाड्स का अध्ययन कर रहा हूं। जब मैंने विकीबूक Category theory आलेख पढ़ा, तो मैंने पाया कि मोनैड मॉर्फिज़्म का हस्ताक्षर तर्क में tautologies की तरह दिखता है, लेकिन आपको M a से ~~A में कनवर्ट करने की आवश्यकता है, यहां ~ तर्क अस्वीकृति है।

return :: a -> M a -- Map to tautology A => ~~A, double negation introduction 
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B 

अन्य कार्यों को भी tautologies है:

fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B) 
join :: M (M a) -> M a -- Map to ~~(~~A) => ~~A 

यह भी समझ में आ जाता है कि तथ्य यह है कि सामान्य कार्यात्मक भाषाओं के Curry-Howard पत्राचार सहज ज्ञान युक्त तर्क, नहीं शास्त्रीय तर्क है, इसलिए हम उम्मीद नहीं कर सकते के अनुसार ~~A => A जैसे टॉटोलॉजी में पत्राचार हो सकता है।

लेकिन मैं कुछ और सोच रहा हूं। क्यों मोनाड केवल दोहरी निषेध से संबंधित हो सकता है? एकल अस्वीकृति का पत्राचार क्या है? यह मैं निम्नलिखित वर्ग परिभाषा के लिए नेतृत्व:

class Nomad n where 
    rfmap :: (a -> b) -> n b -> n a 
    dneg :: a -> n (n a) 

return :: Nomad n => a -> n (n a) 
return = dneg 
(>>=) :: Nomad n => n (n a) -> (a -> n (n b)) -> n (n b) 
x >>= f = rfmap dneg $ rfmap (rfmap f) x 

यहाँ मैं एक अवधारणा "नोमैड" कहा जाता है परिभाषित है, और यह दो आपरेशन (दोनों सहज ज्ञान युक्त तर्क में एक तर्क स्वयंसिद्ध से संबंधित) का समर्थन करता है। "Rfmap" नाम का ध्यान दें, इसका अर्थ यह है कि इसका हस्ताक्षर फ़ैक्टर के fmap के समान है, लेकिन परिणामस्वरूप a और b के क्रम में उलट दिया गया है। अब मैं उनके साथ मोनाड ऑपरेशंस को फिर से परिभाषित कर सकता हूं, M a से n (n a) को प्रतिस्थापित कर सकता हूं।

तो अब सवाल प्रश्न पर जाएं। तथ्य यह है कि मोनाद श्रेणी सिद्धांत से अवधारणा का मतलब है कि मेरा "नोमाड" एक श्रेणी सिद्धांत अवधारणा भी है। तो यह क्या है? क्या यह उपयोगी है? क्या इस विषय में कोई कागजात या शोध परिणाम मौजूद हैं?

Answer 1

डबल निषेध एक विशेष इकाई

data Void --no constructor because it is uninhabited 

newtype DN a = DN {runDN :: (a -> Void) -> Void} 

instance Monad DN where 
    return x = DN $ \f -> f x 
    m >>= k = DN $ \c -> runDN m (\a -> runDN (k a) c)) 

वास्तव में है, यह एक अधिक सामान्य इकाई

type DN = Cont Void 
newtype Cont r a = Cont {runCont :: (a -> r) -> r} 

जो निरंतरता पारित करने के लिए इकाई है का एक उदाहरण है।

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

(a -> b) -> f b -> f a 

एक विधि अच्छी तरह से करने के लिए श्रेणी के सिद्धांत में जाना जाता है के हस्ताक्षर, contravariant functor है। यह अनिवार्य रूप से वही कानूनों का पालन करता है जैसे कि फैनक्टर (संरक्षित (सह) संरचना और पहचान)। दरअसल, एक contravariant मज़ेदार विरोधी वर्ग के लिए बिल्कुल एक मजेदार है।चूंकि हम "हैकेल फ़ैक्टर" में रुचि रखते हैं, जो एंडो-फ़ैक्टर के रूप में माना जाता है, हम देख सकते हैं कि "हैकेल contravariant functor" एक मजेदार Hask -> Hask_Op है।

दूसरी ओर, क्या

a -> f (f a) 

के बारे में क्या कानून इस होना चाहिए? मेरे पास एक सुझाव है। श्रेणी सिद्धांत में, Functors के बीच मानचित्र करना संभव है। श्रेणी D के लिए श्रेणी C से F, G प्रत्येक से दो functors को देखते हुए, F से एक प्राकृतिक परिवर्तनG को D

forall a. F a -> G a 

में एक आकारिता कि कुछ जुटना कानूनों का अनुसरण करता है है। आप "ट्रांसक्टर श्रेणी" को परिभाषित करने के लिए उनका उपयोग करके प्राकृतिक परिवर्तनों के साथ बहुत कुछ कर सकते हैं। लेकिन, क्लासिक मजाक (मैक लेन के कारण) यह है कि श्रेणियों का आविष्कार करने वालों के बारे में बात करने के लिए आविष्कार किया गया था, मज़ेदारों का आविष्कार प्राकृतिक परिवर्तनों के बारे में बात करने के लिए किया गया था, और प्राकृतिक परिवर्तनों का आविष्कार निर्धारण के बारे में बात करने के लिए किया गया था।

एक functor F : D -> C और एक functor G : C -> D रूप C से D के लिए एक adjunction अगर वहाँ दो प्राकृतिक परिवर्तनों मौजूद

unit : Id -> G . F 
counit : F . G -> Id 

एक adjunction के इस विचार को monads को समझने का एक लगातार तरीका है। प्रत्येक जुड़ाव पूरी तरह से प्राकृतिक तरीके से एक मोनड को जन्म देता है। यही कारण है कि, इन दो मकसदों की संरचना एक एंडोफंक्टर है, और आपके पास वापस लौटने के समान कुछ है (इकाई), आपको बस शामिल होना चाहिए। लेकिन यह आसान है, जुड़ें केवल एक समारोह G . F . G . F -> G . F है जिसे आप केवल "मध्य में" देश का उपयोग करके प्राप्त करते हैं।

तो, तो यह सब के साथ, आप क्या देख रहे हैं? खैर

dneg :: a -> n (n a) 

वास्तव में खुद के साथ एक contravariant functor की adjunction के unit तरह दिखता है। इसलिए, आपके Nomad प्रकार की संभावना है (निश्चित रूप से यदि इसका उपयोग मोनैड बनाने के लिए सही है) ठीक उसी तरह "एक contravariant functor जो स्वयं adjoint है।" स्वयं के आस-पास के मकसदों की खोज करने से आपको दोबारा नकारात्मकता और निरंतरता मिल जाएगी ... जो हमने शुरू किया था!

---

संपादित करें: लगभग निश्चित रूप से ऊपर दिए गए तीरों में से कुछ पीछे हैं। हालांकि, मूल विचार सही है। आप इसे नीचे प्रशंसा पत्र का उपयोग कर बाहर अपने आप को काम कर सकते हैं:

पर श्रेणी सिद्धांत सबसे अच्छा पुस्तकों शायद कर रहे हैं,

• स्टीव एवोडे, श्रेणी थ्योरी
• सैंडर्स मैक लेन, कार्य गणितज्ञ के लिए श्रेणियाँ

हालांकि कई और अधिक सुलभ परिचय किताबें कंप्यूटर scie के लिए श्रेणी थ्योरी पर बेंजामिन Pierces पुस्तक सहित मौजूद हैं ntists।

वीडियो Oregon Programming Language Summer School

Catsters यूट्यूब, indexed here पर कम व्याख्यान से भाषण स्टीव एवोडे द्वारा ऑनलाइन

• श्रेणी थ्योरी व्याख्यान, adjunctions पर वीडियो पर विशेष ध्यान दें

एक कागजात की संख्या निरंतरता मोनाड पर अनुलग्नक कोण का पता लगाएं, उदाहरण के लिए

• Hayo Thielecke, निरंतरता शब्दार्थ और स्व adjointness

खोज शब्द "आत्म adjoint", "निरंतरता", और "इकाई" अच्छे हैं। इसके अलावा, कई मुद्दों ने इन मुद्दों के बारे में लिखा है। यदि आप "मोनैड्स कहां से आते हैं" Google पर आपको ngfpe से this one या this one से उपयोगी परिणाम मिलते हैं। कॉमोनैड रीडर के लिए भी Sjoerd Vissche की link।

Answer 2

यह एक स्व-सहायक contravariant Functor होगा। rfmap contravariant functor भाग प्रदान करता है, और dneg अनुलग्नक की इकाई और देश है।

Op r एक उदाहरण है, जो निरंतरता मोनाड बनाता है। कुछ कोड के लिए http://hackage.haskell.org/package/adjunctions में contravariant मॉड्यूल देखें।

आपको http://comonad.com/reader/2011/monads-from-comonads/ पढ़ना चाहिए, जो संबंधित और बहुत रोचक है।