6.1. 组合 IO 与 Reader🔗

当应用程序存在类似“当前配置”的数据需要通过多次递归调用传递时，读取器单子（Reader Monad）就会派上用场。这种程序有一个例子是 tree，它递归地打印当前目录及其子目录中的文件，并用字符表示它们的树形结构。本章中的 tree 版本名为 doug ，取自北美西海岸的道格拉斯冷杉，在显示目录结构时，它提供了 Unicode 框画字符或其 ASCII 对应字符选项。

例如，以下命令将在名为 doug-demo 的目录中创建一个目录结构和一些空文件：

cd doug-demomkdir -p a/b/cmkdir -p a/dmkdir -p a/e/ftouch a/b/hellotouch a/d/another-filetouch a/e/still-another-file-again

运行 doug 的结果如下：

doug

├── doug-demo/
│   ├── a/
│   │   ├── b/
│   │   │   ├── c/
│   │   │   ├── hello
│   │   ├── d/
│   │   │   ├── another-file
│   │   ├── e/
│   │   │   ├── f/
│   │   │   ├── still-another-file-again

6.1.1. 实现🔗

在内部，doug 在递归遍历目录结构时会向下传递一个配置值。该配置包含两个字段： useASCII 决定是否使用 Unicode 框画字符或 ASCII 垂直线和破折号字符来表示结构，而 currentPrefix 字段包含了一个字符串，用于在每行输出前添加。随着当前目录的深入，前缀字符串会不断积累目录中的指标。配置是一个结构体：

structure Config where
  useASCII : Bool := false
  currentPrefix : String := ""

该结构体的两个字段都有默认定义。默认的 Config 使用 Unicode 显示，不带前缀。

调用 doug 的用户需要提供命令行参数。用法如下：

def usage : String :=
  "Usage: doug [--ascii]
Options:
\t--ascii\tUse ASCII characters to display the directory structure"

据此，可以通过查看命令行参数列表来构建配置：

def configFromArgs : List String → Option Config
  | [] => some {} -- both fields default
  | ["--ascii"] => some {useASCII := true}
  | _ => none

main 函数是一个名为 dirTree 的内部函数的包装，它根据一个配置来显示目录的内容。在调用 dirTree 之前，main 需要处理命令行参数。它还必须向操作系统返回适当的退出状态码：

def main (args : List String) : IO UInt32 := do
  match configFromArgs args with
  | some config =>
    dirTree config (← IO.currentDir)
    pure 0
  | none =>
    IO.eprintln s!"Didn't understand argument(s) {" ".separate args}\n"
    IO.eprintln usage
    pure 1

IO.eprintln 是 IO.println 的一个版本，它输出到标准错误。

并非所有路径都应显示在目录树中。特别是名为 . 或 .. 的文件，因为它们实际上是用于导航的特殊标记，而不是文件本身。应该显示的文件有两种：普通文件和目录：

inductive Entry where
  | file : String → Entry
  | dir : String → Entry

为了确定是否要显示某个文件以及它是哪种条目，doug 依赖 toEntry 函数：

def toEntry (path : System.FilePath) : IO (Option Entry) := do
  match path.components.getLast? with
  | none => pure (some (.dir ""))
  | some "." | some ".." => pure none
  | some name =>
    pure (some (if (← path.isDir) then .dir name else .file name))

System.FilePath.components 在目录分隔符处分割路径名，并将路径转换为路径组件的列表。如果没有最后一个组件，那么该路径就是根目录。如果最后一个组件是一个特殊的导航文件（. 或 ..），则应排除该文件。否则，目录和文件将被包装在相应的构造函数中。

Lean 的逻辑无法确定目录树是否有限。事实上，有些系统允许构建循环目录结构。因此，dirTree 函数必须被声明为 partial：

partial def dirTree (cfg : Config) (path : System.FilePath) : IO Unit := do
  match ← toEntry path with
  | none => pure ()
  | some (.file name) => showFileName cfg name
  | some (.dir name) =>
    showDirName cfg name
    let contents ← path.readDir
    let newConfig := cfg.inDirectory
    doList (contents.qsort dirLT).toList fun d =>
      dirTree newConfig d.path

