伊德里斯中的快速排序

Question

我正在学习 Idris，我想我会尝试为 Vect 类型实现快速排序。

但是我在使用实用程序方法时遇到了困难，该方法应该给定一个主元和一个向量，将向量一分为二，一个元素 ≤ 主元，另一个元素 > 主元。

这对于列表来说很简单：

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，我需要表达这样一个事实，即两个 returned Vect 的长度之和等于输入 Vect 的长度。

我显然需要 return 一对依赖。元素数 ≤ pivot 似乎是第一个值的不错候选，但我的第一次尝试：

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 来让类型检查器放心，但是我不知道如何递归地创建一个 return 值 k传递谓词。

我的意思是，即使是基本情况，其中 n = k = 0:

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

错误同时提到了 k1 和 k，这表明类型签名可能有问题：

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来表达不变量：

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

但是我不知道如何进行减法（这应该是可能的，因为一个 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 函数提供以下规范：

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))

伊德里斯中的快速排序

Quicksort in Idris

quicksort

idris