Agda में आकार के प्रकार क्या हैं?

Question

Agda में आकार के प्रकार क्या हैं? मैं MiniAgda के बारे में पढ़ने के लिए कागज की कोशिश की है, लेकिन आगे बढ़ने के लिए विफल रहा है निम्नलिखित बातों की वजह से:

1. क्यों डेटा प्रकार उनके आकार से अधिक सामान्य कर रहे हैं? जहां तक ​​मुझे पता है कि आकार प्रेरण के पेड़ की गहराई है।
2. डेटा प्रकार उनके आकार पर क्यों हैं, यानी मैं < = j -> T_i < = T_j?
3. > और # पैटर्न का अर्थ क्या है?

Answer 1

1. विचार है कि एक आकार प्रकार जो अनिवार्य रूप से ऑर्डिनल्स हैं आकार द्वारा अनुक्रमित प्रकार के सिर्फ एक परिवार है। sized data के रूप में एक अपरिवर्तनीय प्रकार को परिभाषित करते समय, संकलक जांचता है कि परिणाम सही आकार के साथ एक प्रकार है, उदाहरण के लिए, succSNat में आकार 1 में बढ़ता है। इस तरह, आकार के प्रकार S(i : Size) -> S i अनिवार्य रूप से एक तत्व है S आकार i के साथ। मेरे लिए अजीब लग रहा है कि जैसे SNat के लिए शून्य की परिभाषा zero : (i : Size) -> SNat ($ i) है, जैसे zero : (i : Size) -> SNat ($ 0)।
2. आकार आगमनात्मक प्रकारों के लिए इस समझ में आता है, के रूप में T_i आकार से कम मैं के साथ टी के तत्वों के प्रकार है, इसलिए यदि मैं j ≤ तो T_i ≤ T_j कि; रचनाकारों को रिकर्सिव कॉल में आकार बढ़ाना चाहिए।

3. जैसा कि खंड 2.3, # में बताया गया है, T_∞ के समतुल्य है, टी के तत्वों का प्रकार ज्ञात आकार के साथ नहीं है; यह सबटाइपिंग प्रीऑर्डर में टी_आई के लिए एक शीर्ष तत्व है। जे < i को जानकारी रखते हुए पैटर्न (i> j) का उपयोग आकार जे को बांधने के लिए किया जाता है I। शून्य से के लिए समाचार पत्र में उदाहरण यह स्पष्ट करता है:

   fun minus : [i : Size] -> SNat i -> SNat # -> SNat i 
   { minus i (zero (i > j)) y = zero j 
   ; minus i x (zero .#) = x 
   ; minus i (succ (i > j) x) (succ .# y) = minus j x y 
   } 
   

   सबसे पहले हस्ताक्षर का मतलब है कि किसी भी संख्या substracting मैं (कि क्या SNat i साधन है अधिक से अधिक आकार के एक नंबर से (SNat # कोई आकार बाध्य जानकारी के साथ एक संख्या है)) अधिकांश आकार में कई आकार देता है; और > पैटर्न के लिए, आखिरी पंक्ति में हम इसे अधिकांश जे में कई आकारों से मेल खाने के लिए उपयोग करते हैं, और उप-टाइपिंग के कारण रिकर्सिव कॉल प्रकार चेक: SNat j ≤ SNat i।