IOモナド

モナドとしての IO は2つの観点から理解することができます。これは プログラムの実行 の節で説明したとおりです。それぞれの観点から、IO における pure と bind の意味の理解が促進されます。

最初の観点では、IO アクションはLeanのランタイムシステム（RTS）に対する命令として捉えられていました。その命令は、例えば「このファイル記述子から文字列を読み込み、その文字列で純粋なLeanコードを再度呼んでください」などのようなものです。この観点は 外部的な もので、オペレーティングシステム側からプログラムを見ています。この場合、pure は IO アクションであり、RTSにいかなる作用も要求しません。また、bind はRTSに対して、まず潜在的に作用を持つ操作を実行し、その結果得られた値で残りのプログラムを呼び出すように指示します。

2つ目の観点では、IO アクションは世界全体を変換すると考えられます。IO アクション自体は純粋です。というのもこれは一意な世界を引数として受け取り、変更後の世界を返すからです。この観点は 内部的な もので、Leanの内部での IO の表現方法に一致します。Leanにおいて世界はトークンとして表現され、IO モナドは各トークンが正確に一度だけ利用されるように構造化されています。

これがどのように動作するかを知るためには、定義を1つずつはがしていくことが有用です。#print コマンドはLeanのデータ型と定義の内部を明らかにします。例えば、

#print Nat

は以下の結果となります。

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

また、

#print Char.isAlpha

は以下の結果となります。

def Char.isAlpha : Char → Bool :=
fun c => Char.isUpper c || Char.isLower c

#print の出力にはこの本でまだ紹介されていないLeanの特徴が含まれることが時折あります。例えば、

#print List.isEmpty

は以下を出力します。

def List.isEmpty.{u} : {α : Type u} → List α → Bool :=
fun {α} x =>
  match x with
  | [] => true
  | head :: tail => false

ここで、上記の定義名の後ろに .{u} が含まれ、また型に対してただの Type ではなく Type u と注釈されています。これについては今のところ無視して問題ありません。

IO の定義を表示すると、思ったより単純な構造で定義されていることがわかります：

#print IO

@[reducible] def IO : Type → Type :=
EIO IO.Error

IO.Error は IO アクションが投げる可能性のあるすべてのエラーを表します：

#print IO.Error

inductive IO.Error : Type
number of parameters: 0
constructors:
IO.Error.alreadyExists : Option String → UInt32 → String → IO.Error
IO.Error.otherError : UInt32 → String → IO.Error
IO.Error.resourceBusy : UInt32 → String → IO.Error
IO.Error.resourceVanished : UInt32 → String → IO.Error
IO.Error.unsupportedOperation : UInt32 → String → IO.Error
IO.Error.hardwareFault : UInt32 → String → IO.Error
IO.Error.unsatisfiedConstraints : UInt32 → String → IO.Error
IO.Error.illegalOperation : UInt32 → String → IO.Error
IO.Error.protocolError : UInt32 → String → IO.Error
IO.Error.timeExpired : UInt32 → String → IO.Error
IO.Error.interrupted : String → UInt32 → String → IO.Error
IO.Error.noFileOrDirectory : String → UInt32 → String → IO.Error
IO.Error.invalidArgument : Option String → UInt32 → String → IO.Error
IO.Error.permissionDenied : Option String → UInt32 → String → IO.Error
IO.Error.resourceExhausted : Option String → UInt32 → String → IO.Error
IO.Error.inappropriateType : Option String → UInt32 → String → IO.Error
IO.Error.noSuchThing : Option String → UInt32 → String → IO.Error
IO.Error.unexpectedEof : IO.Error
IO.Error.userError : String → IO.Error

EIO ε α は、ε 型のエラーで終了するか、α 型の値で成功するかのどちらかになる IO アクションを表します。つまり、Except ε と同じように IO モナドにもエラー処理と例外を定義することができます。

さらに展開をはがすと、EIO もまたとてもシンプルな構造で定義されています：

#print EIO

def EIO : Type → Type → Type :=
fun ε => EStateM ε IO.RealWorld

EStateM モナドはエラーと状態の両方を保持しています。つまり Except と State を組み合わせたものです。このモナドは EStateM.Result という別の型を使って定義されています：

#print EStateM

def EStateM.{u} : Type u → Type u → Type u → Type u :=
fun ε σ α => σ → EStateM.Result ε σ α

言い換えると、EStateM ε σ α 型を持つプログラムは初期状態として σ を受け取り、戻り値として EStateM.Result ε σ α を返す関数です。

EStateM.Result の定義は Except とよく似ており、正常終了とエラーそれぞれに対して1つずつコンストラクタがあります：

#print EStateM.Result

inductive EStateM.Result.{u} : Type u → Type u → Type u → Type u
number of parameters: 3
constructors:
EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α
EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α

Except ε α と同様に、ok コンストラクタには α 型の結果が、error コンストラクタには ε 型の例外が含まれます。Except とは異なり、どちらのコンストラクタにも計算の最終状態を示す状態のフィールドが追加されています。

EStateM ε σ の Monad インスタンスを定義するには pure と bind が必要です。State と同様に、EStateM の pure の実装は初期状態を受け取り、それを変更せずに返却します。これも Except と同様に、ok コンストラクタに引数を入れて返却します：

#print EStateM.pure

protected def EStateM.pure.{u} : {ε σ α : Type u} → α → EStateM ε σ α :=
fun {ε σ α} a s => EStateM.Result.ok a s

protected は EStateM 名前空間がオープンされていても、呼び出す際には EStateM.pure とフルネームを使う必要があることを意味します。

同様に、EStateM の bind は初期状態を引数に取ります。この初期状態は最初のアクションに渡されます。そして Except の bind と同様に、結果がエラーかどうかのチェックを行います。もしエラーであれば、そのエラーがそのまま返却され、bind の第2引数は未使用のままとなります。結果が成功だった場合は、2番目の引数は戻り値と結果の状態の両方に適用されます。

#print EStateM.bind

protected def EStateM.bind.{u} : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β :=
fun {ε σ α β} x f s =>
  match x s with
  | EStateM.Result.ok a s => f a s
  | EStateM.Result.error e s => EStateM.Result.error e s

これらをすべてまとめると、IO は状態とエラーを同時に追跡するモナドということになります。利用可能なエラーのあつまりは、IO.Error というデータ型によって与えられ、これはプログラム中に起こりうる様々なエラーを記述するコンストラクタを持ちます。状態は IO.RealWorld という実世界を表すデータ型です。それぞれの基本的な IO アクションはこの実世界を受け取り、エラーまたは結果と対になった別の実世界を返します。IO では、pure は世界を変更せずに返しますが、bind はアクションから次のアクションに変更された世界を渡します。

全宇宙はコンピュータのメモリに収まらないため、アクション間で取りまわされる世界は単なる表現にすぎません。世界のトークンが再利用されない限り、表現は安全です。このことは、世界のトークンはデータを一切含む必要がないことを意味します：

#print IO.RealWorld

def IO.RealWorld : Type :=
Unit