पुनरावर्ती रूप से परिभाषित उदाहरण और बाधा

Question

मैं वैक्टर और मैट्रिस के साथ खेल रहा हूं जहां आकार DataKinds एक्सटेंशन का उपयोग करके उनके प्रकार में एन्कोड किया गया है। यह मूल रूप से इस प्रकार है:

data Nat = Zero | Succ Nat 

data Vector :: Nat -> * -> * where 
    VNil :: Vector Zero a 
    VCons :: a -> Vector n a -> Vector (Succ n) a 

अब हम Functor और Applicative जैसे विशिष्ट उदाहरणों चाहते हैं। Functor आसान है:

instance Functor (Vector n) where 
    fmap f VNil = VNil 
    fmap f (VCons a v) = VCons (f a) (fmap f v) 

लेकिन Applicative उदाहरण के साथ कोई समस्या है: हम किस प्रकार शुद्ध में वापस जाने के लिए पता नहीं है। हालांकि, हम वेक्टर के आकार पर उपपादन उदाहरण परिभाषित कर सकते हैं:

instance Applicative (Vector Zero) where 
    pure = const VNil 
    VNil <*> VNil = VNil 

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where 
    pure a = VCons a (pure a) 
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v) 

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

अब, अगर यह केवल Applicative उदाहरण पर लागू होता है तो यह कोई समस्या नहीं होगी, लेकिन यह पता चला है कि इस तरह के प्रकार के साथ प्रोग्रामिंग करते समय रिकर्सिव इंस्टेंस घोषणाओं की चाल आवश्यक है। उदाहरण के लिए, अगर हम TypeCompose लाइब्रेरी का उपयोग पंक्ति वैक्टर का एक वेक्टर के रूप में एक मैट्रिक्स,

type Matrix nx ny a = (Vector nx :. Vector ny) a 

परिभाषित हम एक प्रकार वर्ग को परिभाषित करने और दोनों पक्षांतरित और आव्यूह गुणन लागू करने के लिए पुनरावर्ती उदाहरण घोषणाओं को जोड़ने के लिए है। यह हर बार जब हम कोड का उपयोग करते हैं, तब हमें बाधाओं का एक विशाल प्रसार होता है, भले ही उदाहरण वास्तव में सभी वैक्टरों और मैट्रिस पर लागू होते हैं (बाधाओं को बेकार बनाते हैं)।

क्या इन सभी बाधाओं को दूर करने से बचने का कोई तरीका है? क्या टाइप चेकर का विस्तार करना संभव होगा ताकि यह ऐसे अपरिवर्तनीय निर्माण का पता लगा सके?

Answer 1

pure की परिभाषा वास्तव में समस्या के केंद्र में है। इसका प्रकार, पूरी तरह से मात्राबद्ध और योग्यता क्या होनी चाहिए?

pure :: forall (n :: Nat) (x :: *). x -> Vector n x   -- (X) 

काम नहीं चलेगा, कोई जानकारी निर्धारित करने के लिए pureVNil या VCons फेंकना चाहिए चलाने के समय पर उपलब्ध नहीं है के रूप में। इसके अनुरूप, जैसा कि चीजें खड़ी हैं, आप केवल

instance Applicative (Vector n)        -- (X) 

क्या कर सकते हैं आप क्या कर सकते हैं? खैर,, Strathclyde Haskell Enhancement के साथ काम करने Vec.lhs उदाहरण फ़ाइल में, मैं pure

vec :: forall x. pi (n :: Nat). x -> Vector {n} x 
vec {Zero} x = VNil 
vec {Succ n} x = VCons x (vec n x) 

का पूर्वाभ्यास एक pi प्रकार के साथ परिभाषित करते हैं, की आवश्यकता होती है कि n की एक प्रति कार्यावधि में पारित किया जाना। जहां Natty, वास्तविक जीवन में एक अधिक नीरस नाम के साथ, सिंगलटन GADT है

forall n. Natty n -> 

के रूप में यह pi (n :: Nat). desugars द्वारा

data Natty n where 
    Zeroy :: Natty Zero 
    Succy :: Natty n -> Natty (Succ n) 

दिया और vec के लिए समीकरण में घुंघराले ब्रेसिज़ बस को Nat कंस्ट्रक्टर्स का अनुवाद Natty रचनाकार।मैं फिर निम्नलिखित डायबोलिकल इंस्टेंस को परिभाषित करता हूं (डिफ़ॉल्ट फंक्शन उदाहरण को बंद करना)

