हास्केल एकमात्र: हम SNAT

Question

मैं हास्केल एकमात्र grook कोशिश कर रहा हूँ के साथ क्या प्राप्त करते हैं।

कागज Dependently Typed Programming with Singletons में और अपने ब्लॉग पोस्ट singletons v0.9 Released! रिचर्ड Eisenberg में डेटा प्रकार नेट जो Peano axioms के साथ प्राकृतिक संख्या को परिभाषित करता है परिभाषित करता है:

data Nat = Zero | Succ Nat 

भाषा विस्तार DataKinds इस का उपयोग करके डेटा प्रकार को प्रकार के स्तर पर पदोन्नत किया जाता है। डेटा constuctors शून्य और succ प्रकार कंस्ट्रक्टर्स 'शून्य और ' succ करने के लिए प्रोत्साहित कर रहे हैं। इस के साथ हम हर प्राकृतिक संख्या के लिए प्रकार स्तर पर एक भी और अद्वितीय इसी प्रकार मिलता है। उदाहरण के लिए के लिए हम 'succ (' succ ('succ' शून्य)) मिलता है। तो अब हमारे पास प्राकृतिक संख्याएं हैं।

इसके बाद वे प्रकार परिवार प्लस मूल्य स्तर समारोह प्लस पर और प्रकार स्तर पर परिभाषित करता है इसके अलावा आपरेशन उपलब्ध है। के साथ को बढ़ावा देने के समारोह/एकमात्र पुस्तकालय की quasiqoter हम स्वचालित रूप से प्लस समारोह से प्लस प्रकार परिवार बना सकते हैं। इसलिए हम अपने परिवार के प्रकार लिखने से बच सकते हैं।

अब तक तो अच्छा!

data SNat :: Nat -> * where 
    SZero :: SNat Zero 
    SSucc :: SNat n -> SNat (Succ n) 

मूल रूप से वह केवल एक SNAT निर्माता में नेट प्रकार लपेटता:

GADT वाक्य रचना के साथ वह भी एक डेटा प्रकार SNAT परिभाषित करता है। यह आवश्यक क्यों है? हम क्या हासिल करते हैं? डेटा प्रकार Nat और SNat is isororphic नहीं हैं? क्यों SNAT एक सिंगलटन है, और क्यों नेट नहीं एक सिंगलटन है? दोनों मामलों में हर प्रकार एक ही मूल्य, संबंधित प्राकृतिक संख्या में रहता है।

Answer 1

हमें क्या लाभ होता है? हम्म। सिंगलेट्स की स्थिति अजीब है लेकिन वर्तमान में आवश्यक वर्कअराउंड है, और जितनी जल्दी हम उनके साथ बेहतर कर सकते हैं।

मुझे देखने अगर मैं चित्र स्पष्ट कर सकते हैं करते हैं। हम एक डेटा प्रकार Nat है:

data Nat = Zero | Suc Nat 

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

if <b> then <e> else <t> 

को

if <b> then <t> else <e> 

के हर घटना को फिर से लिखने सकते हैं और आप यह सुनिश्चित करें कि कुछ भी नहीं गलत जाना होगा ... अपने कार्यक्रम के प्रकार की जाँच के परिणाम के साथ हो सकता है।

प्रतिस्थापन संपत्ति एक शर्मिंदगी है। यह स्पष्ट सबूत है कि आपका टाइप सिस्टम उस पल में छोड़ देता है जिसका मतलब मायने रखता है।

अब, रन-टाइम मूल्यों के लिए कोई डेटा प्रकार द्वारा किया जा रहा, Nat भी प्रकार स्तरीय का एक प्रकार का सम्मान करता 'Zero और 'Suc हो जाता है। उत्तरार्द्ध केवल हास्केल की टाइप भाषा में रहता है और इसमें कोई रन-टाइम उपस्थिति नहीं होती है। कृपया ध्यान दें कि हालांकि 'Zero और 'Suc प्रकार के स्तर पर मौजूद हैं, लेकिन उन्हें "प्रकार" के रूप में संदर्भित करने के लिए अनुपयोगी है और जो लोग वर्तमान में ऐसा करना चाहते हैं, वे निराश होना चाहिए। उनके पास * टाइप नहीं है और इस प्रकार वर्गीकृत मान वर्गीकृत नहीं कर सकते हैं जो नाम के योग्य हैं।

