22
मेरा प्रश्न शायद एक उदाहरण के रूप में व्याख्या करने के लिए सबसे आसान है:मिलान 7.6
type family Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0 xs = '[]
type instance Take (n+1) (x ': xs) = x ': Take n xs
यहां दूसरे उदाहरण अस्वीकार कर दिया है, हालांकि, क्योंकि (+), एक प्रकार परिवार में ही किया जा रहा है, तर्कों में इस्तेमाल नहीं किया जा सकता है। लेकिन ऐसा कोई प्रतीत नहीं होता है कि Succ या नाट से मेल खाने के लिए आमतौर पर उपयोग किया जाता है।
तो, यह व्यक्त किया जा सकता है; और यदि हां, तो कैसे?
अद्यतन। मैंने देखा है कि isZero और isEvenGHC.TypeLits में कार्य "विनाशकारी प्रकार-जाल" शीर्षक में हैं। क्या वे किसी भी तरह के स्तर पर इस्तेमाल किया जाना चाहते हैं? मुझे संदेह नहीं होगा ... लेकिन अधिकतर क्योंकि मैं नहीं देख सकता कि कैसे करें। :)
दाएं। मैंने इस कोड को जांचने में सक्षम होने के लिए अभी जीएचसी 7.6 स्थापित किया है, और नीचे दी गई टिप्पणियों में आपके द्वारा उल्लिखित दोनों मुद्दों को जीएचसी द्वारा ध्वजांकित किया जा रहा है। क्षमा याचना। (मैंने अपने उत्तर पर 'हटाएं' बटन दबाया है, इसलिए अब सीधे इस पर टिप्पणी नहीं कर सकते हैं)। – macron
यह समाप्ति की स्थिति को एन्कोड करने जैसा लगता है क्योंकि तर्क काम कर सकते हैं (https://gist.github.com/a39ce17ca47798b0f0ef देखें) लेकिन यह केवल तब सफल होता है जब n == 1। मैंने इसे टाइप-नेट्स शाखा पर कोशिश की है, 7.6 पर नहीं, इसलिए ymmv। –
'isZero' और' isEven' फ़ंक्शंस समान नाम वाले जीएडीटी का निर्माण करते हैं, जो टर्म स्तर पर टाइप-स्तरीय भविष्यवाणी तक पहुंच प्रदान करते हैं। दूसरे शब्दों में, यह एक प्रकार का कार्य करने के बजाय नियमित टर्म-स्तरीय फ़ंक्शन में इच्छित मिलान करने का एक तरीका है। [ –