21.2. 控制结构🔗

通常，使用 IO 编写的程序会使用与其他单子程序相同的控制结构。此外还有一个 IO 专用的辅助函数。

不透明定义

IO.iterate {α β : Type} (a : α) (f : α → IO (α ⊕ β)) : IO β
IO.iterate {α β : Type} (a : α)
  (f : α → IO (α ⊕ β)) : IO β

迭代执行一个 IO 动作。从初始状态开始，反复应用该动作，直到它在 Sum.inr 中返回最终值。每当它返回 Sum.inl 时，返回值都会被视为新的状态。