对 toEntry 的调用是一个嵌套操作 —— 在箭头没有其他含义的位置，如 match，括号是可以省略的。当文件名与树中的条目不对应时（例如，因为它是 ..），dirTree 什么也不做。当文件名指向一个普通文件时，dirTree 会调用一个辅助函数，以当前配置来显示该文件。当文件名指向一个目录时，将通过一个辅助函数来显示该目录，然后其内容将递归地显示在一个新的配置中，其中的前缀已被扩写，以说明它位于一个新的目录中。目录的内容按顺序排序，以便使输出具有确定性，比较依据是 dirLT。

def dirLT (e1 : IO.FS.DirEntry) (e2 : IO.FS.DirEntry) : Bool :=
  e1.fileName < e2.fileName

文件和目录的名称通过 showFileName 和 showDirName 函数来显示：

def showFileName (cfg : Config) (file : String) : IO Unit := do
  IO.println (cfg.fileName file)

def showDirName (cfg : Config) (dir : String) : IO Unit := do
  IO.println (cfg.dirName dir)

这两个辅助函数都委托给了将 ASCII 与 Unicode 设置考虑在内的 Config 上的函数：

def Config.preFile (cfg : Config) :=
  if cfg.useASCII then "|--" else "├──"

def Config.preDir (cfg : Config) :=
  if cfg.useASCII then "|  " else "│  "

def Config.fileName (cfg : Config) (file : String) : String :=
  s!"{cfg.currentPrefix}{cfg.preFile} {file}"

def Config.dirName (cfg : Config) (dir : String) : String :=
  s!"{cfg.currentPrefix}{cfg.preFile} {dir}/"

同样，Config.inDirectory 用目录标记扩写了前缀：

def Config.inDirectory (cfg : Config) : Config :=
  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}

doList 函数可以在目录内容的列表中迭代 IO 操作。由于 doList 只执行列表中的所有操作，并不根据任何操作返回的值来决定控制流，因此不需要使用 Monad 的全部功能，它适用于任何 Applicative 应用程序：

def doList [Applicative f] : List α → (α → f Unit) → f Unit
  | [], _ => pure ()
  | x :: xs, action =>
    action x *>
    doList xs action

6.1.2. 使用自定义单子🔗

虽然这种 doug 实现可以正常工作，但手动传递配置不仅费事还容易出错。例如，类型系统无法捕获向下传递的错误配置。读取器作用不仅可以确保在所有递归调用中都传递相同的配置，而且有助于优化冗长的代码。

要创建一个同时也是 Config 读取器的 IO ，首先要按照求值器示例中的方法定义类型及其 Monad 实例：

def ConfigIO (α : Type) : Type :=
  Config → IO α

instance : Monad ConfigIO where
  pure x := fun _ => pure x
  bind result next := fun cfg => do
    let v ← result cfg
    next v cfg

这个 Monad 实例与 Reader 实例的区别在于，它使用 IO 单子中的 do 标记作为 bind 返回函数的主体，而不是直接将 next 应用于 result 返回的值。由 result 执行的任何 IO 作用都必须在调用 next 之前发生，这一点由 IO 单子的 bind 操作符来保证。 ConfigIO 不是宇宙多态的，因为底层的 IO 类型也不是宇宙多态的。

运行 ConfigIO 操作需要向其提供一个配置，从而将其转换为 IO 操作：

def ConfigIO.run (action : ConfigIO α) (cfg : Config) : IO α :=
  action cfg

这个函数其实并无必要，因为调用者只需直接提供配置即可。不过，给操作命名可以让我们更容易看出代码的各部分会在哪个单子中运行。

下一步是定义访问当前配置的方法，作为 ConfigIO 的一部分：

def currentConfig : ConfigIO Config :=
  fun cfg => pure cfg

这与求值器示例中的 read 相同，只是它使用了 IO 的 pure 来返回其值，而不是直接返回。因为进入一个目录会修改递归调用范围内的当前配置，因此有必要提供一种修改配置的方法：

def locally (change : Config → Config) (action : ConfigIO α) : ConfigIO α :=
  fun cfg => action (change cfg)

