Effect system とは

計算において、エフェクトシステムは、副作用などのコンピュータプログラムの計算効果を記述する正式なシステムです。エフェクトシステムを使用して、プログラムの可能な影響をコンパイル時に確認することができます。
エフェクトシステムは、エフェクトの種類とリージョンを含む「エフェクト」コンポーネントを持つようにタイプの概念を拡張しています。エフェクトの種類は何が行われているのかを記述し、その領域は何が行われているのかを記述します。
エフェクトシステムは、通常、タイプシステムの拡張です。この場合には、「タイプとエフェクトシステム」という用語が使用されることがあります。多くの場合、値の型は、型としての効果とともに表示されます。 (例えば、可変メモリセルのタイプは、セルが存在するメモリ領域のラベルによってパラメータ化される)。
エフェクトシステムで記述できるビヘイビアの例をいくつか挙げます。
 メモリの読み込み、書き込み、または割り当て:エフェクトの種類は読み込み、書き込み、割り当てまたはフリーであり、領域は割り当てが行われたプログラムのポイントです(つまり、割り当てが行われる各プログラムポイントには一意のラベルが割り当てられ、情報はデータフローに沿って静的に伝搬される)。メモリで動作するほとんどの関数は、実際には領域変数で多相になります。たとえば、メモリ内の2つの場所を交換する関数は、for r1 r2、unit! {r1を読み、r2を読み、r1を書き、r2を書き込む}。ファイルなどのリソースの操作:たとえば、エフェクトの種類が開いている、読み込み、終了している可能性があります。また、領域はリソースが開かれているプログラムのポイントです。エフェクトの種類はgoto(コードの一部がジャンプを実行している可能性があります)およびcomefrom(コードの一部がジャンプのターゲットになる可能性があります)であり、リージョンはジャンプが実行されるかまたはそこからジャンプが実行されるプログラム。 Javaのチェック例外は、エフェクトシステムの例です。エフェクトの種類はスローで、領域はスローされる例外の種類です。
エフェクトシステムは、特定の内部的に不純な定義の外部純度を証明するために使用することができます。たとえば、ある関数がメモリの領域を内部的に割り当てたり変更したりしますが、その関数の型にはその領域は含まれません。機能の効果。