İdriste,

Question

parametresinde indeks işlevini alan bir "vect generator" fonksiyonu nasıl yazılırım İdris'te Vect'in boyutunu geçirerek bir Vect yaratan bir fonksiyon ve indeksi alan bir fonksiyon yazmaya çalışıyorum parametresinde.

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 

Ama parametresinde geçirilen işlevi yalnızca vect boyutundan daha az endeks baz alınarak sağlamak istiyoruz: Şimdiye kadar, ben bu ettik.

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 

Ama

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

Sorum şu hata ile derleme değil: Denedim ben mümkün yapmak istediğiniz şey ne ve nasıl?

Answer 1

anahtar fikri vektörü ilk öğesi Eğer k : Fin n varsa, o zaman FS k : Fin (S n) aynı anda değerini ve türünü artırır sonlu sayısının bir "kayma" dir, f 0 ve kuyruk için olmasıdır . Bir başka olasılık @dfeuer önerdi yapmak ve Fin s'lik bir vektör üretmektir generate

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

olarak

bu gözlemi kullanarak, sonra üzerine f harita, yeniden yazabilirsiniz:

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'un kanıtlanması, okuyucuya egzersiz olarak bırakılmıştır.

Answer 2

Cactus'un cevabı, istediğiniz şeyi elde etmenin en iyi yolu hakkında görünüyor, ancak çalışma zamanında kullanılabilecek bir şey istiyorsanız, oldukça verimsiz olacaktır. Bunun temel nedeni, Fin n'un Fin n+m'a zayıflatılması için, FZ türünün türünü değiştirmek için onu tamamen bozmanızı ve sonra tekrar yeniden oluşturmanızı gerektirir. Dolayısıyla, her bir vektör öğesi için üretilen Fin değerleri arasında hiç paylaşım olamaz. Bir alternatif bir bağlı vermiş olduğu aşağıda o silme olanağı yaratmaktadır olduğunu kanıtlayan bir belgeyle bir Nat birleştirmektir: Fin yaklaşımda olduğu gibi

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) 

, sen generate geçmek işlevi çalışmak gerekmez tüm doğallarda; Sadece n'dan daha az olanları işlemek gerekir.

LT m n kanıtının her durumda silinmesini istediğimi açıkça belirtmek için NFin türünü kullandım. Eğer buna ihtiyacım olmasaydı, bunun yerine (m ** LT m n)'u kullanabilirdim.