벡터의 길이가 동일한 경우는 확인

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 (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 ...)을 반환한다는 사실에서 파생하는 방법을 볼 수 있습니다 누락 된 링크를 확장 점차

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

와 함께 시작하면 그 다음 수 그 {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 

을 다음 (Same m)eq에 다시 유형 검사의 결과를 보면서 변경 : 거기에 무슨 일이 일어나고 있는지 볼 수 Just ... 지점에 구멍을 추가처럼.

- + 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) 경우는 다음과 같이이다 : 다음 eq 경우는이처럼

- + 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이 동일하다는 것을 증명합니다.