Überprüfen Sie, ob Vectors Längen gleich sind

Question

die von Type-Driven Development with Idris folgenden Gegeben:

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 

Wenn ich die letzte Funktion des Just (Same m) mit Just eq, der Compiler beschwert ersetzen:

*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 

Wie funktioniert Just (Same m), dh die Arbeits Code, liefern "Beweise", dass exactLength 's len und m sind gleich?

Answer 1

Wenn Sie beginnen mit

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

und nach und nach die fehlenden Glieder verlängern, bis Sie

erreicht

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 

Sie können sehen, wie idris aus der Tatsache ableiten, dass checkEqNat m len eine Just (Same ...) zurückgegeben, dass es dann folgern, dass {m = len}. AFAIK nur Just eq schreiben ist kein Beweis, dass tatsächlich bewohnt ist.

Answer 2

Was ich bei der Arbeit mit Idris nützlich finde, ist das Hinzufügen von Löchern, wenn Sie sich nicht sicher sind, was sie lösen sollen, anstatt sie zu lösen. Wie das Hinzufügen von ein Loch in Just ... Zweig zu sehen, was dort vor sich geht:

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 

und dann (Same m)-eq ändern und zurück, während Blick auf die Ergebnisse der Typprüfung. Im eq Fall ist es wie folgt aus:

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

Und im (Same m) Fall ist es wie folgt aus:

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

So ist eq etwas von einer Art EqNat m len, niemand weiß, ob es sich um Einwohner oder nicht, während Same m (oder Same len) ist definitiv Einwohner was beweist, dass m und len gleich sind.