doug 中的大部分代码都不需要配置，因此 doug 会从标准库中调用普通的 Lean IO 操作，这些操作当然也不需要 Config。普通的 IO 操作可以使用 runIO 运行，它会忽略配置参数：

def runIO (action : IO α) : ConfigIO α :=
  fun _ => action

有了这些组件，showFileName 和 showDirName 可以修改为使用 ConfigIO 单子来隐式获取配置参数。它们使用嵌套动作来获取配置，并使用 runIO 来实际执行对 IO.println 的调用：

def showFileName (file : String) : ConfigIO Unit := do
  runIO (IO.println ((← currentConfig).fileName file))

def showDirName (dir : String) : ConfigIO Unit := do
  runIO (IO.println ((← currentConfig).dirName dir))

在新版的 dirTree 中，对 toEntry 和 readDir 的调用被封装在 runIO 中。此外，它不再构建一个新的配置，然后要求程序员跟踪将哪个配置传递给递归调用，而是使用 locally 自然地将修改后的配置限定在程序的一小块区域内，在该区域内，它是唯一有效的配置：

partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
  match ← runIO (toEntry path) with
    | none => pure ()
    | some (.file name) => showFileName name
    | some (.dir name) =>
      showDirName name
      let contents ← runIO path.readDir
      locally (·.inDirectory)
        (doList (contents.qsort dirLT).toList fun d =>
          dirTree d.path)

新版本的 main 使用 ConfigIO.run 来调用带有初始配置的 dirTree：

def main (args : List String) : IO UInt32 := do
    match configFromArgs args with
    | some config =>
      (dirTree (← IO.currentDir)).run config
      pure 0
    | none =>
      IO.eprintln s!"Didn't understand argument(s) {" ".separate args}\n"
      IO.eprintln usage
      pure 1

与手动传递配置相比，这种自定义单子有很多优点：

能更容易确保配置被原封不动地向下传递，除非需要更改
传递配置与打印目录内容之间的关系更加清晰
随着程序的增长，除了传播配置外，将有越来越多的中间层无需对配置进行处理，这些层并不需要随着配置逻辑的变化而重写。

不过，也有一些明显的缺点：

随着程序的发展和单子需要更多功能，比如 locally 和 currentConfig 等基本算子都需要更新。
将普通的 IO 操作封装在 runIO 中会产生语法噪音，影响程序的流畅性
手写单子实例是重复性的工作，而且向另一个单子添加读取器作用的技术是一种依赖文档和交流开销的设计模式

使用一种名为 单子转换器 的技术，可以解决所有这些弊端。单子转换器以一个单子作为参数，并返回一个新的单子。单子转换器包括：

转换器本身的定义，通常是一个从类型到类型的函数
假定内部类型已经是一个单子的 Monad 实例
从内部单子“提升”一个操作到转换后的单元的操作符，类似于 runIO.

6.1.3. 将读取器添加到任意单子🔗

在 ConfigIO中，通过将 IO α 包装成一个函数类型，为 IO 添加了读取器作用。 Lean 的标准库有一个函数，可以对任意多态类型执行此操作，称为 ReaderT：

def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) :
    Type (max u v) :=
  ρ → m α

它的参数如下:

ρ 是读取器可以访问的环境
m 是被转换的单子，例如 IO
α 是单子计算返回值的类型 α 和 ρ 都在同一个宇宙中，因为在单子中检索环境的算子将具有 m ρ 类型。

有了 ReaderT，ConfigIO 就变成了:

abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α

它是一个 abbrev，因为在标准库中定义了许多关于 ReaderT 的有用功能，而不可归约的定义会隐藏这些功能。与其让 ConfigIO 直接使用这些功能，不如让 ConfigIO 的行为与 ReaderT Config IO 保持一致。

手动编写的 currentConfig 从读取器中获取了环境。这种作用可以以通用形式定义，适用于 ReaderT 的所有用途，名为 read：

def read [Monad m] : ReaderT ρ m ρ :=
   fun env => pure env

然而，并不是每个提供读取器作用的单子都是用 ReaderT 构建的。类型类 MonadReader 允许任何单子提供 read 操作符：

class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) :
    Type (max (u + 1) v) where
  read : m ρ

instance [Monad m] : MonadReader ρ (ReaderT ρ m) where
  read := fun env => pure env

