हास्केल प्रोग्रामिंग में मोनाद बनाम श्रेणी सिद्धांत में मोनाद
मेरे पास गणित में हास्केल प्रोग्रामिंग और श्रेणी सिद्धांत में उपयोग किए जाने वाले मोनाड की अवधारणा के बारे में एक प्रश्न है।
याद रखें हास्केल में एक मोनाड में निम्नलिखित घटक होते हैं:
एक प्रकार का कंस्ट्रक्टर जो प्रत्येक अंतर्निहित प्रकार के लिए परिभाषित करता है कि संबंधित मोनड प्रकार कैसे प्राप्त किया जाए। इस प्रकार के निर्माता का नाम अक्सर पूरे मोनाड के साथ समानार्थक रूप से उपयोग किया जाता है। अगर$M$ संन्यासी का नाम है और $t$ फिर मनमाना निश्चित डेटा प्रकार है $M t$ इसी प्रकार का विचित्र है
एक इकाई फ़ंक्शन जो संबंधित प्रकार के मूल्य को संबंधित मोनड प्रकार के मूल्य पर मैप करता है। परिणाम उसी प्रकार का "सरलतम" मूल्य है जो मूल मूल्य से प्राप्त किया जा सकता है। हास्केल में इस फ़ंक्शन को रिटर्न कहा जाता है। यूनिट फ़ंक्शन में बहुरूपी प्रकार होता है$t → M t$
कम से कम एक और ऑपरेशन, जो मोनैडिक ऑपरेशन के संयोजन का वर्णन करता है।
श्रेणी सिद्धांत में दूसरी ओर एक मोनाड ट्रिपल है $(T, \eta, \mu)$ एक श्रेणी का $C$ कहाँ पे
$T: C \to C$ एक फ़नकार है
$\eta: 1_K \to T$ श्रेणी सिद्धांत के अर्थ में एक प्राकृतिक परिवर्तन
$\mu: T^2 \to T$ एक प्राकृतिक परिवर्तन
और इन वस्तुओं को निम्नलिखित आरेखों को संतुष्ट करना चाहिए: https://en.wikipedia.org/wiki/Monad_(category_theory)
प्रश्न: हास्केल और अमूर्त श्रेणी के सिद्धांत से ये कैसे संबंधित हैं? क्या हास्केल में मोनाड संरचना में श्रेणी सिद्धांत के अर्थ में प्राकृतिक "मोनाड संरचना" है, अर्थात हम कैनोनिकली सहयोगी हो सकते हैं$M$ जैसा कि ऊपर वर्णित एक विहित ट्रिपल?
जवाब
हास्केल में एक मोनड का उद्देश्य प्रकारों की श्रेणी में एक मोनाड होना है, जब श्रेणी सिद्धांत आंतरिक रूप से टाइप सिद्धांत के लिए किया जाता है। हास्केल और समान भाषाओं की क्षमताएं कुछ हद तक सीमित हैं, इसलिए श्रेणी सिद्धांत में बहुत सारे बुनियादी निर्माण हैं जो नहीं किए जा सकते हैं, लेकिन बहुत सारी संरचनाएं हैं जो यथोचित रूप से एन्कोड की जा सकती हैं।
M :: * → *फ़नकार की ऑब्जेक्ट मैपिंग है, जिसे आपने नाम दिया है $T$ बाद में।- फ़नकार का तीर मानचित्रण भाग द्वारा दिया जाता है fmap
- $η$यूनिट फ़ंक्शन है, जिसे हास्केल कहते हैं return(या pure, जो थोड़ा अधिक सामान्य है)
- $μ$द्वारा दिया गया है join।
Monadउदाहरणों से अपेक्षित अपेक्षाएं श्रेणी सिद्धांत में एक साधु होने के बराबर हैं।
अनिवार्य रूप से, यह विशेष रूप से श्रेणी के साधुओं के बारे में बोलने से बहुत अलग नहीं है $\mathsf{Set}$, हास्केल / आदि के पहले उल्लेख से अलग है। थ्योरी सेट करने वाले कुछ निर्माण गायब हैं (ऐसी चीजें हैं जो (सह) उत्पादों की तरह पर्याप्त कार्य करती हैं, लेकिन पुलबैक / पुशआउट्स की तरह नहीं)। आप भिक्षुओं के बारे में बहुत कुछ सोच सकते हैं$\mathsf{Set}$, क्योंकि अमूर्त / सार्वभौमिक बीजगणित में कई संरचनाएं एक को जन्म देती हैं, और इस तरह प्रस्तुत करने योग्य हैं।
हो सकता है कि विभिन्न प्रोग्रामिंग भाषाओं में टाइप करने से कोई तकनीकी रूप से अच्छे गुणों / संरचना के साथ एक श्रेणी न बना ले, लेकिन आप इसके बजाय यह सोच सकते हैं कि आप उनका उपयोग कुछ बेहतर व्यवहार करने वाली प्रणाली के बारे में बात करने के लिए कर रहे हैं। $F_ω$, और यह वास्तव में एक दिलचस्प तरीके से जवाब नहीं बदलेगा।