問題タブ [idris]

私はストリームに似たものを書いてきました。各ファンクターの法則を証明することはできますが、それが合計であることを証明する方法がわかりません。

与えます:

全体性チェッカーも通過するcodataに対するファンクターの法則を証明するトリックはありますか?

Idris で次のような関数を作成しようとしました。

Charこれは、文字列を最初の文字列と残りの文字列に「un-cons」し、Nothing空の場合は戻ります。

だから私はこれを書きましたが、失敗しました：

それで、私はこれを試しましたPrelude.Strings。

これは問題なくコンパイルおよび実行されました。

私の質問は、なぜwithこのように文字列を分割するためにその規則を使用しなければならないのですか? また、元の方法が失敗するのはなぜですか?

注: 申し訳ありませんが、現時点ではインタープリターにアクセスできないため、エラー メッセージをここに書き込むことはまだできません。

これは、このフォローアップの質問のフォローアップです。Zipp は、折り畳みを使用した zip の非再帰的、非パターン マッチング実装です。型なしラムダ計算では、次のようになります。

Haskell では、@András_Kovács によって証明されているように、この用語を入力することは不可能ですが、Agda は少し複雑ではありますが、それを行うことができます。このプログラムを Idris でエレガントに定義することは可能ですか?

私はどのようにinorder + preorderが一意のバイナリツリーを構築するのかを見ていましたか? Idris で正式な証明を書くのは楽しいだろうと考えました。残念ながら、ツリー内の要素を検索する方法が、順序通りに検索する方法に対応していることを証明しようとして、かなり早い段階で行き詰まってしまいました (もちろん、事前順序検索でもそれを行う必要があります)。 . どんなアイデアでも大歓迎です。私は完全な解決策には特に関心がありません。それ以上のことは、正しい方向への出発点に役立つだけです。

与えられた

少なくとも 2 つの方法でリストに変換できます。

また

2 番目のアプローチはほとんどすべてを困難にするように思われるため、私の努力のほとんどは最初のアプローチに集中しています。ツリー内の場所を次のように説明します。

inorder（ の最初の定義を使用して）書くのはとても簡単です

結果はかなり単純な構造になり、証明にはかなり適しているようです。

のバージョンを書くこともそれほど難しくありません。

inorderThenInTree残念ながら、これまでのところ、の逆であることを証明できた のバージョンを書く方法を思いつきませんでしinTreeThenInorderた。私が思いついた唯一の用途

私はそこを通り抜けようとしてトラブルに遭遇します。

私が試したいくつかの一般的なアイデア：

1. Vect代わりにを使用Listすると、左側にあるものと右側にあるものを理解しやすくなります。その「緑のスライム」にはまってしまいました。

2. 木の根元での回転が十分に根拠のある関係につながることを証明するまで、木の回転をいじってみました。（これらの回転について何かを使用する方法を理解できなかったため、以下の回転をいじりませんでした）。

3. ツリー ノードに到達する方法に関する情報でツリー ノードを装飾しようとしています。そのアプローチで何か面白いものを表現する方法が思いつかなかったので、私はこれにあまり時間をかけませんでした。

4. そうする関数を構築しながら、開始した場所に戻るという証拠を構築しようとしています。これはかなり厄介になり、どこかで行き詰まりました。

Haskell では、次のtypeように、型ファミリーを作成する宣言を含む型クラスを作成できます。

そして、次のようにインスタンスを記述します。

Idris で型クラスと型レベル関数を作成できることは承知していますが、メソッドは型自体ではなく、指定された型のデータを操作します。

上記のような Idris で型クラスに制約のある型ファミリを作成するにはどうすればよいですか?

Edwin C. Bradyによる Idris の効果に関する論文「代数効果と従属型を使用したプログラミングと推論」には、次の (参照されていない) 主張が含まれています。

[効果とモナド変換子] は力が同等ではありませんが — モナドとモナド変換子はより多くの概念を表現できます — 多くの一般的な効果的な計算がキャプチャされます。

モナドトランスフォーマーによってモデル化できるが、効果ではモデル化できない例は何ですか?

Idris をいじり始めたばかりで、いくつかの Haskell マシンにシューホーニングしてみました。

ただし、追加のパラメーターを使用して、モナドとして出力を生成できるように一般化Auto a bしたいと思います。私の直感では、 type が含まれるはずでしたが、タイプチェッカーはそれが一致しないと不平を言います。だから私はそれをもう少しポリモーフィックなままにしてみました：AutoM m a bmmType -> Type(Type, Type) -> Type

これは少なくとも型チェックを行います。しかし、私がしようとすると：

しかし、それは良くありません:

そして、型エラーの意味がよくわかりません。の定義で がどこにも使用されていないのに、一体なぜ の型(a, b)が言及されるのでしょうか? 定義自体がすでに間違っている気がしますが、その理由や方法はよくわかりません。aconst_autoAutoM