AgdaとIdrisの違い

Question

私は依存型プログラミングを開始しており、AgdaとIdrisの言語はHaskellに最も近いことが分かりました。

私の質問は：それらの主な違いは何ですか？型システムは両方とも同等にexpresiveですか？包括的な比較と利点についてのディスカッションを行うことは素晴らしいことです。

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

• イドリスは
• イドリスはモナドとApplicativeの表記
• それらの両方に思えるが含まAgdaは、インスタンス引数で行くのに対し、ラ・ハスケルàクラスを入力しています彼らが同じであるかどうか本当に確かではありませんが、再バインド可能な構文のいくつかの並べ替えを持っています。

---

編集：いくつかのより多くの答えがこの質問のRedditのページにあります。http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Answer 1

私はおそらくだイドリスを実装したとして、私は、これに答えるための最良の人ではないかもしれません少し偏っている！ FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - これには何か言いたいことがありますが、少し拡張してください：

Idrisは、定理証明の前に汎用プログラミングをサポートするように設計されており、型クラス、表記、イディオムブラケット、リスト内包、オーバーロードなどがあります。 Idrisは、対話形式の証明に先んじて高度なプログラミングを行いますが、Idrisは戦術ベースの精巧さの上に構築されているため、戦術ベースの対話定理証明（Coqのようなビットですが、少なくともまだ進んでいません）

さらに、Idrisがサポートすることを目指しているもう1つの点は、組み込みDSL実装です。ハスケルを使うと、do not表記で長い道のりを得ることができますし、Idrisでも可能ですが、必要に応じてアプリケーションや変数バインディングなどの他の構造を再バインドすることもできます。この詳細については、このチュートリアルまたはこのペーパーの詳細を参照してください。http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

別の違いがあります。 Agdaは主にHaskell、Idris経由でCを経由します。Agdaのバックエンドは、Idrisと同じバックエンドをC経由で使用していますが、私はそれがどれほど整備されているかはわかりません。 Idrisの主な目標は、常に効率的なコードを生成することです - 私たちは現在よりも多くのことを行うことができますが、私たちはそれに取り組んでいます。

AgdaとIdrisのタイプシステムは、多くの重要な点でかなり似ています。主な違いは、宇宙の取り扱いにあると思います。 Agdaには宇宙多形性があります。Idrisはcumulativityです（これはあまりにも制限があり、あなたの証明が不健全であるかもしれないことに気付かないと、Set : Setを両方持つことができます）。

Answer 2

IdrisとAgdaの他の違いの1つは、Idrisの命題均等性は異種であり、Agdaは均質であるということです。すなわち

、イドリスに平等の推定上の定義は次のようになります

data (=) : {a, b : Type} -> a -> b -> Type where 
    refl : x = x 

Agdaで、それはAgdaのdefintion中のLがのように、無視することができる

data _≡_ {l} {A : Set l} (x : A) : A → Set a where 
    refl : x ≡ x 

でありますエドウィンは彼の答えで言及している宇宙の多形性と関係があります。

重要な違いは、Agdaの等価型は引数としてAの2つの要素をとり、Idrisでは異なる型の2つの値をとることができるという点です。

つまり、Idrisでは、種類の異なる2つのものが同等であると主張することができますが、Agdaではその言葉はナンセンスです。

これは、タイプ理論、特にホモトピー型理論を使用した作業の実現可能性に関して、重要かつ広範囲の結果をもたらします。このために、異質な平等は、HoTTと矛盾する公理を必要とするため、機能しません。他方では、均質な平等で直接記述することができない異質な平等を持つ有用な定理を述べることは可能である。

おそらく最も簡単な例は、ベクトル連結の結合性です。次の型を持つ

data Vect : Nat -> Type -> Type where 
    Nil : Vect 0 a 
    (::) : a -> Vect n a -> Vect (S n) a 

と連結：thusly定義されたベクトルと呼ばれる長さ、インデックス付きのリストを考えると

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

我々はそれを証明することがあります：

concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> 
       xs ++ (ys ++ zs) = (xs ++ ys) ++ zs 

この文は、下のナンセンスであります等価性の左辺は型がVect (n + (m + o)) aで、右辺が型がVect ((n + m) + o) aであるためです。これは異質の平等を持つ完璧に合理的な声明です。