Idrisのクイックソート

Question

私はIdrisを学んでおり、私はVectタイプのQuicksortを実装しようと考えていました。

しかし、ピボット要素とベクトルを指定すると、≤ピボット要素とピボット要素を持つ2つのベクトルを分割するユーティリティメソッドでは苦労しています。

splitListOn : Ord e => (pivot : e) -> List e -> (List e, List e) 
splitListOn pivot [] = ([], []) 
splitListOn pivot (x :: xs) = let (ys, zs) = splitListOn pivot xs in 
           if x <= pivot then (x :: ys, zs) 
              else (ys, x :: zs) 

*Test> splitListOn 3 [1..10] 
([1, 2, 3], [4, 5, 6, 7, 8, 9, 10]) : (List Integer, List Integer) 

しかしVECTのために私は2つの長さの合計がVectsが入力VECTの長さに等しい返されたという事実を表現する必要があります。

これはリストのための簡単です。

明らかに従属ペアを返す必要があります。ピボット≤要素の数は、最初の値のための良い候補だが、私の最初の試み：

splitVectOn : Ord e => e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e)) 

は、k個の≤nのかどうか知らない（当然のように）文句を言う：

When checking type of Main.splitVectOn: 
When checking argument smaller to function Prelude.Nat.-: 
     Can't find a value of type 
       LTE k n 

そのようなものLTE k nをタイプシグネチャを再確認するために型シグネチャに追加することはできますが、再帰的にどのようにして述語を渡す戻り値kを作成するのかわかりません。

私はここで、n = K = 0、いない基本ケースのために、意味：

splitVectOn : Ord e => LTE k n => 
       e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e)) 
splitVectOn _ [] = (_ ** ([], [])) 

エラータイプ署名に問題があるかもしれないことを示唆している​​とk、両方に言及：

splitVectOn : Ord e => e -> Vect n e -> 
       (k : Fin (S n) ** (Vect (finToNat k) e, Vect (??? (n - k)) e)) 

012：

When checking right hand side of splitVectOn with expected type 
     (k1 : Nat ** (Vect k e, Vect (0 - k) e)) 

When checking argument a to constructor Builtins.MkPair: 
     Type mismatch between 
       Vect 0 e (Type of []) 
     and 
       Vect k e (Expected type) 

     Specifically: 
       Type mismatch between 
         0 
       and 
         k 

私も不変を表現するためにFinを使用するのではと思いました

その後私は、減算を実行する方法がわからない（フィン（S n）が常にあるので、可能なはず≤n）はあなたがそうのような出力タイプに必要な証拠を追加することができます

Answer 1

：

ここで

(k ** pf : LTE k n ** (Vect k e, Vect (n - k) e)) 

私たちは、この関数を定義する方法です。

-- auxiliary lemma 
total 
minusSuccLte : n `LTE` m -> S (m `minus` n) = (S m) `minus` n 
minusSuccLte {m} LTEZero = cong $ minusZeroRight m 
minusSuccLte (LTESucc pf) = minusSuccLte pf 

total 
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
         (k ** pf : LTE k n ** (Vect k e, Vect (n - k) e)) 
splitVectOn pivot [] = (0 ** LTEZero ** ([], [])) 
splitVectOn pivot (x :: xs) = 
    let (k ** lte ** (ys, zs)) = splitVectOn pivot xs in 
    if x <= pivot then (S k ** LTESucc lte ** (x :: ys, zs)) 
    else 
    let xzs = replace {P = \n => Vect n e} (minusSuccLte lte) (x :: zs) in 
    (k ** lteSuccRight lte ** (ys, xzs)) 

は、同じ問題に対する別のアプローチは、splitVectOn fucntionに次の仕様を与えることです：

total 
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
       (k1 : Nat ** k2 : Nat ** (k1 + k2 = n, Vect k1 e, Vect k2 e)) 

すなわち、出力ベクトルの長さを定量化し、その長さの合計が入力ベクトルの長さに等しくなければならないという条件を追加します。このk1 + k2 = nの条件を省略することもできますが、実装を大幅に簡素化できます。

total 
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
       (k1 : Nat ** k2 : Nat ** (k1 + k2 = n, Vect k1 e, Vect k2 e)) 
splitVectOn pivot [] = (0 ** 0 ** (Refl, [], [])) 
splitVectOn pivot (x :: xs) = 
    let (k1 ** k2 ** (eq, ys, zs)) = splitVectOn pivot xs in 
    if x <= pivot then (S k1 ** k2 ** (cong eq, x :: ys, zs)) 
    else let eq1 = sym $ plusSuccRightSucc k1 k2 in 
     let eq2 = cong {f = S} eq in 
     (k1 ** S k2 ** (trans eq1 eq2, ys, x :: zs))