交互式编辑

到目前为止，我们已经看到了几个例子，说明了 Idris 的依值类型系统如何通过更精确地描述函数的*类型*中的预期行为来增强对函数正确性的信心。我们还看到了类型系统如何通过允许程序员描述对象语言的类型系统来帮助嵌入式 DSL 开发的示例。然而，精确类型给我们的不仅仅是程序的验证——我们还可以使用类型系统交互式地来帮助编写*按构造正确*的程序，交互。

Idris REPL 提供了几个用于检查和修改程序部分的命令，基于它们的类型，例如模式变量的大小写分割，检查孔的类型，甚至是基本的证明搜索机制。在本节中，我们将解释文本编辑器如何利用这些功能，特别是如何在 Vim 中这样做。 Emacs 的交互模式也可用，自 2021 年 2 月 23 日起针对 Idris 2 兼容性进行了更新。

在 REPL 中编辑

备注

为了尽量减少依赖，Idris2 的 REPL 不支持 readline。遗憾的是，这意味着无法使用行编辑、持久历史和补全等功能。一个实用的解决方法是安装 rlwrap，只需用 rlwrap idris2 启动 Idris2 REPL，即可获得上述所有功能。

REPL 提供了许多命令（下文将简要介绍），可以基于当前加载的模块生成新的程序片段。它们的一般格式如下：

:command [line number] [name]

也就是说，每个命令都作用于特定的源代码行和名称，并输出一个新的程序片段。每个命令还有一种变体，可以*就地*更新源文件：

:command! [line number] [name]

你也可以用 idris2 --client 让 Idris 以一种模式运行 REPL 命令，显示结果后退出。例如：

$ idris2 --client ':t plus'
Prelude.plus : Nat -> Nat -> Nat
$ idris2 --client '2+2'
4

文本编辑器可以结合这些命令，实现交互式编辑支持。

编辑命令

:addclause（添加子句）

:addclause n f 命令（缩写为 :ac n f）会为第 n 行声明的函数 f 创建一个模板定义。例如，如果第 94 行开始的代码包含：

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c

那么执行 :ac 94 vzipWith 会得到：

vzipWith f xs ys = ?vzipWith_rhs

变量名会根据程序员给出的提示选择，如有必要，系统会自动添加数字以保证唯一性。可以如下方式给出提示：

%name Vect xs, ys, zs, ws

这声明了 Vect 家族类型生成的变量名应按 xs、ys、zs、ws 的顺序选择。

:casesplit（分割模式）

:casesplit n c x 命令（缩写为 :cs n c x）会将第 n 行第 c 列的模式变量 x 拆分为所有可能的模式形式，并移除因统一失败而不可能出现的情况。例如，如果第 94 行开始的代码是：

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f xs ys = ?vzipWith_rhs

那么执行 :cs 96 12 xs 会得到：

vzipWith f [] ys = ?vzipWith_rhs_1
vzipWith f (x :: xs) ys = ?vzipWith_rhs_2

也就是说，模式变量 xs 被拆分为两种可能的情况：[] 和 x :: xs。变量名的选择仍然遵循同样的规则。如果我们用 :cs! 更新文件后，在同一行对 ys 进行分割，会得到：

vzipWith f [] [] = ?vzipWith_rhs_3

也就是说，模式变量 ys 只被拆分为一种情况 []，因为 Idris 发现另一种可能 y :: ys 会导致统一失败。

:addmissing（补全缺失）

:addmissing n f 命令（缩写为 :am n f）会为第 n 行的函数 f 添加所有必要的分支，使其覆盖所有输入。例如，如果第 94 行开始的代码是：

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1

那么执行 :am 96 vzipWith 会得到：

vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

也就是说，系统发现缺少空向量的情况，自动生成所需分支，并移除会导致统一失败的分支。

:proofsearch（证明搜索）

:proofsearch n f 命令（缩写为 :ps n f）会通过证明搜索为第 n 行的孔 f 寻找一个值，尝试本地变量、递归调用和所需类型族的构造器。它还可以接受一个*提示*列表，即可尝试用于解决孔的函数。例如，如果第 94 行开始的代码是：

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

那么执行 :ps 96 vzipWith_rhs_1 会得到

[]

之所以这样，是因为它在寻找长度为 0 的 Vect，而空向量是唯一的可能。同理，或许令人惊讶的是，如果我们尝试解决 :ps 97 vzipWith_rhs_2，也只有一种可能：

f x y :: vzipWith f xs ys

这是因为 vzipWith 的类型足够精确：结果向量必须是非空的（即 ::）；第一个元素类型为 c，唯一的获取方式是对 x 和 y 应用 f；最后，向量的尾部只能递归构造。

:makewith（添加 with）

:makewith n f 命令（缩写为 :mw n f）会为某个模式分支添加 with。例如，回忆一下 parity。如果第 10 行是：

parity (S k) = ?parity_rhs

那么执行 :mw 10 parity 会得到：

parity (S k) with (_)
  parity (S k) | with_pat = ?parity_rhs

如果我们将占位符 _ 替换为 parity k，并用 :cs 11 with_pat 对 with_pat 进行分割，会得到如下模式：

parity (S (plus n n)) | even = ?parity_rhs_1
parity (S (S (plus n n))) | odd = ?parity_rhs_2

注意，这里的模式分割已经将模式标准化（用 plus 替代了 +）。无论如何，交互式编辑极大简化了依值模式匹配的实现，让程序员能直观看到所有有效模式。

Vim 中的交互式编辑

Vim 的编辑器模式提供了语法高亮、缩进和基于上述命令的交互式编辑支持。交互式编辑通过以下编辑器命令实现，每个命令都会直接更新缓冲区：

\a 为光标所在行声明的名称生成模板定义
（对应 :addclause 命令）。
\c 对光标处的变量进行模式分割
（对应 :casesplit）。
\m 为光标处的名称补全缺失分支
（对应 :addmissing）。
\w 添加 with 分支（对应 :makewith）。
\s 对光标下的孔进行证明搜索
（对应 :proofsearch）。

此外，还有用于调用类型检查器和求值器的命令：

\t 显示光标下（全局可见）名称的类型。
对于孔，会显示上下文和期望类型。
\e 提示输入要求值的表达式。
\r 重新加载并类型检查缓冲区。

Emacs 模式也提供了对应的命令。其他编辑器也可以通过 idris2 --client 以相对简单的方式实现支持。更复杂的支持可以通过 IDE 协议实现（Idris 2 的协议文档尚未发布，但大体兼容 Idris 1 的协议，详见 Idris 1 IDE 协议文档）。