ocaml - __ 在从 Coq 中提取的 Ocaml 中

Question

从 Coq 中提取的 Ocaml 代码包括(在某些情况下)类型 __和一个函数 __定义如下:

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

文档说在过去，这种类型被定义为 unit (因此 __ 可以被视为 () )但是存在(罕见)类型的值 __ 的情况应用于 __ 类型的值.
__使用 Obj 的未记录功能来自 OCaml 的模块，但似乎定义的本质上是一个完全多态的函数，它吃掉它的所有参数(无论它们的数量是多少)。

是否有一些关于 __ 的情况的文档？从理论上(在不可能消除的情况下构造 Coq 术语)和从实际(显示发生这种情况的实际案例)的角度来看，这种类型的值不能被消除并且这种类型的值应用于相同类型的值？

Answer 1

README 中引用的引用文献给出删除问题的一个很好的概述。具体来说，this报告和this文章详细解释了如何删除 CIC 术语的类型方案和逻辑部分，以及为什么必须有 __ x = __ .问题不完全是 __可以应用于自身，但它可以应用于任何事物。

不幸的是，在任何非病理情况下，这种行为是否重要还不清楚。给出的动机是能够提取任何 Coq 术语，并且文档没有提到从实际角度来看真正有趣的任何案例。 3 上给出的示例这是这个:

Definition foo (X : Type) (f : nat -> X) (g : X -> nat) := g (f 0).
Definition bar := foo True (fun _ => I).

执行 Recursive Extraction bar.给出以下结果:

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
| O
| S of nat

(** val foo : (nat -> 'a1) -> ('a1 -> nat) -> nat **)

let foo f g =
  g (f O)

(** val bar : (__ -> nat) -> nat **)

let bar =
  foo (Obj.magic __)

由于 foo在 Type 上是多态的，没有办法简化 f O应用程序在其主体上，因为它可能具有计算内容。但是，由于 Prop是 Type 的子类型, foo也可申请 True ，这就是 bar 中发生的情况.当我们尝试减少 bar ，因此，我们将有 __正在申请 O .

这个特殊情况不是很有趣，因为可以完全内联 foo :

let bar g =
  g __

由于 True不能应用于任何东西，如果 g对应于任何合法的 Coq 术语，它的 __参数也不会应用于任何东西，因此使用 __ = () 是安全的。 (我相信)。但是，在某些情况下，无法预先知道是否可以进一步应用已删除的术语，这使得 __ 的一般定义必要的。例如查看 Fun示例 here , 在文件末尾附近。