使用达到一定等价的类型

Question

假设我们想将（有符号）整数表示为自然数上的格洛腾迪克群（或者，换句话说，作为一对(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 下（注：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 以对其进行概括。 （或者，通过使用顶部带有PropertyProper 的简单定义，将proper 与一般签名一起写入）。但是，您无法摆脱在某处编写证明，因为它根本不是那么微不足道。

还值得注意的是，(==>) 的用途不是作为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'