22. 迭代器🔗

迭代器提供对某个数据源中各元素的顺序访问。典型的迭代器允许逐个访问列表、数组或 TreeMap 等集合中的元素；它们也可以通过执行某种单子式效果（例如读取文件）来提供数据访问。迭代器为所有这些操作提供了统一接口。依据迭代器接口编写的代码无需关心数据来自何处。

每个迭代器都维护一份内部状态，用以确定下一个值。由于 Lean 是纯函数式语言，消费迭代器不会使其失效，而是会复制出一个状态已更新的迭代器。一如既往，引用计数会将仅使用值一次的程序优化为以破坏性方式修改值的程序。

要使用迭代器，请导入 Std.Data.Iterators。

混用集合

通常，使用 List.zip 或 Array.zip 合并列表与数组，需要先将其中一个转换成另一种集合。使用迭代器，无需转换即可处理二者：

def colors : Array String := #["purple", "gray", "blue"]
def codes : List String := ["aa27d1", "a0a0a0", "0000c5"]

#[("purple", "aa27d1"), ("gray", "a0a0a0"), ("blue", "0000c5")]#eval colors.iter.zip codes.iter |>.toArray

#[("purple", "aa27d1"), ("gray", "a0a0a0"), ("blue", "0000c5")]

在线查看 ↪

避免中间结构

本例合并一个颜色数组和一个颜色编码列表。程序分为三个中间阶段：

将名称与编码组合成二元组。
将二元组转换为可读字符串。
用换行符连接这些字符串。

def colors : Array String := #["purple", "gray", "blue"]

def codes : List String := ["aa27d1", "a0a0a0", "0000c5"]

def go : IO Unit := do
  let colorCodes := colors.iter.zip codes.iter
  let colorCodes := colorCodes.map fun (name, code) =>
    s!"{name} ↦ #{code}"
  let colorCodes := colorCodes.fold (init := "") fun x y =>
    if x.isEmpty then y else x ++ "\n" ++ y
  IO.println colorCodes

purple ↦ #aa27d1
gray ↦ #a0a0a0
blue ↦ #0000c5
#eval go

purple ↦ #aa27d1
gray ↦ #a0a0a0
blue ↦ #0000c5

计算的中间阶段不会分配新的数据结构。相反，转换的所有步骤会融合为一个循环，由 Iter.fold 每次执行一步。每一步都会将一个颜色及其编码组合成二元组、改写为字符串，再加入结果字符串。

在线查看 ↪

Lean 标准库提供三类迭代器操作。 生产者从某个数据源创建新的迭代器。它们决定迭代器返回哪些数据以及如何计算这些数据，但不控制计算在何时发生。 消费者将迭代器中的数据用于某种目的。消费者向迭代器请求数据，而迭代器只计算足以满足请求的数据。 组合子既是消费者也是生产者：它们从现有迭代器创建新的迭代器。例如 Iter.map 和 Iter.filter。所得迭代器通过消费其底层迭代器来生产数据；只有当它们自身被消费时，才会真正遍历底层集合。

每种适合迭代的内置集合都可以被遍历。换言之，集合库包含迭代器生产者。按照约定，集合类型 Coll 会提供函数 Coll.iter，返回遍历该集合元素的迭代器。例如 List.iter、Array.iter 和 TreeMap.iter。此外，区间等其他内置类型也按同一约定支持迭代。