小编Geo*_*nov的帖子

我正在努力使Coq中的Free Selective Applicative Functors正式化，但是我在通过归纳法对具有非均匀类型参数的归纳数据类型进行挣扎。

让我简要介绍一下我正在处理的数据类型。在Haskell中，我们将自由选择函子编码为GADT：

data Select f a where
    Pure   :: a -> Select f a
    Select :: Select f (Either a b) -> f (a -> b) -> Select f b

关键是b第二个数据构造函数中的存在类型变量。

我们可以将此定义转换为Coq：

Inductive Select (F : Type -> Type) (A : Set) : Set :=
    Pure   : A -> Select F A
  | MkSelect : forall (B : Set), Select F (B + A) -> F (B -> A) -> Select F A. …