export MonadReader (read)

类型 ρ 是一个输出参数，因为任何给定的单子通常只通过读取器提供单一类型的环境，所以在已知单子时自动选择它可以使程序编写更方便。

ReaderT 的 Monad 实例与 ConfigIO 的 Monad 实例基本相同，只是 IO 被某个表示任意单子的参数 m 所取代:

instance [Monad m] : Monad (ReaderT ρ m) where
  pure x := fun _ => pure x
  bind result next := fun env => do
    let v ← result env
    next v env

下一步是消除对 runIO 的使用。当 Lean 遇到单子类型不匹配时，它会自动尝试使用名为 MonadLift 的类型类，将实际的单子转换为预期单子。这一过程与使用强制转换相似。 MonadLift 的定义如下：

class MonadLift (m : Type u → Type v) (n : Type u → Type w) where
  monadLift : {α : Type u} → m α → n α

方法 monadLift 可以将单子 m 转换为单子 n。这个过程被称为“提升”，因为它将嵌入到单子中的动作转换成周围单子中的动作。在本例中，它将用于把 IO “提升”到 ReaderT Config IO，尽管该实例适用于任何内部单子 m：

instance : MonadLift m (ReaderT ρ m) where
  monadLift action := fun _ => action

monadLift 的实现与 runIO 非常相似。事实上，只需定义 showFileName 和 showDirName 即可，无需使用 runIO：

def showFileName (file : String) : ConfigIO Unit := do
  IO.println s!"{(← read).currentPrefix} {file}"

def showDirName (dir : String) : ConfigIO Unit := do
  IO.println s!"{(← read).currentPrefix} {dir}/"

原版 ConfigIO 中的最后一个操作还需要翻译成 ReaderT 的形式：locally。该定义可以直接翻译为 ReaderT，但 Lean 标准库提供了一个更通用的版本。标准版本被称为 withReader，它是名为 MonadWithReader 的类型类的一部分：

class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) where
  withReader {α : Type u} : (ρ → ρ) → m α → m α

正如在 MonadReader 中一样，环境 ρ 是一个 outParam。 withReader 操作是被导出的，所以在编写时不需要在前面加上类型类名：

export MonadWithReader (withReader)

ReaderT 的实例与 locally 的定义基本相同：

instance : MonadWithReader ρ (ReaderT ρ m) where
  withReader change action :=
    fun cfg => action (change cfg)

有了这些定义,我们便可以定义新版本的 dirTree:

partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
  match ← toEntry path with
    | none => pure ()
    | some (.file name) => showFileName name
    | some (.dir name) =>
      showDirName name
      let contents ← path.readDir
      withReader (·.inDirectory)
        (doList (contents.qsort dirLT).toList fun d =>
          dirTree d.path)

除了用 withReader 替换 locally 外，其他内容保持不变。

在本节中，用 ReaderT 代替自定义的 ConfigIO 类型并没有节省大量代码行数。不过，使用标准库中的组件重写代码确实有长远的好处。首先，了解 ReaderT 的读者不需要花时间去理解 ConfigIO 的 Monad 实例，也不需要逆向理解单子本身的含义。相反，他们可以沿用自己的初步理解。接下来，给单子添加更多的作用（例如计算每个目录中的文件并在最后显示计数的状态作用）所需的代码改动要少得多，因为库中提供的单子转换器和 MonadLift 实例配合得很好。最后，使用标准库中包含的一组类型类，多态代码的编写方式可以使其适用于各种单子，而无需关心单子转换器的应用顺序等细节。正如某些函数可以在任何单子中工作一样，另一些函数也可以在任何提供特定类型状态或特定类型异常的单子中工作，而不必特别描述特定的具体单子提供状态或异常的方式。

6.1.4. 练习🔗

6.1.4.1. 控制点文件的显示🔗

文件名以点字符 ('.') 开头的文件通常代表隐藏文件，如源代码管理的元数据和配置文件。修改 doug 并加入一个选项，以显示或隐藏以点开头的文件名。应使用命令行选项 -a 来控制该选项。

6.1.4.2. 起始目录作为参数🔗

修改 doug ，使其可以将起始目录作为额外的命令行参数。