idris - 使用达到一定等价的类型

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(for prop : ZTy -> Type) 的参数都被替换为(k : ZTy) -> (k `EqZ` Const) -> prop k，至少可以说（作为一个更应用的例子，我正在努力写下这种类型的双面归纳证明，我仍然不确定我是否得到了该期限权利的签名）。

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

我想到的另一件事是将谓词集限制为在等价关系下成立的谓词。也就是说，用诸如where之P : ZTy -> Type类的东西代替，在等价关系下证明其不变性：P : ZTy -> Type, pAdmissible : ZPred PZPred

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

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

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

标签： idrisdependent-type

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 参数映射到Iso形态类型。也就是说，你需要

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

关系语言如何提供帮助？好吧，replaceP本质上是在关系下说它P与自身“相等” Equiv ==> Iso（NBEquiv ==> 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编写一般签名）。但是，您不能在某处写证明，因为它根本不是那么微不足道。properPropertyProper

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