हैकेल

Question

में चर्च अंकों का घटाव मैं हास्केल में चर्च अंकों को लागू करने का प्रयास कर रहा हूं, लेकिन मैंने मामूली समस्या को मारा है। हास्केल

साथ एक अनंत प्रकार की शिकायत होती है जांच: अनंत प्रकार का निर्माण नहीं कर सकते हैं: टी = (टी -> t1) - जब मैं कोशिश करते हैं और घटाव करना> t2

-> (t1 -> t2)। मैं 99% सकारात्मक हूं कि मेरा लैम्ब्डा कैलकुस मान्य है (हालांकि यदि यह नहीं है, तो कृपया मुझे बताएं)। मैं क्या जानना चाहता हूं, यह है कि क्या मेरे काम के साथ हैकेल काम करने के लिए मैं कुछ भी कर सकता हूं।

module Church where 

type (Church a) = ((a -> a) -> (a -> a)) 

makeChurch :: Int -> (Church a) 
makeChurch 0 = \f -> \x -> x 
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x) 

numChurch x = (x succ) 0 

showChurch x = show $ numChurch x 

succChurch = \n -> \f -> \x -> f (n f x) 

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1 

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1) 

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u) 

subChurch = \m -> \n -> (n predChurch) m 

Answer 1

केवल untyped संस्करण में predChurchdoesn't work in simply typed lambda calculus की यह परिभाषा,। आप predChurch का एक संस्करण पा सकते हैं जो Haskell here में काम करता है।

Answer 2

समस्या यह है कि predChurchभी पॉलीमोर्फिक हिंडली-मिलनर प्रकार अनुमान द्वारा सही ढंग से अनुमानित होने के लिए है। उदाहरण के लिए, यह लिखने के लिए प्रलोभन है:

predChurch :: Church a -> Church a 
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u) 

लेकिन यह प्रकार सही नहीं है। Church a इसकी पहली तर्क a -> a के रूप में लेता है, लेकिन आप n को दो तर्क फ़ंक्शन पास कर रहे हैं, स्पष्ट रूप से एक प्रकार की त्रुटि।

समस्या यह है कि Church a सही ढंग से चर्च संख्या का वर्णन नहीं करता है। एक चर्च संख्या केवल एक संख्या का प्रतिनिधित्व करती है - उस प्रकार पैरामीटर का अर्थ पृथ्वी पर क्या हो सकता है? उदाहरण के लिए:

foo :: Church Int 
foo f x = f x `mod` 42 

कि typechecks, लेकिन foo सबसे निश्चित रूप से नहीं एक चर्च अंक है। हमें इस प्रकार को प्रतिबंधित करने की आवश्यकता है। चर्च अंकों को किसी भीa, केवल एक विशिष्ट a के लिए काम करने की आवश्यकता नहीं है। सही परिभाषा है:

type Church = forall a. (a -> a) -> (a -> a) 

आप इस तरह सक्षम करने के लिए फ़ाइल के शीर्ष पर {-# LANGUAGE RankNTypes #-} की आवश्यकता है।

predChurch :: Church -> Church 
-- same as before 

आप क्योंकि उच्च रैंक प्रकार Hindley-मिलनर द्वारा inferrable नहीं कर रहे हैं यहाँ एक प्रकार हस्ताक्षर देना चाहिए:

अब हम प्रकार हस्ताक्षर हम उम्मीद करते हैं दे सकते हैं।

हालांकि, जब हम subChurch एक और समस्या को लागू करने के लिए जाना उठता है:

Couldn't match expected type `Church' 
     against inferred type `(a -> a) -> a -> a' 

मैं नहीं 100% यकीन है कि ऐसा क्यों होता हूँ, मुझे लगता है कि forall भी उदारतापूर्वक typechecker से सामने आया जा रहा है। हालांकि मुझे आश्चर्य नहीं है; एक कंपाइलर को मौजूद कठिनाइयों के कारण उच्च रैंक प्रकार थोड़ा भंगुर हो सकते हैं।इसके अलावा, हमें का उपयोग अबास्ट्रक्शन के लिए नहीं करना चाहिए, हमें newtype का उपयोग करना चाहिए (जो हमें परिभाषा में अधिक लचीलापन देता है, कंपाइलर के साथ कंपाइलर की सहायता करता है, और उन स्थानों को चिह्नित करता है जहां हम अमूर्तता के कार्यान्वयन का उपयोग करते हैं) :

: subChurch साथ

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u) 

ही:

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) } 

और हम रोल और आवश्यक के रूप में उतारना करने के लिए predChurch को संशोधित करना

subChurch = \m -> \n -> unChurch n predChurch m 

लेकिन हमें अब टाइप हस्ताक्षर की आवश्यकता नहीं है - रोल/अनोल को फिर से अनुमानित प्रकारों में पर्याप्त जानकारी है।

मैं हमेशा एक नया अमूर्त बनाते समय newtype एस की अनुशंसा करता हूं। नियमित type समानार्थी मेरे कोड में बहुत दुर्लभ हैं।

Answer 3

मुझे एक ही समस्या का सामना करना पड़ा है। और मैंने टाइप हस्ताक्षर जोड़ने के बिना इसे हल किया।

conscarSICP से कॉपी किया गया समाधान के साथ यहां समाधान है।

cons x y = \m -> m x y 
car z = z (\p q -> p) 
cdr z = z (\p q -> q) 

next z = cons (cdr z) (succ (cdr z)) 
pred n = car $ n next (cons undefined zero) 

sub m n = n pred m 

आप पूर्ण स्रोत here पा सकते हैं।

मैं sub m n = n pred m लिखने के बाद वास्तव में आश्चर्यचकित हूं, और इसे बिना किसी प्रकार की त्रुटि के ghci में लोड कर रहा हूं!

हास्केल कोड इतना संक्षिप्त है! :-)