2

简单来说，我可以写吗

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

这样这X是一个参数，而不是一个参数，所以我可以让构造函数使用X?

语境

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

这意味着，对于 Coq types 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.

在哈斯克尔

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

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

编译器足够聪明，可以Type_A用作见证termType ~ A- 尽管我认为它不能以同样的方式消除匹配臂inversion。

4

1 回答 1

1

是的; 你只需要forall关键字：

Inductive witness : forall (X : Type), X -> Type :=
  | witness_nat : witness nat 1.
于 2020-03-29T16:25:30.240 回答