In Idris, wie schreibe ich eine "vect Generator" -Funktion, die eine Funktion des Index in Parameter

Question

Ich versuche, in Idris eine Funktion zu schreiben, die ein Vect durch die Größe des Vect und eine Funktion, die den Index zu übergeben in Parameter. Bisher habe ich dies:

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 

Aber ich möchte sicherstellen, dass die Funktion in Parameter übergeben nur Index kleiner als die Größe des Vect nehmen wird. Ich habe versucht, dass:

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 

Aber es ist nicht mit dem Fehler

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

Meine Frage ist nicht kompiliert: ist, was ich will möglich tun und wie?

Answer 1

Die Schlüsselidee ist, dass das erste Element des Vektors f 0 ist, und für den Schwanz, wenn Sie k : Fin n haben, dann FS k : Fin (S n) ist eine „Verschiebung“ der endlichen Zahl, die seinen Wert und seine Art zur gleichen Zeit erhöht .

diese Beobachtung, können wir umschreiben generate als

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

Eine weitere Möglichkeit zu tun ist, was @dfeuer vorgeschlagen und einen Vektor von Fin s zu erzeugen, dann f darüber Karte:

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 _ 

Proving generate f = generate' f ist als Übung für den Leser überlassen.

Answer 2

Die Antwort von Cactus scheint der beste Weg zu sein, um das zu erhalten, wonach Sie gefragt haben, aber wenn Sie etwas wollen, das zur Laufzeit verwendet werden kann, wird es ziemlich ineffizient sein. Der wesentliche Grund dafür ist, dass ein Fin n zu einem Fin n+m schwächen erfordert, dass Sie es vollständig dekonstruieren, um den Typ seines FZ zu ändern, und bauen Sie es dann wieder auf. Zwischen den Fin Werten, die für jedes Vektorelement erzeugt werden, kann also überhaupt keine Freigabe erfolgen. Eine Alternative ist ein Nat mit einem Beweis zu kombinieren, dass sie unter einem gebundenen gegeben sind, was auf die Möglichkeit der Löschung führt:

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) 

Wie im Fin Ansatz, die Funktion, die Sie generate passieren muss nicht arbeiten auf allen natürlichen; es muss nur mit weniger als n umgehen.

Ich verwendete den NFin Typ, um explizit anzugeben, dass ich den Beweis in allen Fällen gelöscht werden soll. Wenn ich das nicht möchte/brauche, kann ich stattdessen (m ** LT m n) verwenden.