理解`decEq`

Question

考虑：

*section3> :module Data.Vect  
*section3> :let e = the (Vect 0 Int) [] 
*section3> :let xs = the (Vect _ _) [1,2] 

*section3> decEq xs e 
(input):1:7:When checking argument x2 to function Decidable.Equality.decEq: 
     Type mismatch between 
       Vect 0 Int (Type of e) 
     and 
       Vect 2 Integer (Expected type) 

     Specifically: 
       Type mismatch between 
         0 
       and 
         2 

为什么一定要Nat参数彼此相当的DecEq？

注 - 张贴在https://groups.google.com/forum/#!topic/idris-lang/qgtImCLka3I原本

Answer 1

decEq是同质命题平等：

||| Decision procedures for propositional equality 
interface DecEq t where 
    ||| Decide whether two elements of `t` are propositionally equal 
    total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2) 

正如你所看到的，x1和x2都是t类型。在你的情况下，你有x1 : Vect 2 Integer和x2 : Vect 0 Int。这是两种不同的类型。

import Data.Vect 

vectLength : {xs : Vect n a} -> {ys : Vect m a} -> xs = ys -> n = m 
vectLength {n = n} {m = n} Refl = Refl 

decEqVect : (DecEq a) => (xs : Vect n a) -> (ys : Vect m a) -> Dec (xs = ys) 
decEqVect {n = n} {m = m} xs ys with (decEq n m) 
decEqVect xs ys | Yes Refl = decEq xs ys 
decEqVect xs ys | No notEq = No (notEq . vectLength)