Wadlerは素晴らしい論文を書きました: Propositions as Types - 彼はHoward-Curry対応について述べており、プログラムの動作をプログラムの型の観点からチェックできると述べています。(特定の言語サブセットの場合)。
最近、Rich Hickeyは、データと関数の仕様を定義するClojure 仕様をリリースしました。
Wadler から、props ≅ types、specs ≅ props -> types が得られたので、静的な spec/contract/type チェックを行うことができます。
私の質問は、Clojure の仕様は Wadler の命題と同等ですか?
型としての命題は、自然演繹法と単純型付けラムダ計算 (STLC) の間に存在する同形性について具体的に述べています。これが意味することは、STLC でプログラミングしている場合、プログラムをロジックの命題に変換できるということです。
たとえば、これらは同等です。
(a -> b) -> a -> b
P implies Q
P
therefore Q
1 つ目は関数の型シグネチャで、2 つ目は論理命題です。「Clojure の仕様は Wadler の命題と同等ですか?」あなたが求めているのは、「Clojure の仕様をロジックのステートメントに変換できますか?」ということです。または、同形のため、「clojure 仕様を STLC に変換できますか?」
仕様により、すべての Clojure述語を使用できます。これにより、仕様は信じられないほど柔軟になりますが、仕様が命題ではないことを確認するための鍵でもあります。
STLC をロジックとして機能させる重要な機能の 1 つは、すべての用語が削減される、つまり、STLC 内のすべてのプログラムが終了することです。Clojure にはこのプロパティがありません。決して終了しない Clojure プログラムを作成するのは簡単です。「非終了」は論理の矛盾に相当するため、プログラミング言語が一貫したロジックであるためには、この終了プロパティが必要です。スペックは Clojure の任意の関数を使用できるため、終了せず、したがって STLC に変換できないスペックを作成できます。したがって、Clojure の仕様は Wadler の命題と同等ではありません。
Clojure specのドキュメントにあるように、spec は型システムではありません。仕様は証明に関係ありませんが、型は証明に関係します。型は、私たちが書くことができるプログラムを、「正しく動く」ことが静的に証明できるものに制限します。型システムにはさまざまなレベルのパワーと表現力がありますが、サウンド型システムはコードに関する特定の特性を証明します。
仕様は、コードに関するプロパティを証明するものではありませんが、代わりに、コードが機能するという確信と、機能しない場合の可視性を提供しようとします。スペックは静的に実行することはできません。基本的にはランタイム値とそれらの間の関係に関するものです。
しかし、これらの違いがあっても、型と Clojure の仕様は同様の実用的な目的を果たします。どちらもコードの信頼性を高め、セマンティクスを関数定義にエンコードすることを可能にし、どちらもテスト生成を支援し、防止するのに役立ちます。バグがコードに忍び込むのを防ぎます。