从 Coq 提取 Prop 到 Haskell 会导致空类型答案

【问题标题】：Extracting Prop from Coq to Haskell results in empty type从 Coq 提取 Prop 到 Haskell 会导致空类型
【发布时间】：2019-04-25 15:13:43
【问题描述】：

我试图确保在将 Coq 提取到 Haskell 时丢弃无用的Prop。但是，当我使用以下示例时，我看到 divides 和 prime 都被提取为 Haskell 空类型。这是为什么呢？

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
  exists (m : nat), ((mult m n) = p).

(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
  (p > 1) /\ (forall (n : nat), ((divides n p) -> ((n = 1) \/ (n = p)))).

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" isPrime divides prime.

这就是divides 和prime 发生的事情：

type Divides = ()

type Prime = ()

提取它们有什么用？

【问题讨论】：

如果将Prop 更改为Type 会怎样？我认为Prop 的部分观点是相同Prop 的两个证明可以被视为相同（在标准库中有一个称为proof_irrelevance 的公理）。这将对应于每个Prop 只有一个居民（Haskell 中的() 就是这种情况）。我不确定是否总是这样。我知道在像 HoTT 这样的系统中，你不一定想要证明无关紧要，但也许这是通过使用 Type 而不是 Prop 来捕获的（或者你可能只是不使用 proof_irrelevance 公理？）。
另外，我怀疑还是会有一些限制。毕竟，Coq 有一个依赖类型的类型系统，而 Haskell 没有（尽管我相信 GHC 最终会朝着这个方向发展）。
那些不是空类型，而是单元类型。空类型没有像Void这样的（非底部）居民，而单元类型()作为居民，即()。
@chi 很棒的观察。提取器似乎可以使用 newtype Void = Void Void 和 type Divides = Void 之类的东西。然后将 undefined 放在每个地方都需要 Divides 类型的术语。
@AntonTrunov 实际上，我更喜欢当前的翻译。滥用底部感觉不对。最多，我会使用Void 来翻译无人居住的类型（但这样做很难，因为我们无法决定）。

标签： haskell coq

【解决方案1】：

这是预期的行为。来自Prop 的东西是命题，这意味着它们在计算上是不相关的，因为命题的存在是为了确保正确性，例如表示算法的前置条件和后置条件，不参与计算。

这种情况类似于静态类型语言中的类型——人们通常希望从运行时删除类型。在这里，我们也希望删除作为证明的条款。

这由 Coq 的类型系统支持，该系统禁止将逻辑信息从 Prop 中的类型泄漏到 Type，例如

Definition foo : True \/ True -> nat :=
  fun t => match t with
        | or_introl _ => 0
        | or_intror _ => 42
        end.

结果

Error:
Incorrect elimination of "t" in the inductive type "or":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

一个自然的问题出现了：

所以理想情况下，divides 和 prime 应该从提取的文件中完全删除，对吧？它们怎么会存在那里？

正如 Pierre Letouzey 在他的 overview of extraction in Coq 中解释的那样：

现在让我们总结一下 Coq 提取的现状。 [7] 中描述的理论提取函数仍然具有相关性，并用作提取系统的核心。这个函数折叠（但不能完全删除）逻辑部分（存在于排序Prop）和类型。完全删除会导致术语评估发生危险的变化，在某些情况下甚至会导致错误或无法终止。

【讨论】：

所以理想情况下 divides 和 prime 应该从提取的文件中完全删除，对吗？它们怎么会存在那里？
@OrenIshShalom 好问题！更新了答案。