idris - 在 Idris : why can't 0 and m+n be unified? 中对向量进行分区

Question

我想将一个向量划分为两个新向量。

我们不知道单个向量的长度是多少，但结果向量的总和必须等于参数。我尝试按如下方式捕获此属性:

partition : (a -> Bool) -> Vect (m+n) a -> (Vect m a, Vect n a)
partition p [] = ([], [])
partition p (x::xs)
  = let (ys,zs) = partition p xs
  in case p xs of
    True  => (x::ys, zs)
    False => (ys, zs)

但是 Idris 报告(指向“partition p []”)在阐述 Main.partition 的左侧时:

Can't unify
        Vect 0 a
with
        Vect (m + n) a

Specifically:
        Can't unify
                0
        with
                plus m n

为什么会这样？

对我来说，如果“0 = m + n”比 m = n = 0 似乎很明显。如何说服 Idris 呢？

Answer 1

请记住，unification 是一种句法操作，在像 Idris 这样的语言中，它根据模式匹配通过简单的减少来增强。它不知道我们可以证明的所有事实!

我们当然可以在 Idris 中证明，如果 n+m=0 那么 m = 0 且 n = 0:

sumZero : (n, m : Nat) -> plus n m = Z -> (n=Z, m=Z)
sumZero Z m prf = (refl, prf)
sumZero (S k) m refl impossible

但这并不能让统一者知道这个事实，因为这会使类型检查变得不可判定。

回到你原来的问题:如果我将你的分区类型翻译成英文，它会说“对于所有自然数 m 和 n ，对于所有 p 上的 bool 谓词 a ，给定一个长度为 plus m n 的向量，我可以产生一对由长度为 m 的向量和长度为 n 的向量“。换句话说，要调用您的函数，我需要提前知道向量中有多少元素满足谓词，因为我需要在调用站点提供 m 和 n!

我认为你真正想要的是一个 partition 函数，给定一个长度为 n 的向量，它返回一对长度加起来为 n 的向量。我们可以使用依赖对来表达这一点，这是存在量化的类型论版本。 “一对长度加起来为 n 的向量”的翻译是“存在一些 m 和 m' 以及具有这些长度的向量，使得 m 和 m' 的总和是我的输入 n 。”

这种类型看起来像这样:

partition : (a -> Bool) -> Vect n a -> (m ** (m' ** (Vect m a, Vect m' a, m+m'=n)))

完整的实现如下所示:

partition : (a -> Bool) -> Vect n a -> (m ** (m' ** (Vect m a, Vect m' a, m+m'=n)))
partition p [] = (Z ** (Z ** ([], [], refl)))
partition p (x :: xs) with (p x, partition p xs)
  | (True, (m ** (m' ** (ys, ns, refl)))) = (S m ** (m' ** (x::ys, ns, refl)))
  | (False, (m ** (m' ** (ys, ns, refl)))) =
      (m ** (S m' ** (ys, x::ns, sym (plusSuccRightSucc m m'))))

说的有点啰嗦，我们来剖析一下。
为了实现该功能，我们首先对输入 Vect 进行模式匹配:

partition p [] = (Z ** (Z ** ([], [], refl)))

请注意，唯一可能的输出是右侧的内容，否则我们无法构建 refl 。由于 n 与 Z 的构造函数 n 的索引统一，我们知道 Nil 是 Vect。

在递归情况下，我们检查向量的第一个元素。在这里，我使用 with 规则，因为它是可读的，但我们可以在右侧使用 if 而不是在左侧匹配 p x。

partition p (x :: xs) with (p x, partition p xs)

在 True 的情况下，我们将元素添加到第一个子向量。因为 plus 减少了它的第一个参数，我们可以使用 refl 构造等式证明，因为加法完全正确:

  | (True, (m ** (m' ** (ys, ns, refl)))) = (S m ** (m' ** (x::ys, ns, refl)))

在 False 的情况下，我们需要做更多的工作，因为 plus m (S m') 无法与 S (plus m m') 统一。还记得我说过统一无法获得我们可以证明的平等吗？不过，库函数 plusSuccRightSucc 可以满足我们的需求:

  | (False, (m ** (m' ** (ys, ns, refl)))) =
      (m ** (S m' ** (ys, x::ns, sym (plusSuccRightSucc m m'))))

作为引用， plusSuccRightSucc 的类型是:

plusSuccRightSucc : (left : Nat) ->
                    (right : Nat) ->
                    S (plus left right) = plus left (S right)

sym 的类型是:

sym : (l = r) -> r = l

上述函数中缺少的一件事是该函数实际上对 Vect 进行了分区。我们可以通过使结果向量由依赖元素对和每个元素满足 p 或 not p 的证据组成来添加这一点:

partition' : (p : a -> Bool) ->
             (xs : Vect n a) ->
             (m ** (m' ** (Vect m (y : a ** so (p y)),
                           Vect m' (y : a ** so (not (p y))),
                           m+m'=n)))
partition' p [] = (0 ** (0 ** ([], [], refl)))
partition' p (x :: xs) with (choose (p x), partition' p xs)
  partition' p (x :: xs) | (Left oh, (m ** (m' ** (ys, ns, refl)))) =
    (S m ** (m' ** ((x ** oh)::ys, ns, refl)))
  partition' p (x :: xs) | (Right oh, (m ** (m' ** (ys, ns, refl)))) =
    (m ** (S m' ** (ys, (x ** oh)::ns, sym (plusSuccRightSucc m m'))))

如果你想变得更疯狂，你还可以让每个元素证明它是输入向量的一个元素，并且输入向量的所有元素都在输出中恰好一次，依此类推。依赖类型为您提供了做这些事情的工具，但值得考虑每种情况下的复杂性权衡。