OCaml 的模块语言为何是 agentic 编程的完美搭档

在过去一年里，我做了相当多的 agentic OxCaml 编程，并不断发现 OCaml 在我最近开发的 各种语言 中 完美契合。如果你不熟悉 OCaml，这篇文章将简要说明我为什么这么认为。

随着代码库变得越来越大，编码代理更擅长填充一个‘定义明确的空洞’，而不是将百万行代码库塞进其上下文窗口。OCaml 在 .mli 文件（模块的接口定义）和 .ml 实现之间有清晰的分离。接下来我将用一个包含两个模块的玩具项目来演示，但该技术可扩展到百万行代码库。我们将从 只编写接口 开始，然后 用测试客户端来检验它们，接着 填充实现。之后我们会更深入地 用 OxCaml 模式进行精化，最后 推测形式化证明可以放在哪里。

1 首先只构建模块接口

我们有一个模块 Money 用于跟踪我们的现金（即它永远不应为负）。如果你需要语法方面的帮助，那么 RWO 导览 可能会有所帮助。

(* lib/money.mli *)

type t

val add : t -> t -> t

val sub : t -> t -> t option
(** [sub a b] is [None] if [b > a]. *)

val to_string : t -> string
(** [to_string m] is e.g. ["£3.05"]. *)

Book 模块是一个存款和取款的列表。

(* lib/book.mli *)

type t

val empty : t
val deposit : Money.t -> t -> t

val withdraw : Money.t -> t -> (t, [ `Insufficient of Money.t ]) result
(** [`Insufficient bal] carries the balance that was too small. *)

val balance : t -> Money.t

注意，我们还没有任何实现，但即便如此，我们定义的类型仍然可以相互引用彼此的模块。这个 OCaml 项目可以通过 dune 指令来编译，以抑制对实现的需求。

(library
 (name ledger)
 (modules_without_implementation money book))

现在魔法开始了，我们可以仅凭这些关于它们应如何协同工作的描述来对项目进行类型检查。

$ dune build @check

这个接口编译时没有警告，所以是时候用一个测试二进制文件来检验我们初生的接口了！

2 为此接口构建一个测试客户端

接下来编写一个二进制文件，我们可以测试刚刚定义的接口是否足够精确，以便在外部实际使用。

(* bin/main.ml *)
open Ledger

let () =
  let ( let* ) = Option.bind in
  let r =
    let* ten = Money.of_pence 1000 in
    let* three = Money.of_pence 305 in
    let b = Book.deposit ten Book.empty in
    match Book.withdraw three b with
    | Ok b -> Some (Money.to_string (Book.balance b))
    | Error _ -> None
  in
  print_endline (Option.value r ~default:"failed")

编译时我们首先意识到，我们的接口过于抽象，因此我们无法创建 Money.t！这导致构建失败：

$ dune build @check
File "bin/main.ml", line 5, characters 15-29:
5 |     let* ten = Money.of_pence 1000 in
                   ^^^^^^^^^^^^^^
Error: Unbound value "Money.of_pence"

因此我们编辑接口，添加构造函数：

(* lib/money.mli *)
type t

val of_pence : int -> t option
(** [of_pence n] is [None] if [n < 0]. *)

现在二进制文件通过了类型检查，但在链接时失败，抱怨没有实现。但由于类型检查器已经通过，我们知道这个接口足够好，值得去实现！

$ dune build ./bin/main.exe
Error: No implementations provided for the following modules:
         "Ledger__Money" referenced from bin/.main.eobjs/native/dune__exe__Main.cmx
         "Ledger__Book" referenced from bin/.main.eobjs/native/dune__exe__Main.cmx

3 逐个填充模块实现

我们现在可以将 Money 交给编码代理，并指示它读取接口（.mli）文件，然后按依赖顺序开始实现模块实现，每个模块都有测试（例如 expect 测试，它将预期输出保留在代码旁边）。

(* lib/money.ml *)
type t = int

let of_pence n = if n < 0 then None else Some n
let add = ( + )
let sub a b = if b > a then None else Some (a - b)
let to_string m = Printf.sprintf "£%d.%02d" (m / 100) (m mod 100)

现在 dune 链接错误只抱怨 Ledger__Book。然后代理继续编写 Book 模块，并带有类似的指示，即只读取接口文件。

这随后又引出了接口的另一个问题，因为编写 Book.empty 表明需要一个起始余额。此时，代理利用其上下文驱动的判断力，要么使用 of_pence，要么向 Money 添加一个辅助函数：

File "lib/book.ml", line 3, characters 12-22:
3 | let empty = Money.zero
                ^^^^^^^^^^
Error: Unbound value "Money.zero"

如果用户（或代理目标）同意重新评估接口设计，那么 Book 接口会获得一个 zero 函数。

3.1 阻止代理走捷径

对于 Book 中的代理来说，一个诱人的捷径是将钱视为普通整数，并在该实现中直接进行操作：

(* lib/book.ml *)
type t = Money.t

