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

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

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

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

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

Idrisチュートリアル、Agdaチュートリアル、および他の多くのチュートリアルスタイルのペーパーと、まだ学習していないことへの終わりのない参照を含む入門資料があります。私はこれらすべての真っ只中にいるようなもので、ほとんどの場合、数学表記と新しい用語が説明なしに突然現れることに固執しています。おそらく私の数学は最悪です:-)

依存型プログラミングにアプローチするための統制のとれた方法はありますか？Haskellを学びたいときのように、「自分自身にHaskellを教えて」から始め、Scalaを学びたいときは、Oderskyの本から始めます。Rubyの場合、変異したバグを含む奇妙なチュートリアルを読みます。しかし、私は彼らの本でアグダやイドリスを始めることはできません。彼らは私の頭上にあります。私はCoqを試してみましたが、そのすべてを証明するスタイルで立ち往生しました。アグダは巨大な数学のバックグラウンドを必要とし、イドリスは、まあ、今はそれを残しましょう！

私は静的型システムをよく理解しています。私はScalaにある程度精通しており、必要に応じてHaskellを使用できます。私は関数型パラダイムを理解し、それを日常的に使用しています。代数的データ型とGADT（実際には非常にスムーズに）を理解し、最近ラムダキューブを理解することができました。しかし、私は数学と論理の部分が不足しています。

私が話しているのは、次のことを定義することはできないということです。

GHCはこれを単純な関数に脱糖するだけであり、これを解決する慣用的な方法は次のようになります。

これを書いた後、私はそれがあまり好きではありません...このタイプクラスは脱糖プロセスの一部ではありませんでしたか？

Aeson JSON解析を書いているときに、その考えが浮かびました。すべてのデータ型のインスタンスを導出するのFromJSONが簡単すぎる場合は、すべてを手作業で書き出す必要がありました（現在は1,000行を超えてカウントしています）。nameデータレコードのような、または単にデータレコードに名前を付けるvalueことは、それほど珍しいことではありません。

http://www.haskell.org/haskellwiki/Performance/Overloadingは、関数のオーバーロードが実行時のオーバーヘッドをもたらすと述べています。しかし、実際には、コンパイラがコンパイル時にこれを解決できず、内部で異なる名前を付けることができない理由がわかりません。

2012年のこのSOの質問は、多かれ少なかれ歴史的な理由を述べており、2006年のメールスレッドを指しています。最近何か変わったことはありますか？

実行時のオーバーヘッドがいくらかあるとしても、ほとんどの人は気にしないでしょう。ほとんどのコードはパフォーマンスが重要ではないからです。

これを実際に可能にする隠された言語拡張機能はありますか？繰り返しますが、よくわかりません...しかし、イドリスは実際にこれを行っていると思いますか？

研究に使用され、おそらくそれを汎用/「実世界」アプリケーションに適用できるイドリスの例はありますか?

私は Haskell にある程度精通しており、Idris はそこからかなり借用しているようです。公式の FAQ/ドキュメントはかなり優れていますが、調査するためのより大きな例がいくつかあると非常に役立ちます。目標は、実用的なソフトウェア開発に Idris を使用することです。ティア。

testMult : mult 3 3 = 9人が住んでいるとイドリスに証明してもらいたい。

残念ながら、これは次のように入力されます

次のように回避できます。

に似た何かを行う方法はありmult (3 : Nat) (3 : Nat) = (9 : Nat)ますか?

Cayenneの例を Idris に翻訳しようとしています- 依存型paperを持つ言語 です。

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

でのパターン マッチングがすぐに複雑になったため、パターン マッチングを容易にするために、formatList Char引数の代わりにを使用しています。StringString

残念ながら、意味を理解できないエラーメッセージが表示されます。

'%' :: ...と の 3 つの要素 ( を含むもの) を持つすべてのパターン マッチ ケースをコメント アウトするPrintfTypeとprintf、コードはコンパイルされます (ただし、明らかに興味深いことは何もしません)。

動作するようにコードを修正するにはどうすればよいprintf "the %s is %d" "answer" 42ですか?

Prelude の組み込み関数の定義を調べたいので、興味があります。

私はそれを検索しましたが、コンパイル済みのファイルが ~/.cabal/share/idris... にしか見つかりませんでした。

Coqを使用して認定プログラムを設計することについて話しているいくつかの異なる研究グループと、少なくとも1冊の本を見ています。認定プログラムの定義についてコンセンサスはありますか? 私が言えることは、それが本当に意味することは、プログラムが完全で型が正しいことが証明されたということだけです。現在、プログラムの型は、空でないこと、ソートされていること、すべての要素が 5 以上であることを証明するリストなど、非常にエキゾチックなものである可能性があります。ただし、最終的には、認定されたプログラムは、Coq が完全で型安全であることを示すものにすぎません。 、すべての興味深い質問は、最終的なタイプに何が含まれていたかに要約されますか?

編集 1

wjedynakの回答に基づいて、以下の回答にリンクされているXavier Leroyの論文「現実的なコンパイラの正式な検証」を見ました。これにはいくつかの良い情報が含まれていると思いますが、この一連の研究のより有益な情報は、Sandrine Blazy と Xavier Leroy によるC 言語の Clight サブセットのための機械化されたセマンティクスの論文で見つけることができると思います。これは、「Formal Verification」ペーパーが最適化を追加する言語です。その中で、Blazy と Leroy は Clight 言語の構文とセマンティクスを提示し、セクション 5 でこれらのセマンティクスの検証について説明します。セクション 5 には、コンパイラーの検証に使用されるさまざまな戦略のリストがあります。. これらは：

1. マニュアルレビュー
2. セマンティクスのプロパティの証明
3. 検証済みの翻訳
4. 実行可能なセマンティクスのテスト
5. 代替セマンティクスとの同等性

いずれにせよ、おそらく追加できるポイントがあり、もっと詳しく聞きたいと思っています.

認定プログラムの定義は何かという最初の質問に戻りますが、それはまだ少し不明確です。Wjedynak は一種の答えを提供しますが、実際には Leroy の作業には、Coq でコンパイラを作成し、ある意味でそれを認定することが含まれていました。理論的には、C->Coq->証明に進むことができるようになったため、C プログラムに関することを証明できるようになりました。そういう意味では、こういうワークフローもありそうですね。

1. X言語でプログラムを書く
2. Coqまたはその他の証明補助ツールでのステップ1のプログラムのモデルの形式。これには、Coq でプログラミング言語のモデルを作成することが含まれる場合もあれば、プログラムのモデルを直接作成すること (つまり、Coq でプログラム自体を書き直すこと) が含まれる場合もあります。
3. モデルに関するいくつかのプロパティを証明します。多分それは価値についての証明です。たぶん、それはステートメントの等価性の証明です（3 = 1 + 2またはf（x、y）= f（y、x）など）。
4. 次に、これらの証明に基づいて、元のプログラムを認定済みと呼びます。

あるいは、プルーフ アシスタント ツールでプログラムの仕様を作成し、仕様に関するプロパティを証明できますが、プログラム自体は証明できません。

いずれにせよ、誰かが定義を持っているなら、私はまだ別の定義を聞くことに興味があります.