如何利用有关此功能类型的信息的信息

Question

说我有以下类型的typ代表bool或nat：

Inductive typ : Type := TB | TN.

我还具有从 typ s列表和结果类型中提取实际功能类型的函数：

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的 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 => constructor true线上失败：

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的限制还是同样的限制适用于其他相关的语言？

编辑：对于上下文，这不是我要解决的原始问题；这是一个凝结的版本，可以显示我对类型系统的问题。在实际版本中，typ -like数据架构也不是硬编码2和true，还带有数据索引以从内存切片和验证功能中解析。app的目的是一个函数，该函数列出了此类 typ s，一个切片和包含此类类型的记录的构造函数，然后构造该记录的实例，从类型的索引进行解析，或返回None(如果有(验证的失败。

Answer 1

原则上想要的东西没有错。但是，至少在COQ中，有一些简单的规则，即如何进行模式匹配，以便可以在类型中使用有关使用哪个构造函数的信息。表面语言(在这种情况下为Gallina(通过帮助编译(或 desugar (模式匹配来隐藏这种简单性，因此，作为用户，您可以编写比基础系统必须处理的更复杂的模式。我不太熟悉IDRI，而是根据我怀疑您在那里遇到类似限制的依赖模式匹配的方式，您必须将代码适合系统可以键入check。

。

在这里，您遇到了此模式匹配汇编的两个限制。首先是，基于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
*)

Answer 2

因为您用 Idris标记了这一点，所以它是在那里工作的方式：

data Typ = TB | TN
get_types : (args : List Typ) -> (res : Type) -> Type
get_types [] res = res
get_types (TB :: xs) res = Bool -> get_types xs res
get_types (TN :: xs) res = Nat -> get_types xs res
app : (args : List Typ) -> (con : get_types args Nat) -> Nat
app [] con = 2
app (TB :: []) con = con True
app (TN :: []) con = con 2
app (TB :: xs) con = app xs (con True)
app (TN :: xs) con = app xs (con 2)

基本上，您没有问题，因为在args上的匹配时，编译器还将渗透con的类型。例如，如果您用

替换最后一个情况

app (TN :: xs) con = ?hole

调查孔，您会发现编译器有有关con的新信息：

  xs : List Typ
 con : Nat -> get_types xs Nat
--------------------------------------
hole : Nat

Answer 3

还有其他两种定义 app的方法。

第一个使用策略，依赖于induction而不是Fixpoint。

Definition app (s: seq typ) (constructor: get_types s nat) : nat.
Proof.
  induction s as [|t xs].
  - exact 2.
  - destruct xs.
    + destruct t.
      * exact (constructor true).
      * exact (constructor 2).
    + destruct t.
      * exact (IHxs (constructor true)).
      * exact (IHxs (constructor 2)).
Defined.

第二个使用gallina和复杂的图案匹配。

Fixpoint app (s: seq typ) : get_types s nat -> nat :=
  match s return get_types s nat -> nat with
  | nil => fun _ => 2
  | x :: xs =>
    match xs as xs0 return xs = xs0 -> get_types (x::xs0) nat -> nat with
    | nil => fun _ => match x return get_types (x::nil) nat -> nat with
            | TB => fun c => c true
            | TN => fun c => c 2
            end
    | _ => fun e => match e in _ = xs1 return get_types (x::xs1) nat -> nat with
           | eq_refl =>
             match x return get_types (x::xs) nat -> nat with
             | TB => fun c => app xs (c true)
             | TN => fun c => app xs (c 2)
             end
           end
    end eq_refl
  end.

破坏xs时，我们记得原始xs与破坏的东西之间的平等性。我们不需要nil分支中的这种平等，并用fun _丢弃它。在另一个分支中，我们在平等证明(match e(上进行模式匹配，该证明与使用此平等的重写相对应。在eq_refl分支中，我们可以使用原始的xs，从而进行终止检查器允许的递归调用。在模式匹配之外，我们返回xs上图案匹配预期的正确类型。最后要做的是提供xs和xs0平等的证明，但它是 eq_refl。

Answer 4

好吧，我不确定您真正要做什么，但是将代码提交代码的第一步确实是为了为您添加更多结构解释。如果将类型的解释与类型列表分开，则可以轻松地使骨架工作：

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Inductive Typ := TB | TN.
(* Interpretation for types *)
Definition iT w : Type :=
  match w with | TB => bool | TN => nat end.
(* Default witness *)
Definition dw w : iT w :=
  match w with | TB => true | TN => 2 end.
Definition get_types (res : Type) := fix gt (args : list Typ) :=
  match args with
  | [::]        => res
  | [:: w & xs] => iT w -> gt xs
  end.
Variable (dt : Typ).
Fixpoint app (args : list Typ) : get_types (iT dt) args -> iT dt :=
  match args with
  | [::]         => fun gt => dw dt
  | [:: tw & xs] => fun gt => app (gt (dw tw))
  end.

请注意，我也概括了返回类型，因为没有充分的理由将定义定义为nat。一个有趣的练习是修改上述app功能，并证明它等同于Tej的基于战术的版本。