我正在阅读CPDT 并且有一个我不理解的例子：
Definition plus_rec : nat -> nat -> nat :=
nat_rec (fun _ : nat => nat -> nat) (fun m => m) (fun _ r m => S (r m)).
除了fun _ : nat => nat -> nat 之外，大部分都是有意义的。我根本不明白这有什么意义，这个函数似乎返回了一个没有值的类型。
我是否误解了关于 Coq 的一些基本内容？那个 lambda 有什么意义？
【问题讨论】：
我们来看看nat_rec：
nat_rec :
forall P : nat -> Set,
P O ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n
它的第一个参数是P，给定nat，返回Set。然后，您将给出集合P O 的一个元素，以及集合P (S n) 的一个元素，假设您有一个来自P n 的元素，最后，您将得到forall n, P n 类型的东西这意味着它可以为您作为输入传入的每个n 构造一个P n 类型的元素（如果您传递O，它将返回您提供的P O，否则它将通过重复构建您的结果第三个参数的应用）。
现在，让你感到困惑的那个 lambda 是我一直在谈论的 P。它被赋予nat 并从中构建“返回类型”。特别是我们试图让nat_rec的返回类型，即forall n : nat, P n成为plus_rec的类型，即nat -> nat -> nat。这可以通过实例化P 来完成，这样对于所有n，P n = nat -> nat。这是我们使用 lambda-term fun _ : nat => nat -> nat 获得的。
该术语忽略输入nat（因为nat_rec 足以构建其类型取决于他们收到的第一个nat 的东西，但部分应用于任何第一个参数的plus_rec 的类型实际上并不取决于该参数的值）。然后它只返回nat -> nat（这是对一个操作数进行部分加法的类型：在返回和nat之前，我们仍然期望nat）。
现在，如果您看一下 nat_rec 部分应用于那个有趣的 lambda 项，类型是：
nat_rec (fun _ : nat => nat -> nat) :
(fun _ : nat => nat -> nat) O ->
(forall n : nat, (fun _ : nat => nat -> nat) n -> (fun _ : nat => nat -> nat) (S n)) ->
forall n : nat, (fun _ : nat => nat -> nat) n
（我刚刚用(fun _ : nat => nat -> nat)回复了P。现在，这简化为：
nat_rec (fun _ : nat => nat -> nat) :
(nat -> nat) ->
(forall n : nat, (nat -> nat) -> (nat -> nat)) ->
forall n : nat, (nat -> nat)
现在这肯定会令人困惑。
您应该将需要给出的第一个参数视为plus 到O 的部分应用的类型。它接收第二个操作数，并返回两者之和：
(fun m => m) (* morally, O + m *)
第二个参数给定一个(n : nat)，一个函数r : nat -> nat，另一个m : nat，需要返回一个最终的nat。它是这群人中最令人困惑的。从道德上讲，r 是 P n，也就是说，给定我们的目标，“一个知道如何将 n 添加到其输入的函数”。再次从道德上讲，最后一个 (nat -> nat) 应该是 P (S n)，即“知道如何将 (S n) 添加到其输入的函数”。特别是，我们将此输入命名为m。你应该能够说服自己结果应该是：
(fun _ r m => S (r m))
(* ignore n, use r (which is the "+ n" function) on m, to get (n + m), and add 1 to get (n + 1) + m *)
有了这一切，我们设法构建了函数plus。
请注意，这是定义plus_rec 的一种非常容易出错的方式，特别是因为您必须非常努力地记住什么是什么，否则您将不会定义您想要的函数，因为打字真的很松散（看看我们在大多数情况下如何忽略n）。事实上，在同一函数的早期草案中存在一个错误，该函数进行了类型检查。
我相信这是为了展示一切是如何隐藏起来的，但不要认为这是你应该定义 plus_rec 的一般方式。
最后，这很难解释，我很确定我的答案不会很清楚。随意删除 cmets，我将编辑答案以使事情更干净。
【讨论】：
Set。不管输入如何，它总是返回相同的类型nat -> nat。