इडिस में, "वेक्ट जेनरेटर" फ़ंक्शन कैसे लिखना है जो पैरामीटर

Question

में इंडेक्स का एक फ़ंक्शन लेता है। मैं इडिस में एक ऐसा फ़ंक्शन लिखने की कोशिश कर रहा हूं जो वेक्ट के आकार को पार करके एक वेक्टर बनाता है और एक फ़ंक्शन इंडेक्स लेता है पैरामीटर में अब तक, मैं इस है:

import Data.Fin 
import Data.Vect 

generate: (n:Nat) -> (Nat -> a) ->Vect n a 
generate n f = generate' 0 n f where 
    generate': (idx:Nat) -> (n:Nat) -> (Nat -> a) -> Vect n a 
    generate' idx Z f = [] 
    generate' idx (S k) f = (f idx) :: generate' (idx + 1) k f 

लेकिन मैं यह सुनिश्चित करें कि समारोह पैरामीटर में पारित केवल कम सूचकांक ले जा रहा है Vect के आकार की तुलना करना चाहते हैं। मैंने कोशिश की है कि:

generate: (n:Nat) -> (Fin n -> a) ->Vect n a 
generate n f = generate' 0 n f where 
    generate': (idx:Fin n) -> (n:Nat) -> (Fin n -> a) -> Vect n a 
    generate' idx Z f = [] 
    generate' idx (S k) f = (f idx) :: generate' (idx + 1) k f 

लेकिन यह त्रुटि

Can't convert 
      Fin n 
    with 
      Fin (S k) 

मेरा प्रश्न है साथ संकलन नहीं है: मैं संभव करने के लिए क्या चाहते है और कैसे?

Answer 1

कुंजी विचार है कि वेक्टर के पहले तत्व f 0 है, और पूंछ के लिए, यदि आप k : Fin n है, तो FS k : Fin (S n) एक सीमित संख्या के "बदलाव" है कि एक ही समय में अपने मूल्य और उसके प्रकार बढ़ता जाता है है ।

इस अवलोकन का उपयोग करना, हम फिर से लिखने generate रूप

generate : {n : Nat} -> (f : Fin n -> a) -> Vect n a 
generate {n = Z} f = [] 
generate {n = S _} f = f 0 :: generate (f . FS) 

एक और संभावना @dfeuer क्या सुझाव दिया है और Fin रों का एक वेक्टर उत्पन्न करने के लिए है सकता है, तो इस पर नक्शा f:

fins : (n : Nat) -> Vect n (Fin n) 
fins Z = [] 
fins (S n) = FZ :: map FS (fins n) 

generate' : {n : Nat} -> (f : Fin n -> a) -> Vect n a 
generate' f = map f $ fins _ 

generate f = generate' f प्रदान करने के लिए पाठक के लिए अभ्यास के रूप में छोड़ दिया गया है।

Answer 2

कैक्टस का उत्तर आपके द्वारा मांगी जाने वाली चीज़ों को प्राप्त करने का सबसे अच्छा तरीका प्रतीत होता है, लेकिन यदि आप कुछ ऐसा करना चाहते हैं जिसे रनटाइम पर उपयोग किया जा सकता है, तो यह काफी अक्षम होगा। इसके लिए आवश्यक कारण यह है कि Fin n को Fin n+m पर कमजोर करने की आवश्यकता है कि आप इसे FZ के प्रकार को बदलने के लिए पूरी तरह से इसे रद्द कर दें, और उसके बाद इसे फिर से बनाएं। इसलिए प्रत्येक वेक्टर तत्व के लिए उत्पादित Fin मानों के बीच कोई साझाकरण नहीं हो सकता है। एक वैकल्पिक एक सबूत है कि यह नीचे एक दिया बाध्य है, जो विलोपन की संभावना की ओर जाता है के साथ एक Nat गठबंधन करने के लिए है:

data NFin : Nat -> Type where 
    MkNFin : (m : Nat) -> .(LT m n) -> NFin n 

lteSuccLeft : LTE (S n) m -> LTE n m 
lteSuccLeft {n = Z} prf = LTEZero 
lteSuccLeft {n = (S k)} {m = Z} prf = absurd (succNotLTEzero prf) 
lteSuccLeft {n = (S k)} {m = (S j)} (LTESucc prf) = LTESucc (lteSuccLeft prf) 

countDown' : (m : Nat) -> .(m `LTE` n) -> Vect m (NFin n) 
countDown' Z mLTEn = [] 
countDown' (S k) mLTEn = MkNFin k mLTEn :: countDown' k (lteSuccLeft mLTEn) 

countDown : (n : Nat) -> Vect n (NFin n) 
countDown n = countDown' n lteRefl 

countUp : (n : Nat) -> Vect n (NFin n) 
countUp n = reverse $ countDown n 

generate : (n : Nat) -> (NFin n -> a) -> Vect n a 
generate n f = map f (countUp n) 

Fin दृष्टिकोण के रूप में, समारोह आप generate के पास काम करने के लिए की जरूरत नहीं है सभी प्राकृतिक पर; इसे केवल n से कम लोगों को संभालने की आवश्यकता है।

मैंने NFin प्रकार का उपयोग स्पष्ट रूप से इंगित करने के लिए किया था कि मैं सभी मामलों में LT m n सबूत मिटाना चाहता हूं। अगर मैं नहीं चाहता/चाहता हूं, तो मैं इसके बजाय (m ** LT m n) का उपयोग कर सकता हूं।