依存型入力の限界は何ですか?

依存型はプログラムの振る舞いについて多くの望ましい保証を提供することができるようです。どのような種類のプログラムプロパティが保証できないのですか(計算上実行不可能なもの以外に)?プログラムの計算可能なプロパティをモデル化できる、さらに強力な、または一般的な型のシステムはありますか?

ベストアンサー

ほとんどの依存型理論から明らかに欠けている特徴の1つは、部分構造推論の能力です。

AgdaやCoqのようなシステムによって保証されるのは非常に拡張的な傾向があります。つまり、演算の代わりに演算のに関するプロパティを強制します。アルゴリズムの動作について追跡したいと思ういくつかの明白な事柄:

  • ランタイム
  • スペース使用量
  • 自分が所有するリソース(例:競合状態の危険なしにアクセスできるファイル

下位型のさまざまなフレーバーでこれらのすべて(そしてもっと!)が可能になります。これは、PLコミュニティにおける重要な積極的な研究課題のようです。

A possible reference is Wadler, Linear Types can Change the
World!

Note that using “deep embeddings”, it is possible to enforce
some of these properties in a standard dependent types system, see
e.g. Brady & Hammond Resource-safe Systems Programming with
Embedded Domain Specific Languages
.

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です