__ OCaml中从Coq的提取

Question

从Coq的提取

ocaml的代码包括（在某些情况下）一个类型__和定义为函数__如下：

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

文档说，在过去，这种类型被定义作为unit（因此__可以被视为()），但是存在（类型__）的值被应用于__类型的值的（罕见）情况。

__使用来自OCaml的Obj模块的未公开的函数，但似乎定义的东西本质上是一个完全多态的函数，可以消耗所有参数（无论它们的数量是多少）。

是否有一些关于__不能被消除并且这种类型的值被应用于相同类型的值的情况的一些文档，无论是从理论（构建的Coq术语，其中消除是不可能的）和实际的（示出发生这种情况的现实情况）的观点？

Answer 1

README中引用的参考文献很好地概括了擦除问题。具体而言，this报告和this文章exaplain详细说明了如何删除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对应于任何法律勒柯克来看，其__论点也不会适用于任何事情，因此它是安全的__ =()（我相信）。但是，在某些情况下，无法预先知道是否可以进一步应用已擦除的术语，这使得必须使用__的一般定义。请检查文件末尾附近的Fun示例here。