Vérifiez si les Longueurs de Vector sont égales

Question

Compte tenu de ce qui suit de Type-Driven Development with Idris:

import Data.Vect 

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where 
    Same : (num : Nat) -> EqNat num num        

sameS : (eq : EqNat k j) -> EqNat (S k) (S j) 
sameS (Same n) = Same (S n) 

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2) 
checkEqNat Z  Z  = Just $ Same Z 
checkEqNat Z  (S k) = Nothing 
checkEqNat (S k) Z  = Nothing 
checkEqNat (S k) (S j) = case checkEqNat k j of 
          Just eq => Just $ sameS eq 
          Nothing => Nothing 

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a) 
exactLength {m} len input = case (checkEqNat m len) of 
           Just (Same m) => Just input 
           Nothing  => Nothing 

Si je remplace la dernière fonction de Just (Same m) avec Just eq, le compilateur se plaint:

*Lecture> :r 
Type checking ./Lecture.idr 
Lecture.idr:19:75: 
When checking right hand side of Main.case block in exactLength at Lecture.idr:18:34 with expected type 
     Maybe (Vect len a) 

When checking argument x to constructor Prelude.Maybe.Just: 
     Type mismatch between 
       Vect m a (Type of input) 
     and 
       Vect len a (Expected type) 

     Specifically: 
       Type mismatch between 
         m 
       and 
         len 
Holes: Main.exactLength 

Comment Just (Same m), à savoir le travail code, fournir "évidence" que exactLengthlen et m sont égaux?

Answer 1

Lorsque vous démarrez avec

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a) 
exactLength {m} len input with (_) 
    exactLength {m} len input | with_pat = ?_rhs 

et d'étendre progressivement les liens manquants jusqu'à ce que vous avez atteint

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a) 
exactLength {m} len input with (checkEqNat m len) 
    exactLength {m = m} len input | Nothing = Nothing 
    exactLength {m = len} len input | (Just (Same len)) = Just input 

vous pouvez voir comment idris peut tirer du fait que checkEqNat m len retourné un Just (Same ...) qu'il peut alors déduire que {m = len}. AFAIK juste en écrivant Just eq n'est pas une preuve que eq est en effet habité.

Answer 2

Ce que je trouve utile lorsque je travaille avec Idris est d'ajouter des trous lorsque vous n'êtes pas sûr de quelque chose plutôt que de les résoudre. Comme l'ajout d'un trou dans Just ... branche pour voir ce qui se passe là-bas:

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a) 
exactLength {m} len input = case (checkEqNat m len) of 
         Just (Same m) => ?hole 
         Nothing => Nothing 

puis changer (Same m)-eq et à l'arrière tout en regardant les résultats de la vérification de type. Dans le eq cas, il est comme ça:

- + Main.hole [P] 
`--   a : Type 
       m : Nat 
      len : Nat 
      eq : EqNat m len 
      input : Vect m a 
    -------------------------------- 
     Main.hole : Maybe (Vect len a) 

Et dans le (Same m) cas, il est comme ça:

- + Main.hole_1 [P] 
`--   m : Nat 
       a : Type 
      input : Vect m a 
    -------------------------------- 
     Main.hole_1 : Maybe (Vect m a) 

Alors eq est quelque chose d'un type EqNat m len, on ne sait pas que ce soit habitant ou non, alors que Same m (ou Same len) est certainement habitant ce qui prouve que m et len ​​sont égaux.