variadic-functions - 如何在 Coq 中使用有关此函数类型的已知信息

Question

假设我有以下类型 typ 代表 bool 或 nat:

Inductive typ : Type := TB | TN.

我还有一个函数可以从 typ 列表和结果类型中提取实际函数类型:

Fixpoint get_types (s: seq typ) (result_type: Type) : Type :=
match s with
| nil => result_type
| x :: xs => match x with
  | TN => nat -> get_types xs result_type
  | TB => bool -> get_types xs result_type
  end
end.
Example get_types_works : get_types (TB :: TN :: nil) nat = bool -> nat -> nat.
Proof. by []. Qed.

现在，我有另一个函数，它将 typ 的列表 s 和 get_types s 类型的函数作为输入:

Fixpoint app (s: seq typ) (constructor: get_types s nat) : nat := 
match s with
| nil => 2 (* Not properly handling empty list case for now *)
| TB :: nil => constructor true
| TN :: nil => constructor 2
| TB :: xs => app xs (constructor true) 
| TN :: xs => app xs (constructor 2)
end. 

在 | 行定义上述函数失败。 TB::nil => 构造函数 true with:

Illegal application (Non-functional construction): 
The expression "constructor" of type "get_types s nat" cannot be applied to the term
 "true" : "bool"

鉴于我们在这里知道 get_types s nat 的类型应该是 bool -> nat，因为 s 的值是 TB::nil，我想知道是否有办法让 Coq 意识到这一点，以便可以定义上述函数？

如果不是，这是 Coq 的限制还是同样适用于其他依赖类型的语言？

编辑:就上下文而言，这不是我要解决的原始问题；这是一个精简版本，显示了我在类型系统上遇到的问题。在实际版本中，不是硬编码 2 和 true，类似 typ 的数据结构还携带数据索引以从内存中解析切片和验证功能。 app 的目标是一个函数，它接受这样的 typ 列表、切片和包含这些类型的记录的构造函数，然后构造该记录的实例从要解析的类型的索引中提取，如果任何验证失败，则返回 None。

Answer 1

原则上你想要的没有错。但是，至少在 Coq 中，有一些简单的规则来检查模式匹配的类型，以便可以在类型中使用有关使用了哪个构造函数的信息。表面语言(在本例中为 Gallina)通过帮助编译(或 desugar)模式匹配来隐藏这种简单性，因此作为用户，您可以编写比底层系统必须处理的更复杂的模式。我对 Idris 不太熟悉，但根据依赖模式匹配的复杂程度，我怀疑您在那里遇到了类似的限制，您必须将代码放入系统可以进行类型检查的形式中。

在这里，您遇到了此模式匹配编译的两个限制。首先是构造函数的类型不是基于 s 上的匹配而专门化的。这很容易通过从 get_types s nat -> nat 计算一个函数来解决，编译器是正确的。

Require Import List.
Import ListNotations.

Inductive typ : Type := TB | TN.

Fixpoint get_types (s: list typ) (result_type: Type) : Type :=
match s with
| nil => result_type
| x :: xs => match x with
  | TN => nat -> get_types xs result_type
  | TB => bool -> get_types xs result_type
  end
end.

Fail Fixpoint app (s: list typ) : get_types s nat -> nat :=
  match s with
  | nil => fun constructor => 2
  | TB :: nil => fun constructor => constructor true
  | TN :: nil => fun constructor => constructor 2
  | TB :: xs => fun constructor => app xs (constructor true)
  | TN :: xs => fun constructor => app xs (constructor 2)
  end.
(* fails due to limitation of termination checker with nested matches *)

...但是您遇到了终止检查器的第二个问题。请注意，您的匹配很复杂:它分析 s 的结构以及它的头部和尾部(如果它是使用 cons 构建的)。最终，所有模式匹配都被编译为单个归纳类型上的嵌套模式匹配。如果你看这个展开，你正在将 s 分解为 t::xs，然后再次将 xs 分解为 t0: :xs'，最后在 xs 上递归。不幸的是，Coq 终止检查器仅将其视为 t0::xs' 并且不将其识别为 s 的子项(它真的想要 xs)。

我很难以类型检查的方式手动编写您的函数，但这里有一个使用功能正确的策略编写的版本。请注意，它产生的定义比任何普通模式匹配都要复杂得多，因为它必须维护由 destruct_with_eqn 产生的证明。但是，该证明对于同时使用 xs 使终止检查器满意并揭示 t0::xs' 对构造函数的应用程序进行类型检查至关重要。它可能很复杂，但您仍然可以正常运行，如最后一行所示。

Fixpoint app (s: list typ) (constructor: get_types s nat) {struct s} : nat.
  destruct s as [|t xs]; simpl in *.
  exact 2.
  destruct_with_eqn xs; simpl in *.
  destruct t; [ exact (constructor true) | exact (constructor 2) ].
  destruct t; simpl in *.
  - apply (app xs).
    subst.
    exact (constructor true).
  - apply (app xs).
    subst.
    exact (constructor 2).
Defined.

Eval compute in app [TB; TN] (fun x y => if x then y+2 else y).
(* = 4
   : nat
*)