`decEq`

Question

Étant donné:

*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 

Pourquoi faut-il les arguments Nat égal entre eux pour DecEq?

Remarque - écrit dans https://groups.google.com/forum/#!topic/idris-lang/qgtImCLka3I à l'origine

Answer 1

decEq est pour homogène égalité propositionnelle:

||| 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) 

Comme vous pouvez le voir, x1 et x2 sont tous deux de type t. Dans votre cas, vous avez x1 : Vect 2 Integer et x2 : Vect 0 Int. Ce sont deux types différents.

Vous pouvez écrire votre propre decider d'égalité hétérogène pour Vect eurs du même type d'élément en vérifiant d'abord leur longueur, puis déléguer à la version homogène:

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)