183

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

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

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

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

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

4

2 に答える 2

206

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 経由です。C 経由で Idris と同じバックエンドを使用する Agda 用の実験的なバックエンドがあります。Idris の主な目標は、常に効率的なコードを生成することです。現在よりもはるかに優れたコードを作成できますが、現在取り組んでいます。

Agda と Idris の型システムは、多くの重要な点でよく似ています。主な違いはユニバースの扱いにあると思います。Agda にはユニバース ポリモーフィズムがあり、Idris には累積性があります (Set : Setこれがあまりにも限定的であり、証明が不健全であることを気にしない場合は、両方を使用できます)。

于 2012-02-27T23:35:50.667 に答える
53

Idris と Agda のもう 1 つの違いは、Idris の命題等価性が異種混合であるのに対し、Agda の命題等価性は同種であることです。

言い換えれば、イドリスにおける平等の推定上の定義は次のようになります。

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

アグダにいる間、それは

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

Agda 定義の l は、Edwin が回答で言及しているユニバース ポリモーフィズムに関係しているため、無視できます。

重要な違いは、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

および次のタイプとの連結:

(++) : 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

等式の左側には type がVect (n + (m + o)) aあり、右側には typeがあるため、このステートメントは同種の等式の下ではナンセンスVect ((n + m) + o) aです。これは、異質な平等を伴う完全に賢明な声明です。

于 2014-01-08T10:02:05.743 に答える