22. 迭代器🔗

iterator 提供对某些数据源的每个元素的顺序访问。典型的迭代器允许对集合（例如列表、数组或 TreeMap）中的元素进行一一访问，但它们也可以通过执行某些 monadic 效果（例如读取文件）来提供对数据的访问。迭代器为所有这些操作提供了一个通用接口。写入迭代器 API 的代码可以不知道数据源。

每个迭代器都维护一个内部状态，使其能够确定下一个值。由于 Lean 是纯函数式语言，因此使用迭代器不会使其无效，而是使用更新后的状态复制它。与往常一样，引用计数用于将仅使用一次值的程序优化为破坏性修改值的程序。

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

Mixing Collections

使用 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")]

Live ↪

Avoiding Intermediate Structures

在此示例中，组合了颜色数组和颜色代码列表。该计划分为三个中间阶段：

名称和代码成对组合。
这些对被转换成可读的字符串。
字符串与换行符组合在一起。

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 一次执行一个步骤。在每个步骤中，单个颜色和颜色代码被组合成一对，重写为字符串，并添加到结果字符串中。

Live ↪

Lean 标准库提供了三种迭代器操作。 Producers 从某些数据源创建一个新的迭代器。它们确定迭代器要返回哪些数据，以及如何计算这些数据，但它们无法控制计算发生的时间。 Consumers 将迭代器中的数据用于某种目的。消费者请求迭代器的数据，迭代器仅计算足够的数据来满足消费者的请求。 Combinators 既是消费者又是生产者：它们从现有迭代器创建新迭代器。示例包括 Iter.map 和 Iter.filter。生成的迭代器通过消耗其底层迭代器来生成数据，并且在它们本身被消耗之前实际上不会迭代底层集合。

每个有意义的内置集合都可以进行迭代。换句话说，集合库包括迭代器生产者。按照约定，集合类型 Coll 提供函数 Coll.iter，该函数返回集合元素上的迭代器。示例包括 List.iter、Array.iter 和 TreeMap.iter。此外，其他内置类型（例如范围）支持使用相同约定的迭代。