8

これをコンパイルしたい：

foo: Vect n String -> Vect n String
foo {n} xs = take n xs

コンパイラは と統合できないため、これはコンパイルに失敗しnますn + m。これは for Vect の署名によるものであることは理解していますがtake、 if で統合できることをコンパイラに示す方法がわかりませんm = 0。

4

2 に答える 2

6

前の回答に追加するために、もう 1 つの可能性はplusZeroRightNeutral、ライブラリの既存のレンマを使用してインラインで書き換えを行うことです。

foo: Vect n String -> Vect n String
foo {n} xs = let xs' : Vect (n + 0) String
                     = rewrite (plusZeroRightNeutral n) in xs in
                 take n xs'

mIdris が統一に苦労しているのは、take の適用でを推論したくないからです。

take : (n : Nat) -> Vect (n + m) a -> Vect n a

Vect n Stringが必要な場所に を与えました-Vect (n + m) aは型コンストラクタであるため、aとをうまく統合しましたが、一般に、関数を反転できないため、と統合することを望んでいません。あなたも私もそれがゼロでなければならないことはわかりますが、イドリスはそれほど賢くありません。StringVectnn + mm

于 2014-07-27T19:45:24.977 に答える
3

イドリスはそれnをn + m知らないので合体できないn = n + 0。それを手動で証明して、彼を助ける必要があります。

まず、なぜこの証明が必要なのか。その理由は、次のことをtake期待しているためですVect (n+m) a。

Idris> :t Vect.take
Prelude.Vect.take : (n : Nat) -> Vect (n + m) a -> Vect n a

したがって、これは型チェックになります

foo: Vect (n + 0) String -> Vect n String
foo {n} xs = take n xs

Vect n aに変換する方法が必要ですVect (n + 0) a:

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n+Z) a

関数で可能replaceです：

Idris> :t replace
replace : (x = y) -> P x -> P y

しかし、今はその証拠が必要ですn = n + 0。ここにあります（コードの残りの部分を含む）：

plusAddZero : (n : Nat) -> n = n + 0
plusAddZero = proof
  intros
  rewrite (plusCommutative n 0)
  trivial

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n + 0) a
addNothing {n} {a} = replace {P = \m => Vect m a} (plusAddZero n)

foo : Vect n String -> Vect n String
foo {n} xs = Vect.take n (addNothing xs)

このような単純な機能には多すぎるようです。誰かがより簡潔な解決策を示してくれることを願っています。

于 2014-07-24T21:32:31.910 に答える