在Idris中对矢量进行分区:为什么0和m + n不能统一？

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)

但伊德里斯报告(指向"分区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.如果说服伊德里斯这个怎么样？

Answer 1

请记住,统一是一种语法操作,在像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了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'))))

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