21. IO🔗

Lean 是一种纯函数式编程语言。虽然 Lean 代码在运行时严格求值，但类型检查期间（尤其是检查定义等价时）使用的求值顺序在形式上未指定，并且使用了许多启发式方法来提高性能，但可能会发生变化。这意味着简单地添加执行副作用的操作（例如文件 I/O、异常或可变引用）将导致程序中的效果顺序未指定。在类型检查期间，甚至带有自由变量的项也会被减少；这将使副作用更加难以预测。最后，Lean 逻辑的基本原则是函数是将域的每个元素映射到范围的唯一元素的函数。包括控制台 I/O、任意可变状态或随机数生成等副作用将违反此原则。

可能有副作用的程序有一个类型（通常为 IO α）来将它们与纯函数区分开来。从逻辑上讲，IO描述了副作用的排序和数据依赖性。从 Lean 逻辑的角度来看，许多基本副作用（例如从文件中读取）都是不透明的常量。其他的则由逻辑上与运行时版本等效的代码指定。在运行时，编译器生成普通代码。