IOモナドは他のモナドと異なりランタイムから特別扱いされている

[Seasawher]

ある意味では特別だけど、型理論的にはそこまで特別ではない。

型理論的には特別ではない

Lean から見ると

IO α

は単なる型だ。

例えば

Option α
StateM σ α
Except ε α
IO α

は全部同じように型コンストラクタとして扱われる。

do 記法も

let x ← m

を

m >>= fun x => ...

に展開しているだけなので、IO 専用の仕組みではない。

⸻

しかし実行時には特別

問題は

def main : IO Unit := ...

をどうやって実行するか。

例えば

def x : Option Nat := some 3

を OS は実行できない。

一方

def main : IO Unit := ...

は

OS
↓
Lean runtime
↓
main を実行

という特別扱いを受ける。

つまり

IOモナドだけがランタイムと接続されている

という意味では特別。

⸻

StateMとの比較

例えば

def prog : StateM Nat Nat := do
modify (· + 1)
get

も

def prog : IO Nat := do
IO.rand

も見た目は似ている。

しかし

#eval prog.run 0

は単なる純粋関数の評価。

一方

#eval (IO.rand)

はランタイムに乱数生成を依頼している。

ここが決定的な違い。

⸻

Haskell 的な説明

Haskell ではしばしば

IO a ≈ RealWorld -> (a, RealWorld)

と説明される。

もし本当にそうなら

abbrev MyIO α := World → α × World

でも似たようなものを作れる。

だが

def rand : MyIO Nat := ?

は作れない。

Lean の純粋関数だけでは乱数源にアクセスできないから。

結局どこかで

OS
乱数デバイス
ファイルシステム
ネットワーク

と接続する原始操作が必要になる。

その原始操作を持っているのが IO。

⸻

もっと正確に言うと

実は Lean の IO は普通のモナドですらない。

内部的には

EIO IO.Error α

だったり、

さらに下では

BaseIO α

やランタイムのプリミティブに繋がっている。

最終的には C++ ランタイムの関数を呼ぶ。

つまり

IO.rand

は数学的に定義された純粋関数ではなく、

Leanコード
↓
ランタイムプリミティブ
↓
OS
↓
乱数取得

という経路を持つ。

⸻

結論としては、

モナドとしての IO は StateM や Option と同じで特別ではない。

しかし「実世界と接続された唯一のモナド」としてランタイムから特別扱いされている。

というのが一番正確な理解になる。