types - タイプアンドエフェクトシステムとは？

Question

効果システムに関するウィキペディアの記事は現在のところ短いスタブに過ぎず、私は効果システムとは何かについてしばらく疑問に思っていました。

• 型システムに加えて効果システムを持つ言語はありますか?
• あなたがよく知っている主流の言語で可能な (仮説的な) 記法は、エフェクトでどのように見えるでしょうか?

Answer 1

「タイプと効果のシステム」は、プログラム内の値の種類だけでなく、それらの値の変化も記述します。「Typestate」チェックは関連するアイデアです。

例としては、ファイル ハンドルを追跡する型システムがあります。close戻り値の型を持つ関数を使用する代わりにvoid、型システムは、ファイル リソースの破棄としての効果を記録closeします。呼び出し後にファイルから読み書きしようとcloseすると、タイプエラー。

主流のプログラミング言語に登場する型と効果のシステムを私は知りません。それらは静的分析を定義するために使用されてきました (たとえば、効果に関して適切なロック/ロック解除の分析を定義することは非常に自然なことです)。そのため、効果システムは通常、具体的な構文ではなく推論スキームを使用して定義されます。次のような構文を想像できます

File open(String name) [+File]; // open creates a new file handle
void close(File f)     [-f]   ; // close destroys f 

詳細を知りたい場合は、次の論文が興味深いかもしれません (公正な警告: 論文は非常に理論的なものです)。

• Atomicity の型: Java の静的チェックと推論。フラナガン、フロイント、リプシン、カディール。
• 低レベル ソフトウェアでの高レベル プロトコルの強制。ロバート・デラインとマヌエル・フェンドリッヒ。
• タイプと効果システム。ニールソンとニールソン。

Answer 2

（これは信頼できる答えではありません。ただ私の記憶をトロールしようとしているだけです。）

ある意味で、言語で「状態モナド」をコーディングするときはいつでも、潜在的なエフェクトシステムとして型システムを使用しています。したがって、Haskellの「State」または「IO」はこの概念をキャプチャします（IOは他の多くの効果もキャプチャします）。「依存型」などの高度な型システムを使用して効果のよりきめ細かい管理を制御するさまざまな言語に関する論文を読んだことをぼんやりと覚えています。たとえば、型/効果システムは、どのメモリ位置が変更されるかについての情報をキャプチャできます。指定されたデータ型。これは、相互に排他的な状態のビットを変更する2つの関数が「通勤」できるようにする方法を提供するので便利です（モナドは通常通勤せず、異なるモナドは常に互いにうまく構成されるとは限りません。

非常に手に負えないレベルでのアナロジーは、 Javaが例外をチェックする方法です。型システムで特定の効果に関する追加情報を表現しますが（類推の目的で例外を「効果」と考えることができます）、これらの「効果」は通常、プログラム全体に漏れ出し、でうまく構成されません。練習（100万の「throws」句を使用するか、チェックされていないランタイム例外タイプを多数使用することになります）。

この分野では、research-y言語とmainstream-y言語の両方について、多くの研究が行われていると思います。関数に効果情報で注釈を付ける機能は、コンパイラーが多くの最適化を行う能力を解き放ち、並行性に影響を与える可能性があるためです。さまざまなプログラム分析とツールのために素晴らしいことをすることができます。個人的には、すぐに期待することはありませんが、多くの賢い人々が長い間取り組んできたと思いますが、それを示すものはまだほとんどありません。