52

言語設計に関して TypeState は何を参照していますか? Rust と呼ばれる mozilla による新しい言語に関するいくつかの議論で言及されているのを見ました。

4

3 に答える 3

48

注: Typestate は Rust から削除されました。限定バージョン (初期化されず、変数から移動されたものを追跡) のみが残されています。最後に私のメモを参照してください。

TypeStateの背後にある動機は、型は不変ですが、そのプロパティの一部は変数ごとに動的であるということです。

したがって、型に関する単純な述語を作成し、コンパイラが他の多くの理由で実行する制御フロー分析を使用して、それらの述語で型を静的に装飾するという考え方です。

これらの述語は実際にはコンパイラー自体によってチェックされません。それは面倒すぎる可能性があります。代わりに、コンパイラーは単にグラフの観点から推論します。

簡単な例として、数値が偶数の場合evenに返すpredicate を作成します。true

ここで、次の 2 つの関数を作成します。

  • halve、数値のみに作用しevenます
  • double、任意の数値を取り、数値を返しevenます。

タイプは変更されないことに注意してください。タイプnumberを作成せずevennumber、以前に作用したすべての関数を複製しnumberます。numberという述語で構成するだけevenです。

それでは、いくつかのグラフを作成しましょう。

a: number -> halve(a)  #! error: `a` is not `even`

a: number, even -> halve(a)  # ok

a: number -> b = double(a) -> b: number, even

シンプルですね。

もちろん、いくつかの可能なパスがある場合は、もう少し複雑になります。

a: number -> a = double(a) -> a: number, even -> halve(a) #! error: `a` is not `even`
          \___________________________________/

これは、述語のセットに関して推論することを示しています。

  • 2 つのパスを結合する場合、述語の新しいセットは、それらの 2 つのパスによって指定された述語のセットの共通部分です。

これは、関数の一般的なルールによって拡張できます。

  • 関数を呼び出すには、必要な述語のセットが満たされている必要があります
  • 関数が呼び出された後、確立された一連の述語のみが満たされます (注: 値によって取得される引数は影響を受けません)

したがって、 Rust の TypeState の構成要素は次のとおりです。

  • check: 述語が保持されていることを確認しfail、そうでない場合は、述語を一連の述語に追加します。

Rustは述語が純粋な関数であることを要求するcheckため、述語がこの時点で既に成立していることを証明できれば、冗長な呼び出しを排除できることに注意してください。

Typestate に欠けているものは単純です: 構成可能性です。

説明を注意深く読むと、次のことがわかります。

  • 関数が呼び出された後、確立された一連の述語のみが満たされます (注: 値によって取得される引数は影響を受けません)

これは、型の述語はそれ自体では役に立たないことを意味し、ユーティリティは関数の注釈から得られます。したがって、既存のコードベースに新しい述語を導入するのは退屈です。既存の関数を見直して微調整し、不変式が必要かどうか、または保持する必要があるかどうかを説明する必要があるからです。

そして、これは、新しい述語がポップアップするときに指数関数的な速度で関数を複製することにつながる可能性があります。残念ながら、述語は構成可能ではありません。彼らが対処することを意図していたまさに設計上の問題 (型の増殖、したがって関数) は対処されていないようです。

于 2012-04-25T15:55:18.017 に答える
13

これは基本的にタイプの拡張であり、一般的に何らかの操作が許可されているかどうかをチェックするだけでなく、この特定のコンテキストでチェックします。これらはすべてコンパイル時に行われます。

元の論文は実際にはかなり読みやすいです。

于 2010-07-09T06:14:20.270 に答える
4

Java 用に作成された typestate チェッカーがあり、Adam Warski の説明ページに役立つ情報がいくつかあります。私はこの資料を自分で理解しているだけですが、Haskell の QuickCheck に精通している場合、QuickCheck のモナド状態への適用は似ているように見えます: 状態を分類し、インターフェイスを介して変更されたときに状態がどのように変化するかを説明します。

于 2010-07-09T08:21:24.623 に答える