为什么新的依赖类型语言没有采用 SSReflect 的方法？

Question

我在 Coq 的 SSReflect 扩展中发现了两个约定，它们看起来特别有用，但我还没有看到它们在较新的依赖类型语言（Lean、Agda、Idris）中被广泛采用。

首先，在可能的情况下，谓词表示为布尔返回函数，而不是归纳定义的数据类型。这在默认情况下带来了可判定性，为计算证明开辟了更多机会，并通过避免证明引擎需要携带大量证明条款来提高检查性能。我看到的主要缺点是在证明时需要使用反射引理来操纵这些布尔谓词。

其次，具有不变量的数据类型被定义为包含简单数据类型和不变量证明的相关记录。例如，固定长度的序列在 SSReflect 中定义如下：

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

seq 和该序列长度为特定值的证明。这与例如Idris 定义了这种类型：

data Vect : (len : Nat) -> (elem : Type) -> Type 

一种依赖类型的数据结构，其中不变量是其类型的一部分。 SSReflect 方法的一个优点是它允许重用，因此例如为seq 定义的许多函数以及关于它们的证明仍然可以与tuple 一起使用（通过对底层seq 进行操作），而与Idris 一起使用' 像reverse、append 之类的方法需要为Vect 重写。 Lean 实际上在其标准库vector 中有一个等效的 SSReflect 样式，但它也有一个 Idris 样式的 array，它似乎在运行时有一个优化的实现。

一个SSReflect-oriented book 甚至声称Vect n A 风格的方法是一种反模式：

依赖类型语言和 Coq 中的一个常见反模式是将这些代数属性编码到数据类型和函数本身的定义中（一个规范的例子 这种方法中的一种是长度索引列表）。虽然这种方法看起来很吸引人，但正如它所展示的那样 依赖类型捕获数据类型和函数的某些属性的能力，它 本质上是不可扩展的，因为总会有另一个感兴趣的属性，它还没有被 由数据类型/函数的设计者预见，因此必须将其编码为外部事实 反正。这就是为什么我们提倡这种方法，其中数据类型和函数被定义为 close 程序员尽可能定义它们的方式，以及它们的所有必要属性 分别证明。

因此，我的问题是，为什么这些方法没有被更广泛地采用。是否有我遗漏的缺点，或者它们的优点在对依赖模式匹配的支持比 Coq 更好的语言中不那么重要？

Answer 1

我可以就第一点提供一些想法（将谓词定义为布尔返回函数）。我对这种方法的最大问题是：那么根据定义，该函数不可能有错误，即使结果证明它计算的不是你想要计算的。在许多情况下，如果您必须在其定义中包含谓词的决策过程的实现细节，它也会掩盖您所说的谓词的实际含义。

在数学应用中，如果您想定义一个谓词，它是对一般情况下不可判定的事物的特化，即使它恰好在您的特定情况下是可判定的，也会存在问题。我在这里谈论的一个例子是用给定的表示来定义组：在 Coq 中，定义它的一种常用方法是 setoid ，其底层集合是生成器中的正式表达式，而“word”给出的等式等价”。一般来说，这种关系是不可判定的，尽管在许多特定情况下它是可判定的。但是，如果您仅限于定义具有单词问题可判定的表示的组，那么您将失去定义将所有不同示例联系在一起的统一概念的能力，并一般证明关于有限表示或有限表示组的事情。另一方面，将词等价关系定义为抽象的Prop 或等价物很简单（如果可能有点长）。

就我个人而言，我更喜欢先给出最透明的谓词定义，然后在可能的情况下提供决策过程（返回{P} + {~P} 类型值的函数是我的偏好，尽管返回布尔值的函数也可以很好地工作）。 Coq 的类型类机制可以提供一种方便的方式来注册此类决策过程；例如：

Class Decision (P : Prop) : Set :=
decide : {P} + {~P}.
Arguments decide P [Decision].

Instance True_dec : Decision True := left _ I.
Instance and_dec (P Q : Prop) `{Decision P} `{Decision Q} :
  Decision (P /\ Q) := ...

(* Recap standard library definition of Forall *)
Inductive Forall {A : Type} (P : A->Prop) : list A -> Prop :=
| Forall_nil : Forall P nil
| Forall_cons : forall h t, P h -> Forall P t -> Forall P (cons h t).
(* Or, if you prefer:
Fixpoint Forall {A : Type} (P : A->Prop) (l : list A) : Prop :=
match l with
| nil => True
| cons h t => P h /\ Forall P t
end. *)

