在 Coq 中继承不同类型的类型类

Question

这是我之前问题的后续问题：Multiple Typeclass Inheritance in Coq，但这是关于期望不同种类的类型类（我猜是 Haskell 术语？）。

我有一个类型类 Collection，它需要一个 Type -> Type 和一个类型类 Monoid，它需要一个 Type，我想我知道如何调和它们，但是我'我在使用 Monoid 函数时遇到问题。

Class Sequence (S : Type -> Type)
  foldr empty insert append
  `{C : Collection S foldr empty insert}
  `{M : Monoid (forall A, S A) append empty} :=
{
  insert_append_id :
    forall (A : Type) (h : S A) (x : A),
    append A (insert A x (empty A)) h = insert A x h
}.

并且（修剪后的）错误是：

Error:
In environment
Sequence :
forall (S : Type -> Type)
  (append : (forall A : Type, S A) ->
            (forall A : Type, S A) -> forall A : Type, S A)
[...]
S : Type -> Type
empty : forall A : Type, S A
append :
(forall A : Type, S A) -> (forall A : Type, S A) -> forall A : Type, S A
[...]
M : Monoid (forall A : Type, S A) append empty
A : Type
h : S A
x : A
The term "A" has type "Type" while it is expected to have type
 "forall A : Type, S A".

我还以为我真的很聪明，想出了(forall A, S A)在Monoid继承中，但现在我不太确定了。 Monoid empty 的类型看起来是正确的，但是 append 的类型对我来说没有任何意义。

在我看来，我要么在 Monoid 继承类型上犯了错误，要么有某种方法可以为 append 提供我没有看到的正确类型。还是其他地方有错误导致了这个问题？

编辑：我想出了一个不同的 Monoid 声明，它似乎更接近我想要的，但仍然不起作用。

Class Sequence (S : Type -> Type)
  foldr empty insert (append : forall A, S A -> S A -> S A)
  `{C : Collection S foldr empty insert}
  `{M : forall (A : Type), Monoid (S A) (append A) (empty A)} :=
{
  insert_append_eq :
    forall (A : Type) (h : S A) (x : A),
    append A (insert A x (empty A)) h = insert A x h
}.

以及新的错误：

Error:
Could not find an instance for "Semigroup (S A) (append A)" in environment:

S : Type -> Type
foldr : forall A B : Type, (A -> B -> B) -> B -> S A -> B
empty : forall A : Type, S A
insert : forall A : Type, A -> S A -> S A
append : forall A : Type, S A -> S A -> S A
F : Foldable S foldr
U : Unfoldable S empty insert
C : Collection S foldr empty insert
A : Type

Answer 1

不，幺半群是应用于特定 A 的特定 S。你不能进一步概括它。下面的代码应该可以工作，但我无法测试它。

Class Sequence (S : Type -> Type) (A : Type)
  foldr empty insert append
  `{C : Collection S foldr empty insert}
  `{M : Monoid (S A) (append A) (empty A)} :=
{
  insert_append_id :
    forall (h : S A) (x : A),
    append _ (insert _ x (empty _)) h = insert _ x h
}.

或者，您可以使用不同类型的幺半群。

Class Mon (F : Type -> Type) (mul : forall X, F X -> F X -> F X)
  (one : forall X, F X) : Type :=
{
  idl : forall X x, mul X (one X) x = x;
  idr : forall X x, mul X x (one X) = x;
  asc : forall X x y z, mul X x (mul X y z) = mul X (mul X x y) z;
}.

Answer 2

在这个问题上又敲了几天之后，我得到了不同 Kinds 的类型类继承，据我所知，这是正确的。

我的问题更新是在正确的轨道上。我所需要做的就是添加对 Semigroup 的显式继承。我仍然不确定为什么从集合继承隐式继承可折叠和展开时它必须是显式的。可能是因为forall作为继承的一部分。

另外，我了解到在类型声明中包含函数是不正确的，或者至少是不必要的。我通过阅读 paper by the author of typeclasses in Coq and the Coq reference manual 发现的。（如果向下滚动到 EqDec 类型类，您会看到 eqb 在大括号中键入。）

所以，这是我的 Sequence 类型类现在的样子：

Class Sequence (S : Type -> Type) `{C : Collection S} `{G : forall (A : Type), Semigroup (S A)} `{M : forall (A : Type), Monoid (S A)} := { insert_append_eq : forall (A : Type) (h : S A) (x : A), op (insert A x (empty A)) h = insert A x h }.

为确保这实际上正确地创建了类型类，我定义了一个 List 类型并将其作为 Sequence 的一个实例。不幸的是，这涉及到首先使它成为每个父类型类的实例。请问有没有更简单的方法

为了包含更多代码示例，因为我发现它们比自然语言解释更容易理解，这是我的 Semigroup 类型类和它的 List 实例：

Class Semigroup (S : Type) := { op : S -> S -> S; semigroup_assoc : forall x y z : S, op x (op y z) = op (op x y) z }. Inductive List (A : Type) : Type := | Nil : List A | Cons : A -> List A -> List A . Instance semigroup_list : forall A, Semigroup (List A) := { op := fix append l l' := match l with | Nil => l' | Cons x xs => Cons A x (append xs l') end }. Proof. intros. induction x. apply eq_refl. rewrite IHx. apply eq_refl. Defined.

谢谢你的帮助，Perce。这听起来很刻薄，但你的回答太令人失望了，我不得不弄清楚你是否真的错了。 :)

在 Coq 中继承不同类型的类型类

Inheriting Typeclasses of different Kinds in Coq

typeclass

coq

type-kinds