私は依存型プログラミングに取り組み始めており、Agda 言語と Idris 言語が Haskell に最も近いことがわかったので、そこから始めました。
私の質問は、これらの主な違いは何ですか？ 両方の型システムは同じように表現できますか？ 包括的な比較と利点についての議論があれば素晴らしいと思います。
私はいくつか見つけることができました:
- IdrisはHaskell風の型クラスを持ちますが、Agdaはインスタンス引数を採用しています。
- Idrisにはモナド記法と応用記法が含まれている
- どちらも何らかの再バインド可能な構文を持っているようですが、同じかどうかはよくわかりません。
編集: この質問の Reddit ページにさらにいくつかの回答があります:http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
ベストアンサー1
私はIdrisを実装した経験があるので、この質問に答えるのに最適な人物ではないかもしれません。FAQ -http://docs.idris-lang.org/en/latest/faq/faq.html- それについては何か言いたいことがあるのですが、もう少し詳しく説明します。
Idris は、定理証明よりも汎用プログラミングをサポートするように根本から設計されており、型クラス、do 記法、イディオム括弧、リストの内包表記、オーバーロードなどの高レベル機能を備えています。Idris は高レベルプログラミングを対話型証明よりも優先しますが、Idris は戦術ベースのエラボレーター上に構築されているため、戦術ベースの対話型定理証明器 (Coq に少し似ていますが、少なくとも現時点ではそれほど高度ではありません) へのインターフェイスがあります。
Idris がサポートしようとしているもう 1 つのことは、組み込み DSL 実装です。Haskell では do 記法でかなりの距離を移動できますが、Idris でも同じことができます。ただし、必要に応じて、アプリケーションや変数バインディングなどの他の構成要素を再バインドすることもできます。詳細については、チュートリアルまたはこの論文を参照してください。http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf
もう 1 つの違いはコンパイルにあります。Agda は主に Haskell 経由で行われ、Idris は C 経由で行われます。Agda には、Idris と同じバックエンドを C 経由で使用する実験的なバックエンドがあります。それがどの程度よくメンテナンスされているかはわかりません。Idris の主な目標は常に効率的なコードを生成することです。現在よりもずっと優れたコードを作成できますが、現在取り組んでいます。
AgdaとIdrisの型システムは、多くの重要な点で非常に似ています。主な違いはユニバースの扱い方にあると思います。Agdaにはユニバース多態性があり、Idrisには累積性Set : Set(これがあまりにも制限的であり、証明が不健全であっても構わないのであれば、両方を使用することもできます)。