私はコントラクト言語による設計で実際にプログラミングしたことはありません。この投稿が動的型付けシステムと静的型付けシステムの戦争になることは絶対に望んでいません。
しばらく読んだ後の私の質問は、タイトルの質問です。型システムが「キャッチ」できるものはすべて、契約による設計もできますか? 一部のサイトで、「契約はステロイドのタイプである」のようなものを読んだり、そのような主張をしたりしました。しかし、それは本当に真のスーパーセットですか?
または、別の言い方をすれば、コントラクトのある動的言語は、コントラクトのない静的に型付けされた言語よりも (実行時に) 同じ検証を行うことができますか?
ありがとう！
いいえ。動的にチェックできるのはローカルプロパティのみですが、ある種のグローバルな知識を必要とするプロパティはチェックできません。一意のもの、エイリアスされていないもの、競合状態やデッドロックのない計算などのプロパティについて考えてみてください。適切な静的型システムは、チェックされている式のコンテキストで特定の不変条件を確立する機能を備えているため、このようなプロパティを検証できます。
私は契約の専門家ではありませんが、これはおおむね正しいと思います。一般に、コントラクトを使用すると、任意の複雑な動作を強制する動的チェックを作成できます。コントラクトの優れた点は、次の目的で使用できることです。
はい、コントラクトは、「セットとしての型」という共通の視点という意味で、型システムと同じくらい単純にすることができます (これは、ポリモーフィック cse では実際には正しくありませんが、気になる多くのケースでいくつかの動作を近似します)。契約言語の構造的制約と見なすことができます。ただし、コントラクト システムを使用すると、より装飾的な動作を記述できます。並べ替え関数の入力と並べ替えられた出力の間の関係を表すコントラクトを作成できますが、これには依存型が必要になります。タイプで正しく書き留められている場合。したがって、単純な答えは、はい、コントラクトを使用して、型システムが定義できるすべてのものなどを定義できるということです。(奇妙なサブ構造型システムなどのエッジ ケースについては完全にはわかりませんが、これは物事を汚染するコントラクトによっても達成できると思います。)
コインの裏返しとして、型システムは、プログラムが (ある程度は) 正しいことを静的に保証します。ただし、契約上、これはまったく言えません。(もちろん、標準タイプ システム、モデル チェック、SMT ソルバーなどを使用して部分的に検証されているものとして、コントラクトの特定の縮退ケースを表示することもできます。また、実際にこの分野でいくつかの作業が行われています。)コントラクトの本当に強力な点は、基本的に、プログラムの検証は難しいという考えです。静的な保証の一部を破棄し、バグの可能性を許容し、何がうまくいかなかったのかについてより良い情報を取得して、迅速に修正できるようにしましょう。
ところで、単純な構造上の制約だけでなく、より高度なコントラクト システムが現在あります。高次の一時的なコントラクト ( here ) や、コントラクトを使用したプログラミングを非常にクールにするその他の拡張機能もあります。
編集：これももっと明確にするべきだったと思います。契約でグローバルに追跡できないプログラムのローカルプロパティが確かにあるので、その点に関してはAndresの応答の方が正しいようです。申し訳ありません!