問題タブ [idris]

この記事の精神に基づいて、依存型のラムダ計算を実装しました。公理。ただし、より複雑なことを行うために誘導型を追加したいと考えています。

その方法は2つ考えています

• Fin-N、Product、および W-type を紹介し、それらで誘導型を表します。
• 帰納公理と再帰公理を生成します。

私はどちらの方法も好きではありません。最初のものはレベルが低すぎて、高級言語からコア言語に変換するのにかなりの労力が必要です。2 番目の方法は、複雑な帰納型の再帰原理の生成には多くのコーナー ケース (正/負の発生) があるため、非常に手間がかかり、エラーが発生しやすくなります。

これはどのように行うことができますか？タイプは、Coq、Agda、Idris などの既存のシステムでどのように実装されていますか?

Idris で String を Integer または Natural に変換する最良の方法は何ですか?

標準ライブラリはまだ進行中の作業であることを知っているので、答えが標準ライブラリに追加する必要がある場合は、それを試してみるのも問題ありませんが、まだ方法がないことを確認する前に.

ユーザーからインデックスを読み取りたい場合、私が思いつくことができる最善の方法は次のとおりです。

しかし、この方法では、キャストからの失敗の兆候はありません。indexAsString が Integer に変換できる形式ではない可能性があるという事実だけでなく、実行時に失敗することさえなく、「不正なキャスト」の結果として 0 が生成されます。

より良い方法があることを教えてください、および/または正しい方向に向けてください。

余談ですが、Idris に Read 型クラスがない特別な理由はありますか? それともまだ入っていないだけですか？

事前にt​​hx。

私が理解している限りでは、ほとんどすべての依存型付き言語は、変換可能性のために弱い頭部正規形を使用しています。なぜそうなのですか？変換可能性をチェックするだけで十分なのはなぜですか (私には十分ではないようです)。これについて何を読むことをお勧めしますか?

依存型型理論には、等価型があります。通常、このタイプが定義されると、いくつかのユーティリティ、つまり cong と subst が導入されます。彼らはどれほど表現力豊かですか？彼らとの対等性のために、エリミネーターで表現できることをすべて表現することは可能ですか?

私がそれを正しく理解していれば (主にapplyTactic関数の存在から)、Idris で定理証明用のカスタム タクティクスを作成することが可能です。その方法を学ぶために使用できる例は何 (またはどこ) ですか?

ここで著者は次のように主張します。

TLS 仕様を形式化し、実装がそれと一致していることを証明することは、実装が論理的に正しいことを示すだけです。ただし、実装が安全であることは示されません。実装は、論理的には正しくても、サイドチャネル攻撃 (特にタイミング攻撃) に対して脆弱になる可能性があります。

私の質問は次のとおりです。 「安全な言語」(Haskell、Idris) で検証済みの SSL/TLS 実装を使用したり、定理証明者 (Coq、Agda) でチェックしたりしても、ハートブリード攻撃に対して脆弱でしたか?

AgdaとIdrisはどちらも、 type の値に対するパターン マッチングを事実上禁止していますType。Agda は常に最初のケースで一致するようですが、Idris はエラーをスローするだけです。

では、なぜタイプケースが悪いのでしょうか? それは一貫性を壊しますか？このトピックに関する多くの情報を見つけることができませんでした。