Coq: я могу использовать аргумент типа в качестве типа последовательного аргумента? - PullRequest
Новая
       25

Coq: я могу использовать аргумент типа в качестве типа последовательного аргумента?

2 голосов
/ 29 марта 2020

Проще, можно ли написать 

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

так, чтобы X был аргументом, а не параметром, поэтому я могу позволить конструкторам выполнять ad-ho c полиморфизм с X?

Контекст

Я пытаюсь закодировать суждение при наборе текста, и мне бы хотелось, чтобы оно было полиморфным c, потому что у меня много правил печатания для разных типов терминов (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.

In Haskell

Я в основном макетирование, которое GH C GADTs допускает: 

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

, где компилятор достаточно умен, чтобы использовать Type_A в качестве свидетеля termType ~ A - хотя я не думаю, он может убирать спички так же, как inversion может.

1 Ответ

1 голос
/ 29 марта 2020

Да; вам просто нужно ключевое слово forall: 

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