ベクトルの長さが等しいかどうかを確認

Question

考える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 

が最後の関数のJust (Same m)Just eqでは、コンパイラは文句：

*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 

どのように作業すなわち、Just (Same m)を行いますコードは、exactLengthのlenとmが等しいという「証拠」を提供しますか？

Answer 1

あなたは

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

で開始し、徐々にあなたが

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 

に達するまでは、イドリスはcheckEqNat m lenは、それが、その後できるJust (Same ...)を返されたという事実から派生することができますどのように見ることができます行方不明のリンクを延長{m = len}と推測します。 AFAIKだけでJust eqを書くことは、eqが実際に住んでいるという証拠ではありません。

Answer 2

Idrisを使って作業するときに役立つのは、それらを解決するのではなく、何かについてわからないときに穴を追加することです。

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 

、その後、型チェックの結果を見ながらeqと背中に(Same m)を変更します。そこに何が起こっているか確認するためにJust ...枝に穴を追加するように。 eqケースでは、このようなものだ：

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

そして(Same m)場合には、このようなものだ：

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

のでeqはタイプEqNat m lenのようなものである、誰もが、それは住民だかどうか知りませんSame m（またはSame len）は確かに住人であり、mとlenが等しいことが証明されます。