इडिस में पोस्टलेट

Question

क्या इडिस में postulate निर्माण की प्रकृति और उपयोग के बारे में कोई अद्यतित जानकारी है? इस विषय पर ट्यूटोरियल/मैनुअल में कुछ भी नहीं है और मुझे विकी में कुछ भी नहीं दिख रहा है। TIA।

Answer 1

मुझे लगता है कि हम बात की इस तरह के लिए एक संदर्भ के अधिक में विकी को विकसित करने के लिए जा रहे थे: https://github.com/idris-lang/Idris-dev/wiki/Manual

postulate के लिए वाक्य रचना है:

postulate identifier : type 

postulate n : Nat 

में के रूप में

या

postulate whyNot : 5 = 6 

यह उस प्रकार का एक अनिर्दिष्ट मूल्य प्रस्तुत करता है। यह उपयोगी हो सकता है जब आपको उस प्रकार के उदाहरण की आवश्यकता होती है जिसे आप अन्यथा नहीं जानते हैं कि कैसे पेश किया जाए।

class Semigroup a where 
    op : a -> a -> a 
    semigroupOpIsAssoc : (x, y, z : a) -> op (op x y) z = op x (op y z) 

काफी आसान Nats और जैसी चीजों के लिए साबित करने के लिए है कि: आप कुछ है कि एक सबूत की आवश्यकता है, लागू करना चाहते हैं की तरह इस semigroup typeclass का सबूत है कि आपरेशन यह एक वैध semigroup पर विचार किया जाएगा के लिए साहचर्य है की आवश्यकता है कहो सूची, लेकिन मशीन int की तरह कुछ के लिए क्या है जहां ऑपरेशन भाषा के बाहर परिभाषित किया गया है? आपको यह दिखाने की ज़रूरत है कि semigroupOpIsAssoc द्वारा दिए गए प्रकार के हस्ताक्षर में निवास किया गया है, लेकिन भाषा में ऐसा करने का कोई तरीका नहीं है। तो आप कंपाइलर को कहने के तरीके के रूप में, इस तरह के किसी चीज़ के अस्तित्व को पोस्ट कर सकते हैं "बस इस पर मेरा विश्वास करें"। ऐसे ही अवधारणा की वजह से

instance Semigroupz Int where 
    op = (+) 
    semigroupOpIsAssoc x y z = intAdditionIsAssoc 
     where postulate intAdditionIsAssoc : (x + y) + z = x + (y + z) 

कार्यक्रम अभी भी चलाने जा सकता है और इस्तेमाल किया है, जब तक किसी भी माने "मूल्यों" रनटाइम मान से पहुंच योग्य नहीं हैं (उनके मूल्य क्या होगा?)। यह समानता शर्तों के लिए ठीक है, जिनका उपयोग कहीं भी नहीं किया जाता है लेकिन टाइपशेकिंग और रनटाइम पर मिटा दिया जाता है। प्रकार का अपवाद वह नियम है जिसका मूल्य मिटाया जा सकता है, उदा। singley-बसे हुए Unit प्रकार:

postulate foo : Unit 

main : IO() 
main = print foo 

अभी भी संकलित करता है तथा रन (प्रिंट "()"); Unit प्रकार का मान वास्तव में show के कार्यान्वयन द्वारा आवश्यक नहीं है।