Program Fixpoint Forall_dec {A : Type} (P : A->Prop)
  `{forall x:A, Decision (P x)} (l : list A) :
  Decision (Forall P l) :=
  match l with
  | nil => left _ _
  | cons h t => if decide (P h) then
                  if Forall_dec P t then
                    left _ _
                  else
                    right _ _
                else
                  right _ _
  end.
(* resolve obligations here *)
Existing Instance Forall_dec.

Answer 2

这在默认情况下带来了可判定性，为计算证明提供了更多机会，并通过避免证明引擎需要携带大量证明条款来提高检查性能。

您不必像Edwin Brady's thesis 中以“强制优化”的名义所描述的那样使用大术语。 Agda 确实有影响类型检查的强制（特别是如何计算宇宙是相关的），但我不确定仅在类型检查时使用的东西是否真的在运行时之前被删除。无论如何，Agda 有两个无关的概念：.(eq : p ≡ q) 是通常的无关（意思是 eq 在类型检查时是无关的，所以它在定义上等于任何其他此类类型的术语）和..(x : A) 是脊柱无关（不是确定这是否是一个正确的术语。我认为 Agda 消息来源称这种东西为“非严格无关”），字面意思是删除计算上不相关但并非完全不相关的术语。所以你可以定义

data Vec {α} (A : Set α) : ..(n : ℕ) -> Set α where
  [] : Vec A 0
  _∷_ : ∀ ..{n} -> A -> Vec A n -> Vec A (suc n)

和n 将在运行时间之前被擦除。或者至少它看起来是这样设计的，很难确定，因为 Agda 有很多文档记录不完整的特性。

而且你可以在 Coq 中编写那些零成本证明，因为它也实现了与 Prop 中的内容无关。但是不相关性在 Coq 的理论中根深蒂固，而在 Agda 中它是一个单独的功能，因此完全可以理解，为什么人们在 Coq 中比在 Agda 中更容易使用不相关性。

SSReflect 方法的一个优点是它允许重用，因此例如为seq 定义的许多函数以及关于它们的证明仍然可以与tuple 一起使用（通过对底层seq 进行操作），而使用 Idris 的方法，如 reverse、append 等需要为 Vect 重写。

如果您无论如何都必须证明属性并且这些证明与在索引数据上定义的函数具有相同的复杂性，那么这并不是真正的重用。做统一机制的工作并传递明确的证明并应用引理从suc (length xs) ≡ n（以及sym、trans、subst 和所有其他统一机制的引理）也很不方便在许多情况下可以拯救你）。此外，由于滥用命题相等，您会失去一些清晰度：使用 xs : List A; length xs ≡ n + m 而不是 xs : Vec A (n + m) 不会提高您的上下文的可读性，特别是如果它们通常是巨大的。还有另一个问题：有时使用 SSReflect 的方法定义一个函数更难：你提到 reverse 为 Vect，我挑战你从头开始定义这个函数（reverse 为 List 作为“重用" 引擎盖下的部分)，然后将您的解决方案与 Agda 标准库中 Data.Vec 中的定义进行比较。如果默认情况下您没有为命题启用无关性（Agda 就是这种情况），那么如果您想证明 reverse (reverse xs) ≡ xs，那么您还需要证明有关证明的属性，这是很多非- 简单的样板。

所以 SSReflect 的方法并不完美。另一个也是。有什么可以改善两者的吗？是的，装饰品（见Ornamental Algebras, Algebraic Ornaments 和The essence of ornaments）。您可以通过应用相应的装饰代数从List 轻松获得Vec，但我不能说您会从中获得多少代码重用以及类型是否会让您发疯。我听说人们实际上在某个地方使用了装饰品。

所以并不是说我们有一个理想的 SSReflect 解决方案而其他人拒绝采用它。只是希望有一种更合适的方式来实现实际的代码重用。

更新

Anton Trunov 在他们的评论中让我意识到我有点过于 Agda 的思想，而且 Coq 中的人有可以大大简化证明的策略，所以在 Coq 中证明通常更容易（前提是你拥有像CPDT 书中的crush 这样的武器），而不是在数据上定义函数。好吧，那么我猜想证明默认情况下的无关性和重型策略机制是 SSReflect 的方法在 Coq 中有效的原因。