__ 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。