は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があります。これらは2つの異なるタイプです。

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)