8.Β IO
Lean is a pure functional programming language. While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking definitional equality, is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change. This means that simply adding operations that perform side effects (such as file I/O, exceptions, or mutable references) would lead to programs in which the order of effects is unspecified. During type checking, even terms with free variables are reduced; this would make side effects even more difficult to predict. Finally, a basic principle of Lean's logic is that functions are functions that map each element of the domain to a unique element of the range. Including side effects such as console I/O, arbitrary mutable state, or random number generation would violate this principle.
Programs that may have side effects have a type (typically IO Ξ±) that distinguishes them from pure functions.
Logically speaking, IO describes the sequencing and data dependencies of side effects.
Many of the basic side effects, such as reading from files, are opaque constants from the perspective of Lean's logic.
Others are specified by code that is logically equivalent to the run-time version.
At run time, the compiler produces ordinary code.