在伊德里斯的Quicksort

Question

我正在学习Idris，我想我会尝试为Vect类型实现Quicksort。

但是我很难使用实用工具方法，给定一个pivot元素和一个向量，将向量分成两个，一个元素≤枢轴，另一个元素> pivot。

这对于列表来说是微不足道的：

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，我需要表达两个返回的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 _ [] = (_ ** ([], []))

错误提到了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))