हम डेटाटाइप को फ़ंक्शन के रूप में एन्कोड करने के लिए फ़ोल्डर्स का उपयोग क्यों करते हैं?

Question

या विशिष्ट होने के लिए, हम संख्याओं को एन्कोड करने के लिए सूचियों और पुनरावृत्ति को एन्कोड करने के लिए फ़ोल्डर का उपयोग क्यों करते हैं?

लंबे समय से परिचय के लिए खेद है, लेकिन मुझे वास्तव में उन चीज़ों का नाम कैसे देना है जिन्हें मैं पूछना चाहता हूं, इसलिए मुझे पहले कुछ एक्सपोज़िशन देना होगा। यह this C.A.McCann post से भारी रूप से आकर्षित करता है जो मेरी जिज्ञासा को पूरी तरह संतुष्ट नहीं करता है और मैं रैंक-एन-प्रकारों और अनंत आलसी चीजों के साथ मुद्दों को भी हाथ से रखूंगा।

---

एक तरह से काम करता है के रूप में डेटाटाइप्स एन्कोड करने के लिए एक "पैटर्न मिलान" समारोह है कि प्रत्येक मामले के लिए एक तर्क प्राप्त करता है बनाने के लिए है, प्रत्येक तर्क एक समारोह है कि मूल्यों कि निर्माता के लिए इसी और सभी तर्कों एक लौटा दिया प्राप्त करता जा रहा है परिणाम प्रकार।

यह सभी के रूप में गैर पुनरावर्ती प्रकार

--encoding data Bool = true | False 
type Bool r = r -> r -> r 

true :: Bool r 
true = \ct cf -> ct 

false :: Bool r 
false = \ct cf -> cf 

--encoding data Either a b = Left a | Right b 
type Either a b r = (a -> r) -> (b -> r) -> r 

left :: a -> Either a b r 
left x = \cl cr -> cl x 

right :: b -> Either a b r 
right y = \cl cr -> cr y 

हालांकि, पुनरावर्ती प्रकार के साथ नीचे पैटर्न मिलान टूट के साथ अच्छा सादृश्य के लिए उम्मीद बाहर काम करता है। हम जैसे

--encoding data Nat = Z | S Nat 
type RecNat r = r -> (RecNat -> r) -> r 
zero = \cz cs -> cz 
succ n = \cz cs -> cs n 

-- encoding data List a = Nil | Cons a (List a) 
type RecListType a r = r -> (a -> RecListType -> r) -> r 
nil = \cnil ccons -> cnil 
cons x xs = \cnil ccons -> ccons x xs 

कुछ करने के लिए परीक्षा हो सकती है, लेकिन हम हास्केल में उन पुनरावर्ती प्रकार परिभाषाएं नहीं लिख सकते हैं! सामान्य समाधान केवल पहले व्यक्ति (यानी, एक गुना/इटरेटर लिखना) की बजाय पुनरावृत्ति के सभी स्तरों पर लागू होने के लिए विपक्ष/succ मामले के कॉलबैक को लागू करना है। इस संस्करण में हम वापसी प्रकार r जहां पुनरावर्ती प्रकार होगा का उपयोग करें: इस संस्करण से काम करता है

--encoding data Nat = Z | S Nat 
type Nat r = r -> (r -> r) -> r 
zero = \cz cf -> cz 
succ n = \cz cf -> cf (n cz cf) 

-- encoding data List a = Nil | Cons a (List a) 
type recListType a r = r -> (a -> r -> r) -> r 
nil = \z f -> z 
cons x xs = \z f -> f x (xs z f) 

, यह बहुत कठिन कुछ कार्यों को परिभाषित करता है। उदाहरण के लिए, सूचियों के लिए "पूंछ" फ़ंक्शन या संख्याओं के लिए "पूर्ववर्ती" फ़ंक्शन लिखना मामूली है यदि आप पैटर्न मिलान का उपयोग कर सकते हैं लेकिन यदि आपको इसके बजाय फ़ोल्डरों का उपयोग करने की आवश्यकता है तो मुश्किल हो जाती है।

तो मेरा असली सवाल पर

:

1. हम कैसे सुनिश्चित करें कि परतों का उपयोग कर एन्कोडिंग काल्पनिक "एन्कोडिंग मिलान पैटर्न" के रूप में के रूप में शक्तिशाली है हो सकता है? क्या पैटर्न मिलान के माध्यम से मनमाने ढंग से कार्य परिभाषा लेने का कोई तरीका है और यांत्रिक रूप से इसके बजाय केवल फ़ोल्डरों का उपयोग करके इसे परिवर्तित कर सकते हैं? (यदि ऐसा है, तो यह कम जादुई के रूप में फ़ोल्डर के मामले में पूंछ या फोल्डल जैसी कठोर परिभाषाओं में मदद करेगा)

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

Answer 1

Scott encoding पर विकिपीडिया पृष्ठ कुछ उपयोगी अंतर्दृष्टि है। लघु संस्करण है, जो आप का जिक्र कर रहे हैं वह चर्च एन्कोडिंग है, और आपका "काल्पनिक पैटर्न-मिलान एन्कोडिंग" स्कॉट एन्कोडिंग है। दोनों चीजें करने के समझदार तरीके हैं, लेकिन चर्च एन्कोडिंग के लिए हल्का प्रकार की मशीनरी का उपयोग करना आवश्यक है (विशेष रूप से, इसे रिकर्सिव प्रकारों की आवश्यकता नहीं है)

सबूत है कि दोनों ईक हैं uivalent निम्नलिखित विचार का उपयोग करता है:

