在Coq中递归使用类型类方法

Question

有没有办法使用Coq的类型类的递归？例如，在为列表定义show时，如果要递归调用列表的show函数，则必须使用如下的修复点：

Require Import Strings.String.
Require Import Strings.Ascii.

Local Open Scope string_scope.


Class Show (A : Type) : Type :=
  {
    show : A -> string
  }.


Section showNormal.

Instance showList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ lshow xs
        end
  }.

End showNormal.

这一切都很好，但如果我想定义一些帮助函数，我将用于定义Show实例怎么办？就像我想要创建一个名为magicShow的更多DAZZLING show函数一样，可以在某些东西周围打印星星......

Definition magicShow {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show a ++ " **".


Instance showMagicList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ magicShow xs
        end
  }.

但是，在这种情况下，Coq无法找到列表xs传递给magicShow的show实例：

Error:
Unable to satisfy the following constraints:
In environment:
A : Type
H : Show A
lshow : list A -> string
l : list A
x : A
xs : list A

?H : "Show (list A)"

一般来说有没有办法做到这一点？即，您是否可以使用依赖于您定义的类型类实例的函数为类型类定义一个方法？

Answer 1

不，没有办法做到这一点。这在Haskell中有效，因为允许任意递归绑定，并且语言不关心绑定的顺序。 Coq在两个方面都更具限制性。如果你考虑一下desugaring的样子，这是有意义的：对show的递归调用将按名称引用当前正在定义的实例，但该绑定尚未在范围内。并且你不能使实例本身成为一个固定点，因为你在一个类型的结构上递归，而不是在代数数据类型的值上。

你的内联fixpoint适用于show，但如果你的方法实现相互引用，问题就会变得更棘手，比如

newtype MyInteger = MyInteger Integer

instance Num MyInteger where
  MyInteger m + MyInteger n = MyInteger $ m  + n
  negate (MyInteger m) = MyInteger $ negate m
  m - n = m + negate n
  -- other methods

在这里，在(+)定义中对negate和(-)的调用需要参考上面的(+)和negate的定义，但这在Coq中也不起作用。唯一的解决方案是单独定义所有方法，手动相互引用，然后通过将每个方法设置为上面定义的方法来定义实例。例如，

Inductive MyInteger := Mk_MyInteger : Integer -> MyInteger.

Definition add__MyInteger (m n : MyInteger) : MyInteger :=
  let 'Mk_MyInteger m' := m in
  let 'Mk_MyInteger n' := n in
  Mk_MyInteger (add m' n').

Definition negate__MyInteger (m : MyInteger) : MyInteger :=
  let 'Mk_MyInteger m' := m in
  Mk_MyInteger (negate m').

Definition sub__MyInteger (m n : MyInteger) : MyInteger :=
  add__MyInteger m (negate__MyInteger n).

Instance Num__MyInteger : Num MyInteger := {|
  add    := add__MyInteger;
  negate := negate__MyInteger;
  sub    := sub__MyInteger;
  (* other methods *)
|}.