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

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

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

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

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

A seq以及该序列长度为某个值的证明。这与例如如何Idris 定义了这种类型：

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

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

One SSReflect 导向书籍 http://ilyasergey.net/pnp/pnp.pdf甚至声称Vect n A样式方法是一种反模式：

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

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

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

在数学应用中，如果您想要定义一个谓词，该谓词是一般不可判定的事物的特化，即使它在您的特定情况下恰好是可判定的，也会出现问题。我在这里讨论的一个例子是用给定的表示来定义组：在 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.