instance {:n :: Nat:} => Applicative (Vec {n}) where 
    hiding instance Functor 
    pure = vec {:n :: Nat:} where 
    (<*>) = vapp where 
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t 
    vapp VNil   VNil   = VNil 
    vapp (VCons f fs) (VCons s ss) = VCons (f s) vapp fs ss 

जो अभी भी और तकनीक की मांग करता है। बाधा {:n :: Nat:} किसी चीज के लिए desugars जो कि Natty n गवाह मौजूद है, और स्कॉप्ड प्रकार चर की शक्ति से, उसी {:n :: Nat:} subpoenas जो स्पष्ट रूप से गवाह है। पूरे अक्षरों में लिखावट, कि

class HasNatty n where 
    natty :: Natty n 
instance HasNatty Zero where 
    natty = Zeroy 
instance HasNatty n => HasNatty (Succ n) where 
    natty = Succy natty 

है और हम HasNatty n साथ बाधा {:n :: Nat:} और (natty :: Natty n) साथ इसी अवधि बदलें। इस निर्माण को व्यवस्थित रूप से टाइप क्लास प्रोलॉग में हास्केल टाइपकेकर का एक टुकड़ा लिखने की मात्रा है, जो खुशी का मेरा विचार नहीं है इसलिए मैं कंप्यूटर का उपयोग करता हूं।

ध्यान दें कि Traversable उदाहरण (मेरी मुहावरा कोष्ठक और मेरे चुप डिफ़ॉल्ट functor और Foldable उदाहरणों क्षमा) ऐसी कोई बेबात

instance Traversable (Vector n) where 
    traverse f VNil   = (|VNil|) 
    traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|) 

सभी संरचना आप आगे स्पष्ट प्रत्यावर्तन के बिना आव्यूह गुणन प्राप्त करने की आवश्यकता है कि आवश्यकता है।

टी एल; डॉ उपयोग सिंगलटन निर्माण और उसके संबंधित प्रकार वर्ग प्रकार स्तर के डेटा, जिसमें से आप स्पष्ट प्रत्यावर्तन द्वारा गणना कर सकता है के लिए एक क्रम गवाह के अस्तित्व में रिकर्सिवली परिभाषित उदाहरणों के सभी संक्षिप्त करने के लिए।

डिजाइन प्रभाव क्या हैं?

जीएचसी 7.4 में प्रकार का प्रचार तकनीक है लेकिन SHE में अभी भी सिंगलटन निर्माण pi-प्रकार के प्रस्ताव हैं। प्रचारित डेटाटाइप के बारे में एक स्पष्ट रूप से महत्वपूर्ण बात यह है कि वे बंद कर चुके हैं, लेकिन यह वास्तव में अभी तक स्पष्ट रूप से दिखाई नहीं दे रहा है: सिंगलटन गवाहों की रचनात्मकता उस बंद होने का प्रकटीकरण है। किसी भी तरह, यदि आपके पास forall (n :: Nat). है तो एक सिंगलटन की मांग करना हमेशा उचित होता है, लेकिन ऐसा करने के लिए जेनरेट कोड में कोई फर्क पड़ता है: चाहे यह मेरे pi निर्माण में स्पष्ट है, या {:n :: Nat:} के लिए शब्दकोश में निहित है, तो अतिरिक्त है रनटाइम जानकारी चारों ओर घूमने के लिए, और एक संगत कमजोर मुक्त प्रमेय।

जीएचसी के भविष्य के संस्करणों के लिए एक खुला डिजाइन प्रश्न यह है कि रनटाइम गवाहों की उपस्थिति और अनुपस्थिति के बीच टाइप-स्तर डेटा के बीच इस भेद को कैसे प्रबंधित किया जाए। एक तरफ, हमें बाधाओं में उनकी जरूरत है। दूसरी ओर, हमें उन पर पैटर्न-मिलान करने की आवश्यकता है। जैसे, pi (n :: Nat). मतलब यह होना चाहिए स्पष्ट

forall (n :: Nat). Natty n -> 

या अस्पष्ट

forall (n :: Nat). {:n :: Nat:} => 

? बेशक, एग्डा और कोक जैसी भाषाओं में दोनों रूप हैं, इसलिए होस्केल को सूट का पालन करना चाहिए। प्रगति करने के लिए निश्चित रूप से कमरा है, और हम इस पर काम कर रहे हैं!