रैंकेंटाइप्स और चर्च अंक

Question

मैं संख्याओं को इस प्रकार का एक प्रकार देकर हास्केल में चर्च अंकों का अध्ययन करने की कोशिश कर रहा हूं, इस विचार के साथ कि प्राकृतिक संख्या n मूल रूप से अभिव्यक्ति है जो निम्न प्रकार के फ़ंक्शन को मान पर लागू करती है बार के लिए t टाइप करें।

zero :: Nat 
zero = \f t -> t 

succ :: Nat -> Nat 
succ n = \f -> f . (n f) 

plus :: Nat -> Nat -> Nat 
plus m n = \f -> (m f) . (n f) 

mult :: Nat -> Nat -> Nat 
mult m n = \f -> m (n f) -- Equal to \f -> (m . n) f 

-- Pointfree version 
mult' :: Nat -> Nat -> Nat 
mult' = (.) 

जब मैं घातांक परिभाषित करने की कोशिश, मैं एक ही तर्क लागू करने की कोशिश करना चाहते हैं:

type Nat = forall t. (t -> t) -> t -> t 

कि विचार के साथ

, मैं zero, successor, plus, mult निम्न तरीकों से परिभाषित कर सकते हैं जिसने मुझे गुणा को परिभाषित करने की अनुमति दी, अर्थात् mult mn बार 1 लागू करने की अनुमति दी।

यह निम्नलिखित कोड

exp' :: Nat -> Nat -> Nat 
exp' m n = n (mult m) (succ zero) 

की ओर जाता है लेकिन इस टाइप करता GHC से निम्न त्रुटि के साथ जांच:

Couldn't match type ‘t’ with ‘t1’ 
    ‘t’ is a rigid type variable bound by 
    the type signature for: 
     exp' :: forall t. Nat -> Nat -> (t -> t) -> t -> t 
    at church.lhs:44:3 
    ‘t1’ is a rigid type variable bound by 
    a type expected by the context: 
     forall t1. (t1 -> t1) -> t1 -> t1 
    at church.lhs:44:17 
    Expected type: ((t -> t) -> t -> t) -> (t -> t) -> t -> t 
    Actual type: Nat -> Nat 

त्रुटि कहना है कि typechecker के लिए प्रकार instantiating नहीं है लगता है n ठीक से, t टाइप करने के लिए अभिव्यक्ति के लिए अन्य 0 (t -> t) के साथ तत्काल टाइप किया जाना चाहिए।

क्या भी भ्रमित कर रहा है मैं हूँ कि निम्नलिखित कोड typechecks:

exp :: Nat -> Nat -> Nat 
exp m n = n ((.) m) (succ zero) -- replace mult by (.) 

कोई मन को समझा सकते हैं कि समस्या क्या यहाँ है? exp' की पहली परिभाषा टाइपशेक क्यों नहीं है लेकिन दूसरा exp टाइपशेक्स क्यों है?

धन्यवाद!

Answer 1

कारण यह काम नहीं करता है इसमें कई अपरिवर्तनीय तत्काल शामिल हैं, जिन्हें सामान्यतः हास्केल में भी अनुमति नहीं दी जाती है। क्योंकि mult' एक उच्च पद प्रकार है, भले ही यह definitionally (.) के बराबर है तो अलग ढंग से प्राप्त आय typechecking

{-# LANGUAGE ImpredicativeTypes #-} 

... 

exp' :: Nat -> Nat -> Nat 
exp' m n = n (mult m) (succ zero) 

दूसरे संस्करण typechecks,: यदि आप -XImpredicativeTypes चालू करते हैं, तो आप इसे संकलित करने के लिए मिल सकता है। चूंकि (.) का प्रकार सरल है (रैंक 1) टाइपशेकिंग अधिक बार सफल हो जाएगी।

जीएचसी दस्तावेज़ ImpredicativeTypes चेतावनी नहीं देता है इसलिए मैं इसका उपयोग करने के लिए सावधानी बरतता हूं।

newtype Nat' = N { instN :: Nat } 

exp'' :: Nat -> Nat -> Nat 
exp'' m n = instN $ n (\(N q) -> N $ mult m q) (N $ succC zero) 

---

कार्रवाई में impredicative इन्स्टेन्शियशन देखने के लिए, आपके द्वारा लिखे गए उपयोग कर सकते हैं छेद:

exp' :: Nat -> Nat -> Nat 
exp' m n = _ (mult m) (succC zero) 

इस प्रकार का रिपोर्ट करेंगे विशिष्ट तरीका एक newtype सरल उपयोग करने के लिए इस के चारों ओर पाने के लिए forall a . (Nat -> Nat) -> Nat -> (a -> a) -> a -> a, जो (Nat -> Nat) -> Nat -> Nat जैसा है।चूंकि आप वहां n डालते हैं, तो आपको forall a . (a -> a) -> a -> a के साथ इस प्रकार को एकजुट करना होगा, जिसमें पॉलीटाइप Nat के साथ टाइप वेरिएबल a को तुरंत चालू करना शामिल है।