効果システム

コンピュータ分野 において、効果システムとは、副作用などのコンピュータプログラムの計算上の影響を記述する形式体系のことである。効果システムは、プログラムの起こりうる影響をコンパイル時にチェックするために使用できる。

効果システムは、型の概念を拡張し、「効果」という要素を持つようにした。この要素は、効果の種類と領域から構成される。効果の種類は、何が行われるかを記述し、領域は、それが何（パラメータ）を用いて行われるかを記述する。

効果システムは、通常、型システムの拡張です。この場合、 「型と効果システム」という用語が使われることがあります。多くの場合、値の型は、その効果とともに型 !効果として表記されます。ここで、型コンポーネントと効果コンポーネントの両方に特定の領域が示されます（たとえば、可変メモリセルの型は、そのセルが存在するメモリ領域のラベルによってパラメータ化されます）。「代数的効果」という用語は、型システムから派生したものです。

効果システムは、内部的に不純な定義の外部的純粋性を証明するために使用できます。たとえば、関数が内部的にメモリ領域を割り当てて変更するが、関数の型がその領域に言及していない場合、対応する効果は関数の効果から消去できます。^{[ 1 ]}

効果システムによって記述できる行動の例としては、以下のようなものがあります。

• メモリの読み取り、書き込み、割り当て: 効果の種類はread、write、allocate 、 freeのいずれかであり、領域は割り当てが実行されたプログラムのポイントです (つまり、割り当てが実行される各プログラムポイントには一意のラベルが割り当てられ、領域情報はデータフローに沿って静的に伝播されます)。メモリを操作するほとんどの関数は、実際には領域変数に関して多態性になります。たとえば、メモリ内の 2 つの場所を交換する関数は、型を持ちます。forall r1 r2, unit ! {read r1, read r2, write r1, write r2}
• ファイルなどのリソースを操作する場合、例えば、効果の種類は「開く」、「読み込む」、「閉じる」などがあり、領域はリソースが開かれるプログラム上のポイントです。
• 継続とロングジャンプによる制御の転送：効果の種類は、goto（つまり、コードがジャンプを実行できる）とcomefrom（つまり、コードがジャンプのターゲットになる）があり、領域は、ジャンプの起点または終点となるプログラム上の位置を示します。

プログラマーの視点から見ると、エフェクトは、特定のアクションの実装（方法）と実行するアクションの仕様を分離できるため便利です。たとえば、ask nameエフェクトは、コンソールから読み取ったり、ウィンドウをポップしたり、デフォルト値を返したりすることができます。制御フローは、 yield（実行が継続される）とthrow（未処理のエフェクトが処理されるまで伝播する）の組み合わせとして説明できます。 ^{[ 2 ]}

• マリノ、ダニエル；ミルスタイン、トッド（2009）。「汎用型と効果システム」。第4回言語設計と実装における型に関する国際ワークショップ議事録（PDF）。ACM。p . 39。CiteSeerX 10.1.1.157.8373。doi : 10.1145 / 1481861.1481868。ISBN   9781605584201. S2CID 14538045 . 
• Lucassen, John M.; Gifford, David K. (1988). "ポリモーフィック効果システム".第15回 ACM SIGPLAN-SIGACT プログラミング言語の原理に関するシンポジウム - POPL '88 議事録. ACM . pp. 47–57 . CiteSeerX 10.1.1.73.4916 . doi : 10.1145/73560.73564 . ISBN   978-0897912525. S2CID 13015611 .