問題タブ [agda]

私はagdaを学ぼうとしています。しかし、問題が発生しました。Agda wiki で見つけたすべてのチュートリアルは、私には複雑すぎて、プログラミングのさまざまな側面をカバーしています。agda の 3 つのチュートリアルを並行して読んだ後、簡単な証明を書くことができましたが、実際のアルゴリズムの正確さのためにそれを使用するにはまだ十分な知識がありません。

このテーマに関するチュートリアルをお勧めできますか? Learn Yourself a Haskell に似ていますが、Agda 用です。

私は依存型プログラミングに飛び込み始めており、Agda 言語と Idris 言語が Haskell に最も近いことがわかったので、そこから始めました。

私の質問は、それらの主な違いはどれですか? 型システムは両方で同じように表現できますか? 包括的な比較と利点についての議論を行うことは素晴らしいことです.

私はいくつかを見つけることができました：

• Idris には Haskell 風の型クラスがありますが、Agda にはインスタンス引数があります。
• Idris には、単項および適用可能な表記法が含まれています
• どちらも、ある種の再バインド可能な構文を持っているようですが、同じかどうかはよくわかりません。

編集：この質問のRedditページには、さらにいくつかの回答があります：http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

私が関数を持っていると仮定します (それは実際に名前が言うことを行います):

ここで、返された従属ペアをどうにかして処理したいと思います。私は簡単なhead関数を書きました：

もちろん、これは完全に機能します。しかし、それは私が疑問に思いました:関数がでのみ呼び出される可能性があることを確認できる方法はありますn ≥ 1か?

理想的には、私は関数を作りたいhead : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → Aです; nで使用すると範囲外になるため、失敗しますIsTrue。

御時間ありがとうございます！

IsTrue次のようなものです：

Agdaを証明システムとして使用する上で役立つ情報をたくさん見つけました。Agdaを使用して使用可能なプログラムを作成することに関する情報はほとんど見つかりませんでした。Agdaの最新バージョンでコンパイルされる「helloworld」の例すら見つかりません。

それで、

1. プログラミング言語としてのAgdaに関する優れたチュートリアルはありますか？

2. プログラミング言語としてそれらを使用するためのより成熟したドキュメントを持っている同様の性質（怠惰な機能依存型）の他の言語はありますか？（Coqに関する多くの優れたドキュメントを見つけましたが、ここでも「HelloWorld」はありません）。

標準ライブラリを使用するAgdaプログラムをコンパイルすると、コンパイラは次のような行を出力するのに長い時間を費やします。

それらを安全に「スキップ」する理由は、それらがすでにコンパイルされているためだと思います（ディレクトリにはすでに.agdaiファイルがあります）。しかし、それでもそれらをスキップするのに多くの時間を費やし、コンパイルには1分以上かかります。

すべてのコンパイルでこの余分な作業をすべて回避する方法はありますか？

未解決のメタの原因を突き止める最善の方法は何ですか? 解決可能なすべての周囲のワイルドカードを拡張することにより、すべての未解決のメタ (および未解決のメタのみ) を穴に変える方法はありますか?

他に何もないとしても、未解決のメタを穴に変更すると、未解決のメタに関するメッセージが消えますか? それなら、メッセージが消えるまですべてのワイルドカードとすべての暗黙の引数を穴に変更してから、どれが問題を引き起こしているかを突き止めることができると思います...

と のいくつかのプロパティを証明していましたが、このプロパティに出くわすfilterまでmap、すべてがうまくいきました: filter p (map f xs) ≡ map f (filter (p ∘ f) xs)。関連するコードの一部を次に示します。

≡-Reasoningさて、モジュールを使って証明を書くのが大好きなので、最初に試したことは次のとおりです。

しかし、残念ながら、それはうまくいきませんでした。1時間試した後、最終的にあきらめて、次のように証明しました。

≡-Reasoningなぜ通り抜けることがうまくいかなかったのかまだ興味があるので、私は非常に些細なことを試しました：

しかし、タイプチェッカーは私に同意しません。現在の目標は残っているように見えます.でfilter p (f x ∷ map f xs) | p (f x)パターンマッチしたとしても.p (f x)filterf x ∷ filter p (map f xs)

これを機能させる方法はあり≡-Reasoningますか？

ありがとう！

Windows 7 64 ビット PC で Agda を実行できません。次のコマンドを実行してみました。

と

どちらも機能しますが、まだemacsでうまくいかないようです。誰か助けてもらえますか? ここからワンクリック インストーラーを試してみましたが、うまくいかないようです。

商型に対して複数の引数を持つ関数を定義しようとしています。カリー化を使用すると、点ごとの積setoidで関数を定義する問題を減らすことができます。

私の質問は、×-quot拡張性を仮定せずにの健全性を証明する方法はありますか？

この haskell データ型を agda コードに変換する必要があります。

これは私がこれまでに持っているものです:

しかし、私はこのエラーを受け取ります:「セットは関数型である必要がありますが、true がセット型の関数への有効な引数であることを確認するときではありません」。Set を別のものに変更する必要があると考えていますが、これがどうあるべきか混乱しています。