問題タブ [idris]

Idris/Haskell では、型に注釈を付け、Vect などの GADT コンストラクターを使用することでデータのプロパティを証明できますが、これにはプロパティを型にハードコーディングする必要があります (たとえば、Vect は List とは別の型でなければなりません)。たとえば、コンストラクターをオーバーロードしたり、効果の流れで何かを使用したりすることにより、プロパティのオープンセット (長さと移動平均の両方を保持するリストなど) を持つ型を持つことは可能ですか?

私は依存型に不慣れで、Haskell の経験があり、ゆっくりと Idris を学んでいます。演習として、ハフマン エンコーディングを書きたいと思います。現在、コード ツリーの「平坦化」によってプレフィックス コードが生成されるという証明を書こうとしていますが、量指定子に行き詰まっています。

あるリストは別のリストのプレフィックスであるという単純な帰納命題があります。

1. これは有効なアプローチですか？または、「xs ++ zs = ysのようなzsがある場合、 xsはysのプレフィックスです」のようなものが良いでしょうか?

2. 「forall」量指定子を導入するのは正しい方法でしたか (私が理解できる限り、Agda では のようなものになりますpNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x :: xs) (y :: ys))? pNext の最初の引数は暗黙的であるべきですか? 2 つのバリアントの意味上の違いは何ですか?

次に、どの要素も別の接頭辞を形成しないベクトル用に作成したいと思います。

空ベクトルには接頭辞がありません:

要素 x、ベクトル xs、および xs のどの要素も x の接頭辞ではない (およびその逆) という証明が与えられると、x :: xs はそのプロパティを保持します。

これは無効な型であり、最初のものを処理した後に修正したいと考えていますが、pvNext の量指定子について同様の質問があります。

ありがとうございました。

次のように、型が関数型かどうかを判断する関数が必要です。

Trueただし、これはすべての入力に対して返されます。どうすればこれを機能させることができますか？

関数を作成しようとしています

reflect私は戦術を使ってそれを試しました：

tしかし、これは変数自体に反映されます:

私は関数を書くことができます

そして自明に証明します：

ここまでは順調ですね。ここで、この関数を一般化して、負の指数で機能するようにします。もちろん、逆を提供する必要があります。

次に、同様のステートメントを証明しようとします。

しかし、Idris は の適用を評価することを拒否しpowApplyI、 のタイプを?powApplyIZero_rhsas powApplyI (Pos 0) i x = x(yes, Zis changed to 0) のままにします。ポイントフリーではないスタイルで書き、モディファイアを使用しpowApplyIて独自のスタイルを定義しようとしましたが（これはわかりません）、どちらも機能しませんでした。の最初のケースを調べて証明を処理しないのはなぜですか?ZZ%elimpowApplyI

イドリスのバージョン: 0.9.15.1

ここにいくつかのことがあります：

最初の証明はうまくいきましたが、?powApplyZFZero_rhs頑固に型を保持していpowApplyZF (Pos 0) f x = xます。明らかに、ZZ（または私の使い方に）問題があります。