रन-टाइम और टाइप-लेवल Nat एस के बीच विनिमय का कोई प्रत्यक्ष माध्यम नहीं है, जो एक उपद्रव हो सकता है।

data Vec :: Nat -> * -> * where 
    VNil :: Vec 'Zero x 
    VCons :: x -> Vec n x -> Vec ('Suc n) x 

हमें दिए गए तत्व की प्रतियां का एक वेक्टर गणना करने के लिए पसंद कर सकते हैं (शायद एक Applicative उदाहरण के हिस्से के रूप): निदर्शनात्मक उदाहरण वैक्टर पर एक प्रमुख आपरेशन से संबंधित है। यह

vec :: forall (n :: Nat) (x :: *). x -> Vec n x 

देने के लिए एक अच्छा विचार प्रतीत हो सकता है लेकिन क्या यह संभवतः काम कर सकता है? n कुछ की प्रतियां बनाने के लिए, हमें रन समय पर n जानने की आवश्यकता है: एक प्रोग्राम को यह तय करना होगा कि VNil को तैनात करना है या VCons को रोकना या तैनात करना है, और इसे करने के लिए कुछ डेटा चाहिए। एक अच्छा सुराग forall क्वांटिफायर है, जो पैरामीट्रिक है: यह इंगित करता है कि मात्रात्मक जानकारी केवल प्रकारों के लिए उपलब्ध है और रन टाइम द्वारा मिटा दी गई है।

हास्केल वर्तमान में निर्भर मात्रा (forall करता है) के बीच एक पूरी तरह से नकली संयोग लागू करता है और रन टाइम के लिए मिटा देता है। यह एक आश्रित लेकिन मिट क्वांटिफ़ायर का समर्थन नहीं करता है, जिसे हम अक्सर pi कहते हैं। प्रकार और vec के कार्यान्वयन होना चाहिए कुछ

तरह

vec :: pi (n :: Nat) -> forall (x :: *). Vec n x 
vec 'Zero x = VNil 
vec ('Suc n) x = VCons x (vec n x) 

जहां pi -positions में तर्क प्रकार भाषा में बनाई गई है, लेकिन डेटा रन टाइम पर उपलब्ध हैं।

तो हम इसके बजाय क्या करते हैं? हम अप्रत्यक्ष रूप से कैप्चर करने के लिए सिंगलेट का उपयोग करते हैं जिसका अर्थ है टाइप-स्तरीय डेटा की रन-टाइम प्रति।

data SNat :: Nat -> * where 
    SZero :: SNat Zero 
    SSuc :: SNat n -> SNat (Suc n) 

अब, SZero और SSuc रन-टाइम डेटा बनाते हैं।SNatNat पर isomorphic नहीं है: पूर्व में Nat -> * टाइप किया गया है, जबकि बाद में * टाइप किया गया है, इसलिए यह उन्हें आइसोमोर्फिक बनाने की कोशिश करने के लिए एक प्रकार की त्रुटि है। Nat में कई रन-टाइम मान हैं, और टाइप सिस्टम उन्हें अलग नहीं करता है; प्रत्येक अलग SNat n में बिल्कुल एक रन-टाइम मान (बोलने योग्य) है, इसलिए तथ्य यह है कि टाइप सिस्टम उन्हें अलग नहीं कर सकता है, बिंदु के बगल में है। मुद्दा यह है कि प्रत्येक SNat n प्रत्येक अलग n के लिए एक अलग प्रकार है, और वह जीएडीटी पैटर्न मिलान (जहां एक पैटर्न जीएडीटी प्रकार के अधिक विशिष्ट उदाहरण का हो सकता है जिसे मिलान करने के लिए जाना जाता है) n के हमारे ज्ञान को परिशोधित कर सकता है।

अब हम लिख सकते हैं

vec :: forall (n :: Nat). SNat n -> forall (x :: *). x -> Vec n x 
vec SZero x = VNil 
vec (SSuc n) x = VCons x (vec n x) 

Singletons हमें, रन टाइम और प्रकार स्तर के डेटा के बीच की खाई को पाटने के लिए है कि प्रकार की जानकारी के शोधन की अनुमति देता है चलाने के समय विश्लेषण के केवल प्रपत्र का दुरुपयोग करके अनुमति देते हैं। यह आश्चर्यजनक है कि वे वास्तव में जरूरी हैं, और वे वर्तमान में हैं, केवल इसलिए कि उस अंतर को अभी तक समाप्त नहीं किया गया है।