इडिस में एक प्रकार के रूप में एक संख्या सीमा निर्दिष्ट करने के लिए कैसे?

Question

मैं इडिस के साथ प्रयोग कर रहा हूं और ऐसा लगता है कि दो अलग-अलग संख्याओं के बीच सभी संख्याओं का प्रतिनिधित्व करने के लिए किसी प्रकार का प्रकार निर्दिष्ट करना सरल होना चाहिए। NumRange 5 10 5 और 10 के बीच सभी संख्याओं का प्रकार है। मैं युगल/फ्लोट्स को शामिल करना चाहता हूं, लेकिन पूर्णांक के साथ ऐसा करने के लिए एक प्रकार समान रूप से उपयोगी होगा। मैं ऐसा कैसे कर पाऊंगा?

Answer 1

प्रैक्टिस में, आप बस आवश्यकतानुसार सीमाओं की जांच करने के लिए बेहतर कर सकते हैं, लेकिन आप निश्चित रूप से ऐसी संपत्ति को लागू करने के लिए डेटा प्रकार लिख सकते हैं। यह इस तरह है करने के लिए

एक सरल तरीके:

data Range : Ord a => a -> a -> Type where 
    MkRange : Ord a => (x,y,z : a) -> (x >= y && (x <= z) = True) -> Range y z 

मैं इसे सामान्य रूप से लिखा है Ord typeclass से अधिक है, हालांकि आप इसे विशेषज्ञ पड़ सकता है। रेंज आवश्यकता को समीकरण के रूप में व्यक्त किया जाता है, इसलिए आप इसे बनाने के दौरान Refl की आपूर्ति करते हैं, और फिर संपत्ति की जांच की जाएगी। उदाहरण के लिए: MkRange 3 0 10 Refl : Range 0 10। इस तरह की किसी चीज़ का एक नुकसान निहित मूल्य निकालने की असुविधा है। और निश्चित रूप से यदि आप प्रोग्रामेटिक रूप से एक उदाहरण बनाना चाहते हैं तो आपको सबूतों की आपूर्ति करने की आवश्यकता होगी कि सीमाएं वास्तव में संतुष्ट हैं, या फिर कुछ संदर्भ में ऐसा करें जो विफलता की अनुमति देता है, जैसे Maybe।

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

data InRange : Nat -> Nat -> Type where 
    IsInRange : (x : Nat) -> LTE n x -> LTE x m -> InRange n m 

अब यह डेटा प्रकार अच्छी तरह से एक सबूत encapsulates है कि एन ≤ x ≤ मीटर। यह कई आकस्मिक अनुप्रयोगों के लिए अधिक होगा, लेकिन यह निश्चित रूप से दिखाता है कि आप इस उद्देश्य के लिए निर्भर प्रकारों का उपयोग कैसे कर सकते हैं।