2017-10-25 5 views
0

を失敗した実装はその関連性がない場合でも、次の関数を考えてみてください:イドリス - 平等の主張は

vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n)) 
vectTranspose {n = Z} [] = [[],[],[]] 
vectTranspose {n = (S len)} (x :: xs) with (natToFin len (S len)) 
    | Just l = let 
     previous = map (map weaken) (vectTranspose xs) 
    in updateAt x (l ::) previous 

私はREPLでvectTransposeを計算しようとした場合、予想通り、私は[[],[],[]]を取得します。私は自分のコードに次の

emptyTest : vectTranspose [] = [[],[],[]] 
emptyTest = Refl 

のような平等のアサーションを追加する場合

はまだ、私はコンパイルエラーを取得:

When checking right hand side of emptyTest with expected type 
     vectTranspose [] = [[], [], []] 

Type mismatch between 
     [[], [], []] = [[], [], []] (Type of Refl) 
and 
     vectTranspose [] = [[], [], []] (Expected type) 

Specifically: 
     Type mismatch between 
       [[], [], []] 
     and 
       vectTranspose [] 

私は何かが足りないのですか?私はアサーションの中に何らかの形で[[],[],[]]の型を指定すべきですか?

答えて

2

イドリスは

Specifically: 
    Type mismatch between 
      [[], [], []] 
    and 
      vectTranspose [] 

のタイプについて不平を言うということは、vectTransposeがタイプにまだあるし、解決されていないことを示しています。 vectTransposeは合計ではなく、実際にそれがない場合はそれはケースです:あなたはすべてのMaybe例をカバーしていないため

VecTest.vectTranspose is possibly not total due to: 
with block in VecTest.vectTranspose, which is not total as there are missing cases 

起きています。

簡単な解決策は、小さなヘルパー関数を作成することができます

total 
natToFin': (n: Nat) -> Fin (S n) 
natToFin' Z = FZ 
natToFin' (S k) = FS (natToFin' k) 

total 
vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n)) 
vectTranspose {n = Z} [] = [[], [], []] 
vectTranspose {n = (S len)} (x :: xs) with (natToFin' len) 
    vectTranspose {n = (S len)} (x :: xs) | l = let 
      previous = map (map weaken) (vectTranspose xs) 
      in updateAt x (l ::) previous 
+0

感謝! 'Nothing'ケースを追加すると動作します。それでも 'natToFin len(S len)'は常に 'Just l'なので' Nothing'の場合は到達できません。私が '|不可能なものはありません。問題が残っています。決して達成されない本当の 'Nothing'ケースを提供せずに動作させる方法はありますか? – marcosh

+0

私はかなりエレガントなアプローチがあると確信していますが、単純なものはあなたのケースをカバーする小さなヘルパーを提供することです。私はあなたの機能が何をしているのかも分かっていないので、一日の終わりにはまったく別のもので終わる可能性があります。 – Markus