मैन्युअल रूप से '(।) के प्रकार का अनुमान कैसे लगाएं। (।)। (।) '?

Question

एडवर्ड Kmett की बात Lenses, Folds, and Traversals में, स्लाइड "पावर डॉट में है" पर, वह पता चलता (.) . (.) . (.) के प्रकार

(a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b

मैं GHCi में अपनी तरह दिखा कर इसे देख सकते हैं है। लेकिन मैं यह भी जानना चाहूंगा कि क्यों।

(.)    :: (a -> b) -> (c ->   a) -> c ->   b 
(.) . (.)  :: (a -> b) -> (c -> d ->  a) -> c -> d ->  b 
(.) . (.) . (.) :: (a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b 

पी.एस.: दूसरी बात मुझे समझ में करना चाहते हैं यही कारण है कि (.) से (.) . (.) और (.) . (.) . (.) के मापदंडों के नियमित परिवर्तन में पैटर्न है मैंने (.) . (.) की फ़ंक्शन परिभाषा का विस्तार करके (.) . (.) को हल करने का प्रयास किया। (.) की परिभाषा लागू करने के बाद मुझे मिल गया:

\x y z t -> x ((y z) t) 

तो मैं प्रकार निष्कर्ष निकाला:

x :: a -> b 
y :: c -> d -> a 
z :: c 
t :: d 

हालांकि मैं (.) . (.) . (.) पर खो गया। और मुझे नहीं पता कि यह मैन्युअल प्रकार अनुमान लगाने का सही तरीका है या नहीं।

Answer 1

कार्यों के साथ

,

instance Functor ((->) r) where 
    -- fmap :: (a -> b) -> f a -> f b 
    --   (a -> b) -> (r -> a) -> (r -> b) 
    fmap   p   q   x = p (q x) -- fmap = (.) 

तो क्या आप वास्तव में है fmap . fmap . fmap है:

fmap    :: (a -> b) -> f  a -> f  b 
fmap . fmap  :: (a -> b) -> f (g a) -> f (g b) 
fmap . fmap . fmap :: (a -> b) -> f (g (h a)) -> f (g (h b)) 

जो है

(a -> b) -> (c -> (d -> (e -> a))) -> (c -> (d -> (e -> b))) ~ 
(a -> b) -> (c -> d -> e -> a) -> (c -> d -> e -> b)  

fmap . fmap :: (a -> b) -> f (g a) -> f (g b) क्यों है? क्योंकि,

(fmap . fmap) foo = fmap (fmap foo) 
{- 
fmap   :: (a -> b) -> f a  -> f b 
foo    :: a -> b 
fmap foo  ::    f a  -> f b 
fmap foo  :: g a -> g b 
fmap (fmap foo) ::    f (g a) -> f (g b) 
-} 

यांत्रिक प्रकार व्युत्पत्ति सभी प्रतिस्थापन और प्रकार चर के अनुरूप नाम के बारे में है। और देखें उदा। here या here। पहले चारों ओर कोष्ठकों डॉट्स को कम:

((.) . (.) . (.)) f = (.) ((.) ((.) f)) 
        = (.) ((.) (f .)) 
        = (.) ((f .) .) 
        = ((f .) .) .) 

दूसरा शेष अभिव्यक्ति

((f .) .) .) g = ((f .) .) . g 
       = \x -> ((f .) .) (g x) 
       = \x -> (f .) . g x 
       = \x y -> (f .) (g x y) 
       = \x y -> f . g x y 
       = \x y z -> f (g x y z) 

को कम तो सबसे पहले आप n - 1 डॉट्स का उपयोग कर कोष्ठक में n डॉट्स रचना

Answer 2

(.) . (.) . (.) दो चरणों में कम कर देता है। फिर आप इस निर्माण को f :: a -> b और g पर काम करने के लिए लागू करते हैं और (...((f .) .) ... .) g प्राप्त करते हैं जहां प्रत्येक बिंदु g प्राप्त करता है कि तर्क है - यही कारण है कि एक पैटर्न है: प्रत्येक बिंदु कोष्ठक में g का एक तर्क संभालता है और आपको इस बिंदु को लिखने के लिए एक और बिंदु चाहिए सब पिछले सभी कटौती के बाद अभिव्यक्ति

\x1 x2 ... xn -> f (g x1 x2 ... xn) 

और इसका प्रकार स्पष्ट है।

---

एक अच्छी बात यह है कि अगर हम पोस्टफ़िक्स ऑपरेटरों के लिए होता है हम (कोड AGDA में है) ((f .) .) . g की लिख सकता है

open import Function renaming (_∘′_ to _∘_) using() 

_% = _∘_ 

postulate 
    a b c d e : Set 
    f : a -> b 
    g : c -> d -> e -> a 

fg : c -> d -> e -> b 
fg = f % % ∘ g 

बजाय है।