まとめ

副作用のエンコード

Leanは純粋関数型言語です。これは可変変数やロギング、例外等の副作用を言語として含んでいないことを意味します。しかし、ほとんどの副作用は関数と帰納型か構造体を組み合わせることで エンコード できます。例えば、可変状態は初期状態から最終状態と結果のペアへの関数としてエンコードされ、例外は正常終了と異常終了のそれぞれへのコンストラクタを持つ帰納型としてエンコードできます。

エンコードされた作用それぞれは型です。その結果、これらのエンコードされた作用を使うプログラムは、作用を使っていることが型に表れます。関数型プログラミングは作用が使えないことを意味せず、シンプルに使用する作用について 正直であること が求められます。Leanの型シグネチャは関数が受け取る引数の型と関数の戻り値だけでなく、そこで使われる作用についても記述します。

モナド型クラス

作用をどこでも使えるような言語でも純粋で関数型のプログラムを書くことは可能です。例えば、2 + 3 はPythonにおいて一切作用を持たないプログラムとして成立します。同様に、作用を持つプログラムの結合には作用がどの順番で行われるかを定める方法が求められます。つまり、変数を変更する前に例外が投げられるか、変更した後に例外が投げられるかが重要なのです。

Monad 型クラスはこれら2つの重要な性質を兼ね備えています。このクラスには2つのメソッドがあります：pure はプログラムが作用を持たないことを表し、bind は作用を含むプログラムを結合します。Monad インスタンスの約定は bind と pure が本当に純粋な計算と連結を体現することを保証します。

モナドのための do 記法

IO に限ることなく、do 記法はどんなモナドでも使うことができます。これにより、プログラム中で文を順々に並べるというあたかも文指向（statement-oriented）言語を思わせるようなスタイルでモナドを使うことができます。さらに、do 記法はネストしたアクションなどの追加の便利な短縮記法を可能にします。do で書かれたプログラムはその裏で >>= の適用に翻訳されます。

モナドの自作

異なる言語では異なる副作用が提供されます。ほとんどの言語では可変変数とファイルのI/Oを兼ね備えている一方、例外を持たない言語も存在します。また一部の言語では珍しく独特な作用を用意しています。例えばIconの検索に基づくプログラムの実行やSchemeとRubyの継続、Common Lispの再開可能な例外などです。モナドで作用をエンコードすることには、言語から提供される作用だけに限定されなくなるというアドバンテージがあります。Leanはどんなモナドでも快適にプログラミングできるように設計されているため、プログラマは任意のアプリケーションにぴったりな副作用を自由に選ぶことができます。

IO モナド

Leanでは、実世界に影響を及ぼすプログラムは IO アクションとして記述されます。IO は数多くあるモナドの中の1つです。IO モナドは状態と例外をエンコードしており、このうち状態は世界の状態を追跡するために、例外は失敗と回復をモデル化するためにそれぞれ用いられます。