契約/制約に基づく型システムに関する有益な情報はありますか?

Question

問題：

～についての良い紹介を探しています 型システム、それに基づいています 契約/制約
(申し訳ありませんが、型システムにどの用語が適切かは覚えていません).

このような実験的なシステムを実装するには、その情報が必要です。

私の知る限り、そのような型システムは次のようなもので使用されています。 XSD (Xml スキーマ定義)。

データ型を定義する代わりに、可能な値のセットに対する制約を定義します。

例：

パラメーターを使用してメソッドを定義します。 "nothing", 、または整数範囲に一致します [0..100].

このようなメソッドは次の値を受け入れます。

"nothing"
0
1
...
100

自分自身を明確にすることができれば幸いです。

Answer 1

Common Lisp では、このような型テストを提供しています。 実行時間. 。これには精巧な型システムがありますが、静的型付け言語でよく使われるような使用は行われません。マクロ check-type を受け入れます タイプスペック, 、組み込み仕様またはマクロによって定義された仕様にすることができます。 deftype. 。typespec で表現できる制約は、ホスト言語で記述された述語関数の制約です。つまり、実行時に検査できるものはすべて、新しい型を構成する基準になり得ます。

次の例を考えてみましょう。

(defun is-nothing (val)
  (when (stringp val)
    (string= val "nothing")))

(deftype strange-range ()
  "A number between 0 and 100 inclusive, or the string \"nothing\"."
  '(or (integer 0 100)
       (satisfies is-nothing)))

これは「strange-range」と呼ばれるタイプを定義します。次に、それに対していくつかの値をテストします。

CL-USER> (let ((n 0))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 100))
           (check-type n strange-range))
NIL
CL-USER> (let ((n "nothing"))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 101))
           (check-type n strange-range))

最後のものは、次のメッセージを表示してデバッガーをトリガーします。

The value of N should be of type STRANGE-RANGE.
The value is: 101
   [Condition of type SIMPLE-TYPE-ERROR]

これも同じ結果を引き起こします。

CL-USER> (let ((n "something"))
           (check-type n strange-range))

この方法で課すことのできる制約は表現力豊かですが、Haskell や Scala などの言語の精巧な型システムと同じ目的は果たしません。型定義は Common Lisp コンパイラを誘導して、オペランドの型に合わせてより効率的に調整されたコードを出力することができますが、上記の例は実行時の型チェックを記述するためのより簡潔な方法です。

Answer 2

次のような言語を確認できます ハスケル, 、 あるいは アグダ. 。また、 オレグ 素晴らしいリソースがたくさんあります。

Answer 3

これは私の専門分野ではないので、話が逸れるかもしれませんが、Microsoft Research には次のプロジェクトがあります。 コードコントラクト, これは、「.NET プログラムでコーディングの前提条件を表現する言語に依存しない方法を提供します。契約は、前提条件、事後条件、およびオブジェクトの不変条件の形式をとります。」