Coq：我可以使用类型参数作为连续参数的类型吗？

Question

简单来说，我可以写

Inductive witness : (X : Type) -> X -> Type :=
  | witness_nat : witness nat 1. (* for example *)

使得X是一个参数，而不是参数，因此我可以让构造函数使用X进行临时多态性？

上下文

我正在尝试对类型判断进行编码，并且我希望它是多态的，因为我对不同种类的术语（Coq类型）有很多类型输入规则，但是所有规则都具有相同的判断形式。

这意味着对于Coq类型A，B，我希望能够执行类似的操作

Inductive typing_judgement : (X : Type) -> context -> X -> myType -> Prop :=
  | type_A : ... (* type terms of Coq type A *)
  | type_B_1 : ... (* type terms of Coq type B, one way *)
  | type_B_2 : ... (* type terms of type B, another way *)

然后就可以在适当的位置inversion在（例如）只与构造函数type_B_1和type_B_2匹配，如果知道X实际上是B。

在Haskell中

我基本上是在模拟GHC的GADTs允许的模式：

data Judgement termType
  = Type_A :: ... -> Judgement A
  | Type_B_1 :: ... -> Judgement B
  | Type_B_2 :: ... -> Judgement B

[编译器足够聪明，可以使用Type_A作为termType ~ A的见证人-尽管我认为编译器无法像inversion那样以相同的方式淘汰匹配项。

Answer 1

是；您只需要forall关键字：

Inductive witness : forall (X : Type), X -> Type :=
  | witness_nat : witness nat 1.