21. IO🔗

Lean 是一种纯函数式编程语言。 Lean 代码在运行时采用严格求值；然而，类型检查所用的求值顺序——尤其是检查定义相等时——在形式上并未指定，而是依赖多种可提升性能但可能变化的启发式方法。这意味着，如果直接加入执行副作用的操作（例如文件 I/O、异常或可变引用），程序中的副作用顺序将无法确定。类型检查期间，连含有自由变量的项也会被归约；这会使副作用更加难以预测。最后，Lean 逻辑的一项基本原则是：函数确实是函数，即把定义域中的每个元素映射到值域中的唯一元素。若纳入控制台 I/O、任意可变状态或随机数生成等副作用，就会违反这一原则。

可能产生副作用的程序具有一种类型（通常为 IO α），以便与纯函数区分。从逻辑上说，IO 描述副作用的先后次序与数据依赖关系。从 Lean 逻辑的角度看，许多基本副作用（例如读取文件）是不透明常量。另一些则由逻辑上等价于运行时版本的代码来规定。在运行时，精译器会生成普通代码。