6.5. 其他便利功能🔗

6.5.1. 管道操作符🔗

函数通常写在参数之前。当从左往右阅读程序时，这种做法会让人觉得函数的输出是最重要的 —— 函数有一个要实现的目标（也就是要计算的值），在这个过程中，函数会得到参数的支持。但有些程序更容易理解，通过想象不断完善输入来产生输出。针对这些情况，Lean 提供了与 F# 类似的管道操作符。管道操作符在与 Clojure 的线程宏相同的情况下非常有用。

管道 E₁ |> E₂ 是 E₂ E₁ 的缩写。举个例子，求值：

"(some 5)"#eval some 5 |> toString

可得：

"(some 5)"

虽然这种侧重点的变化可以使某些程序的阅读更加方便，但当管道包含许多组件时，才是它真正派上用场的时刻。

有如下定义：

def times3 (n : Nat) : Nat := n * 3

下面的管道：

"It is 15"#eval 5 |> times3 |> toString |> ("It is " ++ ·)

会产生：

"It is 15"

更一般地说，一系列管道 E₁ |> E₂ |> E₃ |> E₄ 是嵌套函数应用 E₄ (E₃ (E₂ E₁)) 的简称。

管道也可以反过来写。在这种情况下，它们并不优先考虑数据转换这个主旨；而是在许多嵌套括号给读者带来困难的情况下，给出明确应用的步骤。前面的例子可以这样写成等价形式：

"It is 15"#eval ("It is " ++ ·) <| toString <| times3 <| 5

是下面代码的缩写：

"It is 15"#eval ("It is " ++ ·) (toString (times3 5))

Lean 的方法点符号（Dot notation）使用点前的类型名称来解析点后操作符的命名空间，其作用与管道类似。即使没有管道操作符，我们也可以写出 [1, 2, 3].reverse 而不是 List.reverse [1, 2, 3] 。不过，管道运算符也适用于使用多个带点函数的情况。 ([1, 2, 3].reverse.drop 1).reverse 也可以写成 [1, 2, 3] |> List.reverse |> List.drop 1 |> List.reverse 。该版本避免了表达式因接受参数而必须使用括号的麻烦，和 Kotlin 或 C# 等语言中方法调用链一样简便。不过，它仍然需要手动提供命名空间。作为最后一种便利功能，Lean 提供了“管道点”（Pipeline dot）操作符，它像管道一样对函数进行分组，但使用类型名称来解析命名空间。使用“管道点”，可以将示例改写为 [1, 2, 3] |>.reverse |>.drop 1 |>.reverse 。

6.5.2. 无限循环🔗

在一个 do 块中，repeat 关键字会引入一个无限循环。例如，一个发送垃圾邮件字符串 "Spam!" 的程序可用它完成：

def spam : IO Unit := do
  repeat IO.println "Spam!"

repeat 循环还支持和 break 和 continue，和 for 循环一样。

feline实现中的函数 dump 使用递归函数来永远运行：

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

利用 repeat 可将这个函数大大缩短：

def dump (stream : IO.FS.Stream) : IO Unit := do
  let stdout ← IO.getStdout
  repeat do
    let buf ← stream.read bufsize
    if buf.isEmpty then break
    stdout.write buf

无论是 spam 还是 dump 都不需要声明为 partial 类型，因为它们本身并不是无限递归的。相反，repeat 使用了一个类型，该类型的 ForM 实例是 partial。部分性不会“感染”函数调用者。

6.5.3. While 循环🔗

在使用局部可变性编程时，while 循环可以方便地替代带有 if 修饰的 break 的 repeat 循环：

def dump (stream : IO.FS.Stream) : IO Unit := do
  let stdout ← IO.getStdout
  let mut buf ← stream.read bufsize
  while not buf.isEmpty do
    stdout.write buf
    buf ← stream.read bufsize

在后端， while 只是 repeat 的一个更简单的标记。