リストの平等は、この演習を提示イドリスと

Question

型駆動開発を機能定義：私は「ので、私はEqList (x :: xs) (x :: ys)でxを推論

data EqList : (xs : List a) -> (ys : List a) -> Type where 
    Same : (xs: List a) -> EqList xs xs 

sameS : (xs : List a) -> (ys : List a) -> (x: a) -> (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
sameS xs xs x (Same xs) = Same (x :: xs) 

same_cons : {xs : List a} -> {ys : List a} -> (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
same_cons {xs} {ys} eq = sameS xs ys _ eq 

：

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys 

はしかし、私は経由でそれを実装しようとしましたどのようにxを取得する混乱m xsとysが空の場合混乱しています。また

、上記のコンパイルが、私はそれを呼び出すようにしようとしたとき、それは失敗しました：

*Exercises> same_cons (Same [1,2,3]) 
(input):Can't infer argument x to same_cons 

Answer 1

それを制約するための呼び出しsame_cons (Same [1,2,3])に情報がないので、暗黙の引数xをご利用の場合には推測できません何かに。結果のタイプを修正すると、xという選択肢が表示されます。

λΠ> the (EqList [0,1,2,3] [0,1,2,3]) (same_cons (Same [1,2,3])) 
Same [0, 1, 2, 3] : EqList [0, 1, 2, 3] [0, 1, 2, 3] 

x:xsため[0,1,2,3]の選択は0とxを統一以来。

eq引数の型がxsとysので、あなたはイドリスはそれを推測させることができますを決定するため、ところであなたはsame_consの定義を簡略化することができます。

same_cons : (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
same_cons eq = sameS _ _ _ eq 

Answer 2

x取得する方法について明確にするために：に小文字で すべてを型格解消は、明示的でない場合は暗黙の引数になります。だから、

same_cons : {xs : List a} -> {ys : List a} -> 
      (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 

は

xが隠れているところだ

same_cons : {a : Type} -> {x : a} -> {xs : List a} -> {ys : List a} -> 
      (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 

と同じです。したがって、定義の左側に{x}を使用して取得することができます。あるいは、Idrisがすべてのものを扱い、Cactusの定義を使用させるだけです。引数の将来の問題については、REPL内の:set showimplicitsを使用して、タイプを尋ねるときにすべての暗黙の引数を表示することができます。 :t same_cons。

そして、イドリスは暗黙の引数の値を推測することができないとき、あなたはサボテンのような結果の種類を与えることによって、それを助けるやったか、値に暗黙の引数を設定することができます。

*> same_cons {x=0} (Same [3,2,5]) 
Same [0, 3, 2, 5] : EqList [0, 3, 2, 5] [0, 3, 2, 5]