let empty = Money.zero
let deposit m b = Money.add m b
let withdraw m b = if m > b then Error (`Insufficient b) else Ok (b - m)
let balance b = b

然而，这在 OCaml 中会导致类型错误：

Error: The implementation "lib/book.ml"
       does not match the interface "lib/.ledger.objs/byte/ledger__Book.cmi":
       Values do not match:
         val withdraw : int -> int -> (int, [> `Insufficient of int ]) result
       is not included in
         val withdraw : t -> t -> (t, [ `Insufficient of t ]) result
       Type "int" is not compatible with type "t"

agent 无法直接减去便士，因为 OCaml 接口强制规定只有 Money 模块才能对该类型的值执行此操作。 方便的是，编译器会拒绝它，并给出足够有用的错误信息，让 agent 能够根据 Money 接口写出正确的实现。

(* lib/book.ml *)
type t = Money.t

let empty = Money.zero
let deposit m b = Money.add m b

let withdraw m b =
  match Money.sub b m with
  | Some b' -> Ok b'
  | None -> Error (`Insufficient b)

let balance b = b

现在可以完整地端到端构建了，耶！

$ dune build ./bin/main.exe && ./_build/default/bin/main.exe
£6.95

这项技术的妙处在于，它可以扩展到拥有数百个 mli 文件的庞大项目，而且这种 agentic 工作流允许在着手进行昂贵的实现之前，先廉价地定义一组复杂的接口。OCaml 的分离编译让构建时间保持得非常快，因此我们拥有快速的编辑/编译循环。

4 用 OxCaml 模式进一步精炼

不过我们不必止步于 OCaml 接口！OxCaml 是 Jane Street 的一个语言扩展，它提供了模式注解，可以扩展这一工作流。（如果你想了解更多，我们在 ICFP 2025 上举办了一场OxCaml 教程。）

我们现在可以运行一次 agentic 处理，来精炼我们的接口，使其拥有更多检查：

(* lib/money.mli *)
type t : immutable_data

val add : t @ local -> t @ local -> t
val to_string : t @ local -> string

(* lib/book.mli *)
type t : immutable_data

immutable_data 注解承诺 Money.t 或 Book.t 在其实现中不包含可变状态，因此它可以（例如）在并行线程之间自由共享。

@ local 确保函数不会持有其参数，因此调用者可以传入一个栈分配的值，而不必进行堆分配。

一个决定用可变余额来“优化”Book 的 agent 现在会失败：

type t = { mutable bal : Money.t }

Error: The implementation "lib/book.ml"
       does not match the interface "lib/.ledger.objs/byte/ledger__Book.cmi":
       Type declarations do not match:
         type t = { mutable bal : Money.t; }
       is not included in
         type t : immutable_data
       The kind of the first is
           mutable_data with Money/2.t @@ forkable unyielding many
         because of the definition of t at file "lib/book.ml", line 1, characters 0-34.
       But the kind of the first must be a subkind of immutable_data.
       The first mode-crosses less than the second along:
         contention: mod uncontended ≰ mod contended
         visibility: mod read_write ≰ mod immutable

诚然，这个错误对人类用户来说有点晦涩（OxCaml 正在改进这一点），但对于拥有OxCaml 技能的 agent 来说没问题。（我在一个沙盒化 devcontainer 中运行这些 agent。）至关重要的是，这些模式注解帮助阻止了 agent 引入一个微妙的错误，该错误在跨多个处理器使用时可能会损坏数据。

5 在精炼的兔子洞里越挖越深

前面所有的 OxCaml 模式都是由编译器静态定义的，而编译器正变得越来越强大。今年夏天的 ICFP 2026 mode crossings 论文展示了编译器如何自动为某些类型的值强化模式，这就是我们的 Money.t 能够简洁地声明 immutable_data 的方式。但如果我们还能在接口中表达任意逻辑条件，那岂不是更酷？！

这里是一个使用 Gospel 风格规范的 Money 草图。我实际上还没有编译过这个，但你会明白意思的：

(* lib/money.mli *)
type t
(*@ model pence : integer
    invariant pence >= 0 *)

val sub : t -> t -> t option
(*@ r = sub a b
    ensures match r with
            | None -> a.pence < b.pence
            | Some c -> c.pence = a.pence - b.pence *)

这个注释现在是一个机器检查的契约，因此每个实现都必须保证满足这些前置和后置条件。

大约二十年前，Patrick Rondon 和 Ranjit Jhala 研究过一个具有这些特性的 liquid OCaml（PLDI 2008 论文）。我非常兴奋它正回归现代 OxCaml，因为我长期以来一直羡慕 Liquid Haskell :-)

使用 OCaml 的模块系统作为这些形式化扩展的基础，其美妙之处在于我上面勾勒的分离编译架构意味着，即使在百万行代码库上，编辑/反馈循环也很快。注解的分层还让我们能够逐步增加代码的规范程度，而不必堆砌大量的单元测试。

这对智能体来说是上下文高效的，并且随着代码变得越来越复杂，也能保持人类的理智。我们也才刚刚开始研究如何在用户界面中可视化这类约束，比如 Hazel 中正在进行的工作，以及我们自己关于 双向类型切片 的工作，用于调试类型错误（另外，这最后一篇论文刚刚被 POPL 2027 有条件接收，我对此非常兴奋，之后会写更多相关内容！）