使用类型达到某种等价

Question

假设我们想将（签名的）整数表示为Grothendieck组的自然（或者换句话说，作为一对(m, n)，其中所理解的整数是m - n）：

data ZTy : Type where
  MkZ : (m, n : Nat) -> ZTy

现在语言赋予我们的（结构）平等不再是我们想要的：相反，我们只关心某种等价关系（即，(m1, n1) ~ (m2, n2) iff m1 + n2 = m2 + n1）。没什么大不了的，让我们写下来吧！

data Equiv : ZTy -> ZTy -> Type where
  MkEquiv : (prf : m1 + n2  = m2 + n1) -> Equiv (MkZ m1 n1) (MkZ m2 n2)

但是使用它会很快变得混乱。任何类型prop Const（对于prop : ZTy -> Type）的论证都被(k : ZTy) -> (k `EqZ` Const) -> prop k取代，至少可以说（作为一个更实际的例子，我正在努力写下这种类型的双面感应证明，我仍然不确定我得到了那个词的签名吧）。

此外，像replaceZ : {P : ZTy -> Type} -> (k1 `Equiv` k2) -> P k1 -> P k2（显然）的功能不存在，但我找不到更好的候选人。作为一个有趣的旁注/观察，如果我们不导出ZTy的定义，没有客户端代码P可以观察它，并且这个函数对任何其他模块中定义的任何P都有意义，但看起来我们无法内化这个在语言中。

我想到的另一件事是将谓词集限制在等价关系下的谓词集。也就是说，用P : ZTy -> Type取代P : ZTy -> Type, pAdmissible : ZPred P，其中ZPred在等价关系下携带其不变性的证明：

data ZPred : Type -> Type where
  MkZPred : {P : ZTy -> Type} ->
            (preservesEquiv : {k1, k2 : ZTy} -> (k1 `Equiv` k2) -> P k1 -> P k2) ->
            ZPred P

无论如何，使用这些类型的常用方法是什么？还有什么能够很好地运作吗？

我也听说过关于商类型的东西，但我不太了解。

Answer 1

Coq用丰富的“关系组合器”语言来描述这些情况，这是你最后一个想法的更好版本。我会翻译它。你有

ZTy : Type -- as yours

然后你继续定义关系的关系和功能：

-- if r : Relation t and x, y : t, we say x and y are related by r iff r x y is inhabited
Relation : Type -> Type
Relation t = t -> t -> Type

-- if x, y : ZTy, we say x and y are (Equiv)alent iff Equiv x y is inhabited, etc.
Equiv : Relation ZTy  -- as yours
(=)   : Relation a    -- standard
Iso   : Relation Type -- standard

-- f and f' are related by a ==> r if arguments related by a end up related by r
(==>) : Relation a -> Relation b -> Relation (a -> b)
(==>) xr fxr = \f, f' => (x x' : a) -> xr x x' -> fxr (f x) (f' x')
infixr 10 ==>

这个想法是Equiv，(=)和Iso都是平等关系。 Equiv和(=)是两个不同的ZTy平等概念，而(=)和Iso是两个Type平等的概念。 (==>)将关系结合到新的关系中。

如果你有

P : ZTy -> Type

你想说Equivalent参数映射到Isomorphic类型。也就是说，你需要

replaceP : (x x' : ZTy) -> Equiv x x' -> Iso (P x) (P x')

关系语言如何帮助？好吧，replaceP基本上说P与它本身“相等”，在Equiv ==> Iso的关系下（NB Equiv ==> Iso不是等价的，但它唯一缺少的是反身性。）如果一个函数在Equiv ==> Iso下与它自身“不相等”，然后这有点像“矛盾”，并且你的宇宙中的这个功能“不存在”。或者，相反，如果你想写一个函数

f : (ZTy -> Type) -> ?whatever

您可以通过要求这样的证明参数来限制自己使用正确的函数类型

Proper : Relation a -> a -> Type
Proper r x = r x x

f : (P : ZTy -> Type) -> Proper (Equiv ==> Iso) P -> ?whatever

但是，通常情况下，除非绝对需要，否则请不要使用证据。实际上，标准库已经在ZTy上包含了很多函数，比如

concatMap : Monoid m => (ZTy -> m) -> List ZTy -> m

而不是写一个concatMap采取证据论证，你真的只需要写一个关于concatMap的证明：

concatMapProper : Proper ((Equiv ==> (=)) ==> Pairwise Equiv ==> (=))
-- you'd really abstract over Equiv and (=), but then you need classes for Relations
Pairwise : Relation a -> Relation [a] -- as you may guess

我不确定你想写什么感应原理，所以我就把它留下来。但是，你担心的是

proof : Property Constant

总是需要更换

proof : (k : ZTy) -> Equiv k Constant -> Property k

只是部分有根据的。如果你已经拥有

PropertyProper : Proper (Equiv ==> Iso) Property

你很可能应该这样，那么你可以写proper : Property Constant，然后通过PropertyProper把它推到需要的时候进行推广。 （或者，使用proper的简单定义在顶部写下具有一般签名的PropertyProper）。你不能在某处写出证据，因为它根本不是那么微不足道的。

同样值得注意的是，(==>)除了作为Proper的论据之外还有其他用途。它用作通用的扩展相等：

abs1 : ZTy -> Nat
abs1 (MkZ l r) = go l r
  where go (S n) (S m) = go n m
        go Z     m     = m
        go n     Z     = n
abs2 : ZTy -> Nat
abs2 (MkZ l r) = max l r - min l r

absEq : (Equiv ==> (=)) abs1 abs2
--    : (x x' : ZTy) -> Equiv x x' -> abs1 x = abs2 x'