若 a 是共享值（即其引用计数 RC(a) 大于 1），则显示给定消息；无论是否显示消息，
都原样返回 a。
12.2. 引用计数
Lean 使用引用计数来管理内存。 每个已分配对象都会维护一个计数，记录有多少其他对象引用它。 新增引用时计数递增，丢弃引用时计数递减。 当引用计数降为零时，该对象便不再可达，也不可能再参与程序后续的执行。 系统会释放该对象并丢弃它对其他对象的全部引用，这可能进一步触发其他对象的释放。
引用计数有许多优点：
- 复用内存
如果某个对象的引用计数恰在需要分配另一个同样大小的对象时降为零，就可以安全地将原对象的内存复用于新对象。 因此，当待遍历的数据结构恰好只有一个引用时，许多常见的数据结构遍历（例如
List.map）都不必分配内存。- 条件允许时原地更新
字符串和数组等原语类型（参见字符串和数组）可以在数据共享时执行复制，而在数据未共享时原地修改。 只要待修改值只有这一个引用，这些原语类型上的许多操作就会直接修改值，而不是复制值。 这可以显著提升性能。 精心编写的
Array代码既能避免不可变数据结构的性能开销，又能保留纯函数便于推理的特性。- 可预测性
引用计数会在可预测的时刻递减。 因此，可以用引用计数对象管理文件句柄等其他资源。 在 Lean 中，
Handle无需显式关闭，因为它一旦不再可访问就会立即关闭。- 更简单的 FFI
回收未使用的内存时，不需要移动由引用计数管理的对象。 这大幅简化了与 C 等其他语言所编写代码的交互。
引用计数的传统缺点包括更新引用计数带来的性能开销，以及无法识别和释放循环数据。 前一个缺点通过基于借用的分析得到缓解；这种分析可以省去许多引用计数更新。 不过，多线程代码要求线程之间同步引用计数更新，这也会带来显著的开销。 为降低这种开销，Lean 将值划分为可从多个线程访问的值和不可从多个线程访问的值。 单线程引用计数的更新速度可以远高于多线程引用计数，而且许多值只会在单个线程上访问。 这些技术相结合，大幅降低了引用计数的性能开销。 由于 Lean 的可验证片段无法创建循环数据，Lean 运行时没有检测循环数据的机制。 关于 Lean 中引用计数的实现，Ullrich and de Moura (2019)Sebastian Ullrich and Leonardo de Moura, 2019. “Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming”. In Proceedings of the 31st Symposium on Implementation and Application of Functional Languages (IFL 2019).提供了更多细节。
12.2.1. 观察唯一性
要在 Lean 中编写高效代码，确保数组和字符串只有一个引用至关重要。
原语 dbgTraceIfShared 可用于检查数据结构是否存在别名。
调用它时，它会原样返回参数；如果参数的引用计数大于一，则打印所提供的跟踪消息。
受 Lean.Parser.Command.eval : command#eval 具体实现方式的影响，将 dbgTraceIfShared 与 Lean.Parser.Command.eval : command#eval 一同使用可能产生误导。
应当改在明确经过编译并运行的代码中使用它。
观察唯一性
该程序从用户处读取一行输入，将第一个字符替换为空格后打印出来。
如果字符串未被共享，且新旧字符都属于 Unicode 的 7 位 ASCII 子集，替换字符串中的字符时就会执行原地更新。
dbgTraceIfShared 调用没有任何输出，这表明字符串确实会原地更新，而不是先被复制。
def process (str : String) (h : str.startPos ≠ str.endPos) : IO Unit := do
IO.println (String.Pos.set (dbgTraceIfShared "String update" str).startPos ' ' h)
def main : IO Unit := do
let line := (← (← IO.getStdin).getLine).trimAscii.copy
if h : line.startPos ≠ line.endPos then
process line h
使用以下输入运行时：
stdinHere is input.程序输出：
stdout ere is input.标准错误输出为空：
stderr<empty>
这个版本的程序保留了对原字符串的引用，因此调用 String.Pos.set 时必须复制字符串。
这一点可以从它的标准错误输出中看出。
def process (str : String) (h : str.startPos ≠ str.endPos) : IO Unit := do
IO.println (String.Pos.set (dbgTraceIfShared "String update" str).startPos ' ' h)
def main : IO Unit := do
let line := (← (← IO.getStdin).getLine).trimAscii.copy
if h : line.startPos ≠ line.endPos then
process line h
IO.println "Original input:"
IO.println line
使用以下输入运行时：
stdinHere is input.程序输出：
stdout ere is input.Original input:Here is input.
在标准错误中可以看到传给 dbgTraceIfShared 的消息。
stderrshared RC String update12.2.2. 编译器中间表示（IR）
编译器选项 trace.compiler.ir.result 可用于查看函数的编译器中间表示（IR）。
在这种中间表示中，引用计数、内存分配和复用都是显式的：
-
isShared运算符检查引用计数是否为1。 -
ctor_n分配某个类型的第n个构造器。 -
proj_n从构造器值中取出第n个字段。 -
setx[n]修改x中构造器的第n个字段。 -
retx返回x中的值。
引用计数操作的具体方式可能取决于内联等优化阶段的结果。 绝大多数 Lean 代码无须关注这些细节就能获得良好性能，但在编写性能关键型代码时，掌握如何诊断唯一引用相关的问题可能非常重要。
IR 中的引用计数
通过编译器中间表示（IR）可以观察引用计数何时递增，这有助于诊断以下情形：本以为某个值只有一个传入引用，但它实际上却被共享。
这里，process 和 process' 都接受一个字符串参数，使用 String.Pos.set 修改它，并返回一对字符串。
process 将常量字符串作为二元组的第二个元素返回，而 process' 则返回原字符串。
set_option trace.compiler.ir.result true
def process (str : String) : String × String :=
(String.Pos.Raw.set str 0 ' ', "")
def process' (str : String) : String × String:=
(String.Pos.Raw.set str 0 ' ', str)
process 的 IR 中不包含 inc 或 dec 指令。
如果传入的字符串 x_1 是唯一引用，那么将它传给 String.Pos.set 时，它仍然是唯一引用，因此可以就地修改：
另一方面，process' 的 IR 会在调用 String.Pos.set 之前递增该字符串的引用计数。
因此，无论 x_1 的原始引用是否唯一，修改后的字符串 x_4 都是一个副本：
IR 中的内存复用
函数 discardElems 是 List.map 的简化版本，它将列表中的每个元素替换为 ()。
查看其中间表示可以看出，当列表的引用唯一时，它会复用列表的内存。
set_option trace.compiler.ir.result true
def discardElems : List α → List Unit
| [] => []
| _ :: xs => () :: discardElems xs
这会生成如下 IR：
在 IR 中，List.cons 分支会显式检查参数值是否被共享（即其引用计数是否大于一）。
如果引用唯一，则会递减被丢弃的列表元素 x_5 的引用计数，并复用构造器值。
如果引用被共享，则会在 x_11 中为结果分配一个新的 List.cons。