检查向量的长度相等

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合作时，发现有用的东西是当你不确定某些东西而不是解决问题时添加漏洞。比如增加一个洞Just ...分支，看看发生了什么事情有：

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和背部，同时在看的类型检查的结果。在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是平等的。