churchfold :: (a -> b -> b) -> b -> [a] -> b 
churchfold _ z [] = z 
churchfold f z (x:xs) = f x (churchfold f z xs) 

scottfold :: (a -> [a] -> b) -> b -> [a] -> b 
scottfold _ z [] = z 
scottfold f _ (x:xs) = f x xs 

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b 
scottFromChurch f z xs = fst (churchfold g (z, []) xs) 
where 
    g x ~(_, xs) = (f x xs, x : xs) 

विचार यह है कि जब से churchfold (:) [] सूची में पहचान है, तो एक चर्च गुना उस सूची तर्क यह दिया जाता है और साथ ही परिणाम यह उत्पादन करने के लिए माना जाता है का उत्पादन कर सकते हैं। फिर चेन x1 `f` (x2 `f` (... `f` xn) ...) में बाहरीतम f एक जोड़ी (y, x2 : ... : xn : []) प्राप्त करता है (कुछ y के लिए हमें परवाह नहीं है), इसलिए f x1 (x2 : ... : xn : []) लौटाता है। बेशक, इसे x1 : ... : xn : [] वापस करना होगा ताकि f के किसी और अनुप्रयोग भी काम कर सकें।

(यह वास्तव में "कमजोर" या प्रेरण के सामान्य सिद्धांत से strong (or complete) induction के गणितीय सिद्धांत के सबूत के समान ही है।

वैसे, Bool r प्रकार असली चर्च बूलियन के लिए थोड़ा बड़ा है - उदा। (+) :: Bool Integer, लेकिन (+) वास्तव में एक चर्च बूलियन नहीं है। यदि आप RankNTypes सक्षम करते हैं तो आप अधिक सटीक प्रकार का उपयोग कर सकते हैं: type Bool = forall r. r -> r -> r। अब इसे polymorphic होने के लिए मजबूर किया जाता है, इसलिए वास्तव में केवल दो होते हैं (seq और नीचे) निवासियों को अनदेखा करते हैं - \t _ -> t और \_ f -> f। इसी तरह के विचार आपके अन्य चर्च प्रकारों पर भी लागू होते हैं।

Answer 2

कुछ आगमनात्मक डेटा प्रकार को देखते हुए

data Nat = Succ Nat | Zero 

हम इस डेटा के हम कैसे पैटर्न मैच पर विचार कर सकते

case n of 
    Succ n' -> f n' 
    Zero -> g 

यह स्पष्ट है कि प्रकार Nat -> a के हर समारोह द्वारा परिभाषित किया जा सकता होना चाहिए उचित f और g दे रहा है और Nat (नीचे बार्सिंग) बनाने का एकमात्र तरीका दो सी में से एक का उपयोग कर रहा है onstructors।

---

संपादित करें: एक पल के लिए f के बारे में सोचें। हम उपयुक्त f और g देकर एक समारोह foo :: Nat -> a को परिभाषित कर रहे हैं ऐसी है कि f रिकर्सिवली foo कॉल की तुलना में हम फिर से परिभाषित कर सकते हैं f जैसे f' n' (foo n') कि f' पुनरावर्ती नहीं है। अगर a = (a',Nat) टाइप करें तो हम f' (foo n) लिख सकते हैं। तो, व्यापकता की हानि के बिना

foo n = h $ case n 
       Succ n' -> f (foo n) 
       Zero -> g 

इस सूत्रीकरण कि मेरी पोस्ट कर भावना के बाकी बनाता है:

---

तो, हम इस तरह एक "नाशक शब्दकोश आवेदन के रूप में मामले बयान के बारे में सोच सकते हैं "

data NatDict a = NatDict { 
    onSucc :: a -> a, 
    onZero :: a 
} 

अब से पहले से हमारे मामले बयान बन सकता है

h $ case n of 
     Succ n' -> onSucc (NatDict f g) n' 
     Zero -> onZero (NatDict f g) 

इस दिए गए हम

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a} 

प्राप्त कर सकते हैं हम तो दो कार्य

fromBB :: NatBB -> Nat 
fromBB n = cataNat n (NatDict Succ Zero) 

और

toBB :: Nat -> NatBB 
toBB Zero = Nat $ \dict -> onZero dict 
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict) 

हम इन दोनों कार्यों साबित कर सकते हैं परिभाषित कर सकते हैं एक समाकृतिकता गवाह कर रहे हैं (तेजी से और तर्क खोना) और इस प्रकार दिखाएं कि

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a) 

(जो सिर्फ NatBB के समान है) सिर्फ साबित करते हुए कि अंतर्निहित प्रकार से Nat

हम अन्य प्रकार के साथ एक ही निर्माण का उपयोग कर सकते हैं, और साबित होता है कि समारोह प्रकार जिसके परिणामस्वरूप हम क्या चाहते हैं के लिए है isomorphic बीजगणितीय तर्क (और प्रेरण) के साथ isomorphic हैं।

आपके दूसरे प्रश्न के अनुसार, हास्केल की टाइप सिस्टम आईएसओ-रिकर्सिव पर आधारित नहीं है जो इक्वि-रिकर्सिव प्रकार नहीं है। यह शायद सिद्धांत और प्रकार अनुमान को आईएसओ-रिकर्सिव प्रकारों के साथ काम करना आसान है, और उनके पास सभी शक्तियां हैं जो वे प्रोग्रामर भाग पर थोड़ा और काम लगाती हैं।मैं दावा करता है कि आप किसी भी भूमि के ऊपर

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r) 

लेकिन जाहिरा तौर पर GHCs अनुकूलक कभी कभी उन पर chokes :(बिना अपने इसो-पुनरावर्ती प्रकार प्राप्त कर सकते हैं पसंद है।