用DecEq实现'等于Vect'

Question

我试图实现以下内容:

headEqual : DecEq a => (x : a) -> (y : a) -> Maybe (Dec (x = y))
headEqual x y = case decEq x y of
                  Yes Refl  => Just (Yes Refl)
                  No contra => Nothing

vectEqual : DecEq a => (xs : Vect n a) -> (ys : Vect n a) -> Maybe (Dec (xs = ys))
vectEqual []         []         = Just (Yes Refl)
vectEqual (x :: xxs) (y :: yys) = case headEqual x y of
                                  Just (Yes prf) => vectEqual xxs yys
                                  No contra      => Nothing
vectEqual (x :: xxs) []         = Nothing
vectEqual []         (y :: yys) = Nothing

但是,它无法编译:

*section3> :r
Type checking ./section3.idr
section3.idr:45:63-66:
When checking right hand side of Main.case block in vectEqual at section3.idr:44:40 with expected type
        Maybe (Dec (x :: xxs = y :: yys))

When checking argument xs to Main.vectEqual:
        Unifying len and S len would lead to infinite value
Holes: Main.y, Main.vectEqual

我不明白这个编译时错误.有人可以解释一下吗？

Answer 1

对于非空案例,您需要两个证明 - 一个是头部相等而一个是尾部.然后,您需要将这些证明组合成一个用于输入向量.在:

Just (Yes prf) => vectEqual xxs yys

当您需要整个列表的证明时,您正试图返回尾部证明.您需要检查递归调用的结果以构建证明,例如

vectEqual : DecEq a => (xs : Vect n a) -> (ys : Vect n a) -> Maybe (Dec (xs = ys))
vectEqual [] [] = Just (Yes Refl)
vectEqual (x :: xs) (y :: ys) = case decEq x y of
  Yes hd_prf => case vectEqual xs ys of
    Just (Yes tl_prf) => ?combine_proofs
    _ => Nothing
  No contra => Nothing

如果您在REPL加载上面的定义,你会看到的类型hd_prf和tl_prf:

hd_prf : x = y
tl_prf : xs = ys

你可以rewrite用来构建所需的证据(x :: xs) = (y :: ys)

Just (Yes tl_prf) => rewrite hd_prf in rewrite tl_prf in Just (Yes Refl)

注意这个函数的返回类型有点奇怪,因为你Nothing用来编码Dec已经使用No构造函数提供的失败案例,所以你永远不会返回Just (No _).