从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

自述文件中引用的参考文献很好地概述了擦除问题。具体来说，这份报告和这篇文章都详细解释了 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示例，靠近文件末尾。