0

問題：

契約/制約に基づく型システムについての良い紹介を探しています（申し訳ありませんが、どの用語が型システムに適しているか覚えていません）。

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

私の知る限り、このような型システムはXSD（Xml Schema Definition）で使用されています。

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

例：

"nothing"のいずれかであるか、積分範囲に一致するパラメーターを使用して、いくつかのメソッドを定義します[0..100]。

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

"nothing"
0
1
...
100

自分のことをはっきりさせたいと思います。

4

3 に答える 3

2

HaskellやAgdaなどの言語を見ることができます。また、オレグには素晴らしいリソースがたくさんあります。

于 2009-11-27T20:55:02.290 に答える
1

Common Lisp は、実行時にそのような型テストを提供します。精巧な型システムを備えていますが、静的に型付けされた言語で慣れている可能性があるため、使用されていません。マクロはtypespeccheck-typeを受け入れます。これは、組み込み仕様またはマクロによって定義されたものです。typespec で表現できる制約は、ホスト言語で記述された述語関数の制約です。つまり、実行時に検査できるものはすべて、新しい型を構成する基準になる可能性があります。deftype

次の例を検討してください。

(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))

最後の 1 つは、次のメッセージでデバッガーをトリガーします。

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 コンパイラを誘導して、オペランドの型に合わせてより効率的なコードを生成することができますが、上記の例は、実行時の型チェックを記述するためのより簡潔な方法です。

于 2009-11-27T21:46:28.163 に答える
1

これは私の専門分野ではないため、トピックから外れている可能性がありますが、Microsoft Research にはプロジェクトCode Contractsがあり、「.NET プログラムでコーディングの仮定を表現する言語にとらわれない方法を提供します。契約は、前提条件、事後条件の形式をとります。 、およびオブジェクトの不変条件」。

于 2009-11-27T21:04:30.087 に答える